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

State before:
β✝ : Type u_1
inst✝⁵ : Encodable β✝
ι : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : Primcodable ι
inst✝² : DecidableEq ι
inst✝¹ : IsEmpty ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
⊢ encode f = 0
Tactic:
have : Fintype.card ι = 0 := Fintype.card_eq_zero
State after:
β✝ : Type u_1
inst✝⁵ : Encodable β✝
ι : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : Primcodable ι
inst✝² : DecidableEq ι
inst✝¹ : IsEmpty ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
this : Fintype.card ι = 0
⊢ encode f = 0

State before:
β✝ : Type u_1
inst✝⁵ : Encodable β✝
ι : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : Primcodable ι
inst✝² : DecidableEq ι
inst✝¹ : IsEmpty ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
this : Fintype.card ι = 0
⊢ encode f = 0
Tactic:
simp[encode_fintypeArrow, encode_finArrow, this]
State after:
no goals