Theorem: Digraph.Iso.card_eq_of_iso (GraphProjects/Digraph.lean)

State before:
ι : Sort ?u.420619
𝕜 : Type ?u.420622
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f✝ : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
f : G ≃g G'
⊢ Fintype.card V = Fintype.card W
Tactic:
rw [← Fintype.ofEquiv_card f.toEquiv]
State after:
ι : Sort ?u.420619
𝕜 : Type ?u.420622
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f✝ : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
f : G ≃g G'
⊢ Fintype.card W = Fintype.card W

State before:
ι : Sort ?u.420619
𝕜 : Type ?u.420622
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f✝ : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
f : G ≃g G'
⊢ Fintype.card W = Fintype.card W
Tactic:
apply @Fintype.card_congr' _ _ (_) (_) rfl
State after:
no goals