Theorem: FinDenumerable.fin_decode_eq_decode₂ (FormalSystems/Preliminaries/FinDenumerable.lean)

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.decode ↑n = Encodable.decode₂ α ↑n
Tactic:
rw [← Option.some_get (decode_fin_is_some n)]
State after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ some (Option.get (Encodable.decode ↑n) ⋯) = Encodable.decode₂ α ↑n

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ some (Option.get (Encodable.decode ↑n) ⋯) = Encodable.decode₂ α ↑n
Tactic:
apply Eq.symm
State after:
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.decode₂ α ↑n = some (Option.get (Encodable.decode ↑n) ⋯)

State before:
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.decode₂ α ↑n = some (Option.get (Encodable.decode ↑n) ⋯)
Tactic:
rw [Encodable.decode₂_is_partial_inv]
State after:
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n

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

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