Theorem: LO.FirstOrder.Semiformula.and_primrec (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
⊢ Primrec₂ fun x x_1 => x ⋏ x_1
Tactic:
letI : ∀ n , Primcodable { p : UFormula L μ // p.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp 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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec₂ fun x x_1 => x ⋏ x_1

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec₂ fun x x_1 => x ⋏ x_1
Tactic:
have : Primrec₂ (fun p q => UFormula.and (subfEquiv p) (subfEquiv q)
    : Semiformula L μ n → Semiformula L μ n → UFormula L μ) :=
  UFormula.and_primrec.comp₂
    (subtype_val.comp₂ $ of_equiv.comp₂ Primrec₂.left)
    (subtype_val.comp₂ $ of_equiv.comp₂ Primrec₂.right)
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).and ↑(subfEquiv q)
⊢ Primrec₂ fun x x_1 => x ⋏ x_1

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).and ↑(subfEquiv q)
⊢ Primrec₂ fun x x_1 => x ⋏ x_1
Tactic:
exact Primrec₂.encode_iff.mp <| (Primrec.encode.comp₂ this).of_eq <| by
  intro p q
  simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).and ↑(subfEquiv q)
⊢ ∀ (a b : Semiformula L μ n), encode ((↑(subfEquiv a)).and ↑(subfEquiv b)) = encode (a ⋏ b)
Tactic:
intro p q
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).and ↑(subfEquiv q)
p q : Semiformula L μ n
⊢ encode ((↑(subfEquiv p)).and ↑(subfEquiv q)) = encode (p ⋏ q)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).and ↑(subfEquiv q)
p q : Semiformula L μ n
⊢ encode ((↑(subfEquiv p)).and ↑(subfEquiv q)) = encode (p ⋏ q)
Tactic:
simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
State after:
no goals