Theorem: LO.FirstOrder.Semiterm.Operator.comp_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 σ
l : ℕ
o : Operator L 2
⊢ Primrec fun a => encode fun x => (![a.1, a.2] x).term
Tactic:
simp[Matrix.comp_vecCons', Matrix.constant_eq_singleton]
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 σ
l : ℕ
o : Operator L 2
⊢ Primrec fun a => encode ![a.1.term, a.2.term]

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 σ
l : ℕ
o : Operator L 2
⊢ Primrec fun a => encode ![a.1.term, a.2.term]
Tactic:
have : Primrec (fun p : Operator L l × Operator L l => encode [p.1.term, p.2.term]) :=
  Primrec.encode.comp (list_cons.comp (term_primrec.comp fst) $
    list_cons.comp (term_primrec.comp snd) (.const []))
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 σ
l : ℕ
o : Operator L 2
this : Primrec fun p => encode [p.1.term, p.2.term]
⊢ Primrec fun a => encode ![a.1.term, a.2.term]

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 σ
l : ℕ
o : Operator L 2
this : Primrec fun p => encode [p.1.term, p.2.term]
⊢ Primrec fun a => encode ![a.1.term, a.2.term]
Tactic:
exact this.of_eq <| by simp[encode_finArrow]
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 σ
l : ℕ
o : Operator L 2
this : Primrec fun p => encode [p.1.term, p.2.term]
⊢ ∀ (n : Operator L l × Operator L l), encode [n.1.term, n.2.term] = encode ![n.1.term, n.2.term]
Tactic:
simp[encode_finArrow]
State after:
no goals