rw [← Set.toFinset_card, ← edgeFinset, copyCount, ← card_subtype, subtype_univ, card_univ]
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
⊢ Fintype.card ↑H.edgeSet - G.copyCount H = Fintype.card ↑H.edgeSet - Fintype.card { H' // Nonempty (G ≃g H'.coe) }
no goals