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

State before:
α : Type u_1
inst : FinDenumerable α
⊢ ∀ (n : Fin (Fintype.card α)), encode_fin (decode_fin n) = n
Tactic:
simp [encode_fin, Fin.ext_iff, decode_fin]
State after:
α : Type u_1
inst : FinDenumerable α
⊢ ∀ (n : Fin (Fintype.card α)), Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n

State before:
α : Type u_1
inst : FinDenumerable α
⊢ ∀ (n : Fin (Fintype.card α)), Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Tactic:
intro n
State after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Tactic:
have ⟨ a, ph ⟩ := fin_preimage_exists n
State after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
ph : Encodable.encode a = ↑n
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
ph : Encodable.encode a = ↑n
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Tactic:
simp [<- ph]
State after:
no goals