α✝ : Type ?u.4685
β✝ : Type ?u.4688
γ : Type ?u.4691
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card β = card β
α✝ : Type ?u.4685
β✝ : Type ?u.4688
γ : Type ?u.4691
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card α = card β
rw [← ofEquiv_card f]
case h.e_2.h
α✝ : Type ?u.4685
β✝ : Type ?u.4688
γ : Type ?u.4691
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ ofEquiv α f = inst✝
α✝ : Type ?u.4685
β✝ : Type ?u.4688
γ : Type ?u.4691
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card β = card β
congr
no goals
case h.e_2.h
α✝ : Type ?u.4685
β✝ : Type ?u.4688
γ : Type ?u.4691
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ ofEquiv α f = inst✝
apply Subsingleton.elim