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

State before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
hι : Fintype.card ι = 1
β : Type u_3
inst✝ : Primcodable β
f : ι → β
i : ι
⊢ encode f = encode [f i]
Tactic:
have : Subsingleton ι := Fintype.card_le_one_iff_subsingleton.mp (by simp[hι])
State after:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
hι : Fintype.card ι = 1
β : Type u_3
inst✝ : Primcodable β
f : ι → β
i : ι
this : Subsingleton ι
⊢ encode f = encode [f i]

State before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
hι : Fintype.card ι = 1
β : Type u_3
inst✝ : Primcodable β
f : ι → β
i : ι
⊢ Fintype.card ι ≤ 1
Tactic:
simp[hι]
State after:
no goals