calc
  _ = H.edgeFinset.card - card {H' : H.Subgraph // Nonempty (G ≃g H'.coe)} := ?_
  _ ≤ H.edgeFinset.card - (univ.image f).card := Nat.sub_le_sub_left card_image_le _
  _ = H.edgeFinset.card - (Set.range f).toFinset.card := by rw [Set.toFinset_range]
  _ ≤ (H.edgeFinset \ (Set.range f).toFinset).card := le_card_sdiff ..
  _ = (G.kill H).edgeFinset.card := ?_
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ H.edgeFinset.card - G.copyCount H ≤ (G.kill H).edgeFinset.card
case inr.calc_1
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ H.edgeFinset.card - G.copyCount H = H.edgeFinset.card - Fintype.card { H' // Nonempty (G ≃g H'.coe) }

case inr.calc_2
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ (H.edgeFinset \ (Set.range f).toFinset).card = (G.kill H).edgeFinset.card