Theorem: WType.elim_eq_elimL (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 β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
⊢ elim γ f w = elimL (fun a l => f ⟨a, fintypeArrowEquivFinArrow.symm fun i => l.getI ↑i⟩) w
Tactic:
simp[elimL]
State after:
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
⊢ elim γ f w = elim γ (fun x => f ⟨x.fst, fintypeArrowEquivFinArrow.symm fun i => x.snd (fintypeEquivFin.symm i)⟩) w

State before:
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
⊢ elim γ f w = elim γ (fun x => f ⟨x.fst, fintypeArrowEquivFinArrow.symm fun i => x.snd (fintypeEquivFin.symm i)⟩) w
Tactic:
congr
State after:
case e_fγ
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
⊢ f = fun x => f ⟨x.fst, fintypeArrowEquivFinArrow.symm fun i => x.snd (fintypeEquivFin.symm i)⟩

State before:
case e_fγ
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
⊢ f = fun x => f ⟨x.fst, fintypeArrowEquivFinArrow.symm fun i => x.snd (fintypeEquivFin.symm i)⟩
Tactic:
funext ⟨a, j⟩
State after:
case e_fγ.h
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
⊢ f ⟨a, j⟩ = f ⟨⟨a, j⟩.fst, fintypeArrowEquivFinArrow.symm fun i => ⟨a, j⟩.snd (fintypeEquivFin.symm i)⟩

State before:
case e_fγ.h
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
⊢ f ⟨a, j⟩ = f ⟨⟨a, j⟩.fst, fintypeArrowEquivFinArrow.symm fun i => ⟨a, j⟩.snd (fintypeEquivFin.symm i)⟩
Tactic:
simp
State after:
case e_fγ.h
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
⊢ f ⟨a, j⟩ = f ⟨a, fintypeArrowEquivFinArrow.symm fun i => j (fintypeEquivFin.symm i)⟩

State before:
case e_fγ.h
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
⊢ f ⟨a, j⟩ = f ⟨a, fintypeArrowEquivFinArrow.symm fun i => j (fintypeEquivFin.symm i)⟩
Tactic:
congr
State after:
case e_fγ.h.e_a.e_snd
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
⊢ j = fintypeArrowEquivFinArrow.symm fun i => j (fintypeEquivFin.symm i)

State before:
case e_fγ.h.e_a.e_snd
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
⊢ j = fintypeArrowEquivFinArrow.symm fun i => j (fintypeEquivFin.symm i)
Tactic:
funext b
State after:
case e_fγ.h.e_a.e_snd.h
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
b : β a
⊢ j b = fintypeArrowEquivFinArrow.symm (fun i => j (fintypeEquivFin.symm i)) b

State before:
case e_fγ.h.e_a.e_snd.h
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
a : α
j : β a → γ
b : β a
⊢ j b = fintypeArrowEquivFinArrow.symm (fun i => j (fintypeEquivFin.symm i)) b
Tactic:
simp
State after:
no goals