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

State before:
α : Type u_1
inst : FinDenumerable α
⊢ ↑(Set.range encode_fin) ≃ Fin (Fintype.card α)
Tactic:
rw [Function.Surjective.range_eq _]
State after:
α : Type u_1
inst : FinDenumerable α
⊢ ↑Set.univ ≃ Fin (Fintype.card α)

α : Type u_1
inst : FinDenumerable α
⊢ Function.Surjective encode_fin

State before:
α : Type u_1
inst : FinDenumerable α
⊢ ↑Set.univ ≃ Fin (Fintype.card α)

α : Type u_1
inst : FinDenumerable α
⊢ Function.Surjective encode_fin
Tactic:
exact Equiv.Set.univ (Fin (Fintype.card α))
State after:
α : Type u_1
inst : FinDenumerable α
⊢ Function.Surjective encode_fin

State before:
α : Type u_1
inst : FinDenumerable α
⊢ Function.Surjective encode_fin
Tactic:
exact encode_fin_bijective.surjective
State after:
no goals