Theorem: LO.FirstOrder.Semiterm.brew_primrec (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
⊢ Primrec₂ fun z x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default
Tactic:
letI : ∀ n, Primcodable { t : UTerm L μ₂ // t.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp UTerm.bv_primrec (Primrec.const n))
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec₂ fun z x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec₂ fun z x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default
Tactic:
have : Primrec₂ (fun z x => (Nat.toFin n₁ x).casesOn default (fun i => (subtEquiv (b z i)).val) : α → ℕ → UTerm L μ₂) :=
  to₂' <| option_casesOn (α := α × ℕ) (nat_toFin.comp snd) (Primrec.const default) <| subtype_val.comp₂ <| of_equiv.comp₂ <|
  to₂' <| finArrow_app (v := fun (p : (α × ℕ) × Fin n₁) => b p.1.1) (hb.comp (fst.comp fst)) snd
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
⊢ Primrec₂ fun z x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
⊢ Primrec₂ fun z x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default
Tactic:
exact this.of_eq <| by
  intro a x; simp[Nat.toFin]
  by_cases hx : x < n₁ <;> simp[hx]
State after:
no goals

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
⊢ ∀ (a : α) (b_1 : ℕ),
    (Option.casesOn (n₁.toFin b_1) default fun i => ↑(subtEquiv (b a i))) =
      if hx : b_1 < n₁ then ↑(subtEquiv (b a ⟨b_1, hx⟩)) else default
Tactic:
intro a x
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
a : α
x : ℕ
⊢ (Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b a i))) =
    if hx : x < n₁ then ↑(subtEquiv (b a ⟨x, hx⟩)) else default

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
a : α
x : ℕ
⊢ (Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b a i))) =
    if hx : x < n₁ then ↑(subtEquiv (b a ⟨x, hx⟩)) else default
Tactic:
simp[Nat.toFin]
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
a : α
x : ℕ
⊢ Option.rec default (fun val => ↑(subtEquiv (b a val))) (if hx : x < n₁ then some ⟨x, hx⟩ else none) =
    if hx : x < n₁ then ↑(subtEquiv (b a ⟨x, hx⟩)) else default

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
a : α
x : ℕ
⊢ Option.rec default (fun val => ↑(subtEquiv (b a val))) (if hx : x < n₁ then some ⟨x, hx⟩ else none) =
    if hx : x < n₁ then ↑(subtEquiv (b a ⟨x, hx⟩)) else default
Tactic:
by_cases hx : x < n₁ <;> simp[hx]
State after:
no goals