Theorem: WType.SubWType.depth_decode_primrec (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 β
⊢ Primrec₂ fun s e => Option.map (fun w => (↑w).depth) (decode e)
Tactic:
have : Primrec₂ (elimDecode β (fun a l => l.sup + 1)) :=
  primrec_elimDecode β (by simp only [← Nat.succ_eq_add_one]; apply Primrec.succ.comp $ (list_sup nat_max).comp snd)
State after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
this : Primrec₂ (elimDecode β fun a l => l.sup + 1)
⊢ Primrec₂ fun s e => Option.map (fun w => (↑w).depth) (decode e)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
this : Primrec₂ (elimDecode β fun a l => l.sup + 1)
⊢ Primrec₂ fun s e => Option.map (fun w => (↑w).depth) (decode e)
Tactic:
exact this.of_eq (by simp[depth_eq_elimDecode])
State after:
no goals

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
⊢ Primrec₂ fun a l => l.sup + 1
Tactic:
simp only [← Nat.succ_eq_add_one]
State after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
⊢ Primrec₂ fun a l => l.sup.succ

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
⊢ Primrec₂ fun a l => l.sup.succ
Tactic:
apply Primrec.succ.comp $ (list_sup nat_max).comp snd
State after:
no goals

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
this : Primrec₂ (elimDecode β fun a l => l.sup + 1)
⊢ ∀ (a b : ℕ), elimDecode β (fun a l => l.sup + 1) a b = Option.map (fun w => (↑w).depth) (decode b)
Tactic:
simp[depth_eq_elimDecode]
State after:
no goals