ι : Sort ?u.637529
𝕜 : Type ?u.637532
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
f✝ : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
f : G ≃g G'
⊢ Fintype.card W = Fintype.card W
ι : Sort ?u.637529
𝕜 : Type ?u.637532
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
f✝ : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
f : G ≃g G'
⊢ Fintype.card V = Fintype.card W
rw [← Fintype.ofEquiv_card f.toEquiv]
no goals
ι : Sort ?u.637529
𝕜 : Type ?u.637532
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
f✝ : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
f : G ≃g G'
⊢ Fintype.card W = Fintype.card W
apply @Fintype.card_congr' _ _ (_) (_) rfl