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

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ fintypeEquivFin true = 1
Tactic:
simp [fintypeEquivFin]
State after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ cast ⋯ ((List.Nodup.getEquivOfForallMemList (sortedUniv Bool) ⋯ ⋯).symm true) = 1

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ cast ⋯ ((List.Nodup.getEquivOfForallMemList (sortedUniv Bool) ⋯ ⋯).symm true) = 1
Tactic:
rfl
State after:
no goals