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 : ℕ
this : Primrec₂ fun f t => funcL ⟨1, f⟩ [t]
⊢ ∀ (a : L.Func 1) (b : Semiterm L μ n), funcL ⟨1, a⟩ [b] = some (func a ![b])
Tactic:
intro f t
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 ⟨1, f⟩ [t]
f : L.Func 1
t : Semiterm L μ n
⊢ funcL ⟨1, f⟩ [t] = some (func f ![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 ⟨1, f⟩ [t]
f : L.Func 1
t : Semiterm L μ n
⊢ funcL ⟨1, f⟩ [t] = some (func f ![t])
Tactic:
simp[funcL, Matrix.constant_eq_singleton]
State after:
no goals