Theorem: Primrec.w_depth (Logic/Vorspiel/W.lean)

State before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
⊢ Primrec depth
Tactic:
have : Primrec (fun n => (encodeDecode (WType β) n).map $ fun e => e.unpair.1) :=
  option_map Primrec.encodeDecode (fst.comp₂ $ unpair.comp₂ Primrec₂.right)
State after:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this : Primrec fun n => Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n)
⊢ Primrec depth

State before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this : Primrec fun n => Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n)
⊢ Primrec depth
Tactic:
exact decode_iff.mp (this.of_eq $ fun n => by
  simp[encodeDecode_eq_encode_map_decode]
  rcases decode n <;> simp[WType.encode_eq, WType.SubWType.ofW])
State after:
no goals

State before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this : Primrec fun n => Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n)
n : ℕ
⊢ Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n) = Option.map depth (decode n)
Tactic:
simp[encodeDecode_eq_encode_map_decode]
State after:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this : Primrec fun n => Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n)
n : ℕ
⊢ Option.map ((fun e => e.unpair.1) ∘ encode) (decode n) = Option.map depth (decode n)

State before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this : Primrec fun n => Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n)
n : ℕ
⊢ Option.map ((fun e => e.unpair.1) ∘ encode) (decode n) = Option.map depth (decode n)
Tactic:
rcases decode n <;> simp[WType.encode_eq, WType.SubWType.ofW]
State after:
no goals