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

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

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