simp only [Finset.sdiff_eq_inter_compl, Set.diff_eq, ← Set.iUnion_singleton_eq_range, coe_sdiff,
  Set.coe_toFinset, coe_filter, Set.sep_mem_eq, Set.iUnion_subtype, ← Fintype.card_coe,
  ← Finset.coe_sort_coe, coe_inter, coe_compl, Set.coe_toFinset, Set.compl_iUnion,
  Fintype.card_ofFinset]
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})
no goals