simp
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
⊢ H.edgeFinset.card - ⊥.copyCount H ≤ (⊥.kill H).edgeFinset.card
no goals