Theorem: WType.mk₀_eq (Logic/Vorspiel/W.lean)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
h : IsEmpty (β a)
⊢ mk₀ a = some (mk a h.elim')
Tactic:
simp[mk₀, mkL, Fintype.card_eq_zero_iff.mpr h]
State after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
h : IsEmpty (β a)
⊢ (fintypeArrowEquivFinArrow.symm fun i => [].get (Fin.cast ⋯ i)) = h.elim'

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
h : IsEmpty (β a)
⊢ (fintypeArrowEquivFinArrow.symm fun i => [].get (Fin.cast ⋯ i)) = h.elim'
Tactic:
funext x
State after:
case h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
h : IsEmpty (β a)
x : β a
⊢ fintypeArrowEquivFinArrow.symm (fun i => [].get (Fin.cast ⋯ i)) x = h.elim' x

State before:
case h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
h : IsEmpty (β a)
x : β a
⊢ fintypeArrowEquivFinArrow.symm (fun i => [].get (Fin.cast ⋯ i)) x = h.elim' x
Tactic:
exact IsEmpty.elim h x
State after:
no goals