simp only [kill_of_ne_bot, hG, Ne, not_false_iff, Set.iUnion_singleton_eq_range,
  Set.toFinset_card, Fintype.card_ofFinset, edgeSet_deleteEdges]
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
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 =
    Fintype.card ↑(H.edgeSet \ ⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})