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

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Option.isSome (Encodable.decode ↑n) = true
Tactic:
apply Option.isSome_iff_exists.2
State after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∃ a, Encodable.decode ↑n = some a

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∃ a, Encodable.decode ↑n = some a
Tactic:
apply (decode_partial_inv n).imp
State after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∀ (a : α), a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n → Encodable.decode ↑n = some a

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∀ (a : α), a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n → Encodable.decode ↑n = some a
Tactic:
intro _ h
State after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a✝ : α
h : a✝ ∈ Encodable.decode ↑n ∧ Encodable.encode a✝ = ↑n
⊢ Encodable.decode ↑n = some a✝

State before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a✝ : α
h : a✝ ∈ Encodable.decode ↑n ∧ Encodable.encode a✝ = ↑n
⊢ Encodable.decode ↑n = some a✝
Tactic:
exact h.1
State after:
no goals