Theorem: FinDenumerable.equiv_fin (FormalSystems/Preliminaries/FinDenumerable.lean)

State before:
α : Type u_1
inst : FinDenumerable α
⊢ α ≃ Fin (Fintype.card α)
Tactic:
have tmp := Equiv.ofLeftInverse encode_fin (fun _ => inst.decode_fin) (fun _ => encodek_fin_left_inverse)
State after:
α : Type u_1
inst : FinDenumerable α
tmp : α ≃ ↑(Set.range encode_fin)
⊢ α ≃ Fin (Fintype.card α)

State before:
α : Type u_1
inst : FinDenumerable α
tmp : α ≃ ↑(Set.range encode_fin)
⊢ α ≃ Fin (Fintype.card α)
Tactic:
apply Equiv.trans tmp encode_fin_range
State after:
no goals