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

State before:
L : Language
μ : Type v
x✝ arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝
⊢ (↑(ofSubformula (Semiformula.rel r v))).toSubformula ⋯ = Semiformula.rel r v
Tactic:
simp[ofSubformula, toSubformula, UTerm.toSubterm_ofSubterm]
State after:
no goals

State before:
L : Language
μ : Type v
x✝ arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝
⊢ (↑(ofSubformula (Semiformula.nrel r v))).toSubformula ⋯ = Semiformula.nrel r v
Tactic:
simp[ofSubformula, toSubformula, UTerm.toSubterm_ofSubterm]
State after:
no goals

State before:
L : Language
μ : Type v
x✝ : ℕ
p q : Semiformula L μ x✝
⊢ (↑(ofSubformula (p ⋏ q))).toSubformula ⋯ = p ⋏ q
Tactic:
simp[ofSubformula, toSubformula]
State after:
L : Language
μ : Type v
x✝ : ℕ
p q : Semiformula L μ x✝
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p ∧ (↑(ofSubformula q)).toSubformula ⋯ = q

State before:
L : Language
μ : Type v
x✝ : ℕ
p q : Semiformula L μ x✝
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p ∧ (↑(ofSubformula q)).toSubformula ⋯ = q
Tactic:
exact ⟨toSubformula_ofSubformula p, toSubformula_ofSubformula q⟩
State after:
no goals

State before:
L : Language
μ : Type v
x✝ : ℕ
p q : Semiformula L μ x✝
⊢ (↑(ofSubformula (p ⋎ q))).toSubformula ⋯ = p ⋎ q
Tactic:
simp[ofSubformula, toSubformula]
State after:
L : Language
μ : Type v
x✝ : ℕ
p q : Semiformula L μ x✝
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p ∧ (↑(ofSubformula q)).toSubformula ⋯ = q

State before:
L : Language
μ : Type v
x✝ : ℕ
p : Semiformula L μ (x✝ + 1)
⊢ (↑(ofSubformula (∀' p))).toSubformula ⋯ = ∀' p
Tactic:
simp[ofSubformula, toSubformula]
State after:
L : Language
μ : Type v
x✝ : ℕ
p : Semiformula L μ (x✝ + 1)
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p

State before:
L : Language
μ : Type v
x✝ : ℕ
p : Semiformula L μ (x✝ + 1)
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p
Tactic:
exact toSubformula_ofSubformula p
State after:
no goals

State before:
L : Language
μ : Type v
x✝ : ℕ
p : Semiformula L μ (x✝ + 1)
⊢ (↑(ofSubformula (∃' p))).toSubformula ⋯ = ∃' p
Tactic:
simp[ofSubformula, toSubformula]
State after:
L : Language
μ : Type v
x✝ : ℕ
p : Semiformula L μ (x✝ + 1)
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p