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

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∃ a ∈ Encodable.decode ↑n, Encodable.encode a = ↑n
Tactic:
have ⟨ a, pa, _ ⟩  := encode_fin_bijective.existsUnique n
State after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
pa : (fun a => encode_fin a = n) a
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
⊢ ∃ a ∈ Encodable.decode ↑n, Encodable.encode a = ↑n

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
pa : (fun a => encode_fin a = n) a
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
⊢ ∃ a ∈ Encodable.decode ↑n, Encodable.encode a = ↑n
Tactic:
exists a
State after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
pa : (fun a => encode_fin a = n) a
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
⊢ a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
pa : (fun a => encode_fin a = n) a
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
⊢ a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n
Tactic:
simp [Fin.ext_iff, encode_fin] at pa
State after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
pa : Encodable.encode a = ↑n
⊢ a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
pa : Encodable.encode a = ↑n
⊢ a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n
Tactic:
simp [pa]
State after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
pa : Encodable.encode a = ↑n
⊢ Encodable.decode ↑n = some a

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
pa : Encodable.encode a = ↑n
⊢ Encodable.decode ↑n = some a
Tactic:
simp [<- pa]
State after:
no goals