Theorem: LO.FirstOrder.UFormula.ofFn_dep_FinArrow_primrec (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
⊢ Primrec fun a => encode (List.ofFn a.2.snd.2)
Tactic:
simp[←encode_finArrow]
State after:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
⊢ Primrec fun a => encode a.2.snd.2

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
⊢ Primrec fun a => encode a.2.snd.2
Tactic:
exact this.of_eq <| by rintro ⟨⟨⟨x, m, p⟩, l⟩, ⟨k, r, v⟩⟩; simp
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
⊢ ∀ (n : ((σ × ℕ × UFormula L μ₁) × List (UFormula L μ₂)) × (k : ℕ) × L.Rel k × (Fin k → UTerm L μ₁)),
    (encode n).unpair.2.unpair.2.unpair.2 = encode n.2.snd.2
Tactic:
rintro ⟨⟨⟨x, m, p⟩, l⟩, ⟨k, r, v⟩⟩
State after:
case mk.mk.mk.mk.mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
l : List (UFormula L μ₂)
x : σ
m : ℕ
p : UFormula L μ₁
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
⊢ (encode (((x, m, p), l), ⟨k, (r, v)⟩)).unpair.2.unpair.2.unpair.2 = encode (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2

State before:
case mk.mk.mk.mk.mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
l : List (UFormula L μ₂)
x : σ
m : ℕ
p : UFormula L μ₁
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
⊢ (encode (((x, m, p), l), ⟨k, (r, v)⟩)).unpair.2.unpair.2.unpair.2 = encode (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2
Tactic:
simp
State after:
no goals