Theorem: LO.FirstOrder.Semiterm.func₂_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
n : ℕ
⊢ Primrec₂ fun a b => some (func a ![b.1, b.2])
Tactic:
have : Primrec₂ (fun f t => funcL ⟨2, f⟩ [t.1, t.2] : L.Func 2 → Semiterm L μ n × Semiterm L μ n → Option (Semiterm L μ n)) :=
  (funcL_primrec' 2).comp₂ Primrec₂.left
    <| list_cons.comp₂ (fst.comp₂ Primrec₂.right) <| list_cons.comp₂ (snd.comp₂ Primrec₂.right) (Primrec₂.const [])
State after:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
⊢ Primrec₂ fun a b => some (func a ![b.1, b.2])

State before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
⊢ Primrec₂ fun a b => some (func a ![b.1, b.2])
Tactic:
exact this.of_eq <| fun f ⟨t₁, t₂⟩ => by
  simp[funcL]
  funext i; cases i using Fin.cases <;> simp
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
n : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
f : L.Func 2
x✝ : Semiterm L μ n × Semiterm L μ n
t₁ t₂ : Semiterm L μ n
⊢ funcL ⟨2, f⟩ [(t₁, t₂).1, (t₁, t₂).2] = some (func f ![(t₁, t₂).1, (t₁, t₂).2])
Tactic:
simp[funcL]
State after:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
f : L.Func 2
x✝ : Semiterm L μ n × Semiterm L μ n
t₁ t₂ : Semiterm L μ n
⊢ (fun i => [t₁, t₂].get i) = ![t₁, t₂]

State before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
f : L.Func 2
x✝ : Semiterm L μ n × Semiterm L μ n
t₁ t₂ : Semiterm L μ n
⊢ (fun i => [t₁, t₂].get i) = ![t₁, t₂]
Tactic:
funext i
State after:
case h
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
f : L.Func 2
x✝ : Semiterm L μ n × Semiterm L μ n
t₁ t₂ : Semiterm L μ n
i : Fin 2
⊢ [t₁, t₂].get i = ![t₁, t₂] i

State before:
case h
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
f : L.Func 2
x✝ : Semiterm L μ n × Semiterm L μ n
t₁ t₂ : Semiterm L μ n
i : Fin 2
⊢ [t₁, t₂].get i = ![t₁, t₂] i
Tactic:
cases i using Fin.cases <;> simp
State after:
no goals