Theorem: Encodable.fintypeEquivFin_symm_zero (Logic/Vorspiel/Computability.lean)

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ fintypeEquivFin.symm 0 = false
Tactic:
simp [fintypeEquivFin]
State after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ (sortedUniv Bool).get (cast ⋯ 0) = false

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ (sortedUniv Bool).get (cast ⋯ 0) = false
Tactic:
rfl
State after:
no goals