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

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

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

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

State before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.and q).bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p ∧ ↑(ofSubformula (q.toSubformula ⋯)) = q
Tactic:
exact ⟨ofSubformula_toSubformula p (by simp at h; exact h.1), ofSubformula_toSubformula q (by simp at h; exact h.2)⟩
State after:
no goals

State before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.and q).bv ≤ x✝
⊢ p.bv ≤ x✝
Tactic:
simp at h
State after:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : p.bv ≤ x✝ ∧ q.bv ≤ x✝
⊢ p.bv ≤ x✝

State before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : p.bv ≤ x✝ ∧ q.bv ≤ x✝
⊢ p.bv ≤ x✝
Tactic:
exact h.1
State after:
no goals

State before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.and q).bv ≤ x✝
⊢ q.bv ≤ x✝
Tactic:
simp at h
State after:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : p.bv ≤ x✝ ∧ q.bv ≤ x✝
⊢ q.bv ≤ x✝

State before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : p.bv ≤ x✝ ∧ q.bv ≤ x✝
⊢ q.bv ≤ x✝
Tactic:
exact h.2
State after:
no goals

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

State before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.or q).bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p ∧ ↑(ofSubformula (q.toSubformula ⋯)) = q
Tactic:
exact ⟨ofSubformula_toSubformula p (by simp at h; exact h.1), ofSubformula_toSubformula q (by simp at h; exact h.2)⟩
State after:
no goals

State before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.or q).bv ≤ x✝
⊢ p.bv ≤ x✝
Tactic:
simp at h
State after:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : p.bv ≤ x✝ ∧ q.bv ≤ x✝
⊢ p.bv ≤ x✝

State before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.or q).bv ≤ x✝
⊢ q.bv ≤ x✝
Tactic:
simp at h
State after:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : p.bv ≤ x✝ ∧ q.bv ≤ x✝
⊢ q.bv ≤ x✝

State before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.all.bv ≤ x✝
⊢ ↑(ofSubformula (p.all.toSubformula h)) = p.all
Tactic:
simp[ofSubformula, toSubformula]
State after:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.all.bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p

State before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.all.bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p
Tactic:
exact ofSubformula_toSubformula p (by simp only [bv_all] at h; exact Nat.le_add_of_sub_le h)
State after:
no goals

State before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.all.bv ≤ x✝
⊢ p.bv ≤ x✝ + 1
Tactic:
simp only [bv_all] at h
State after:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.bv.pred ≤ x✝
⊢ p.bv ≤ x✝ + 1

State before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.bv.pred ≤ x✝
⊢ p.bv ≤ x✝ + 1
Tactic:
exact Nat.le_add_of_sub_le h
State after:
no goals

State before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.ex.bv ≤ x✝
⊢ ↑(ofSubformula (p.ex.toSubformula h)) = p.ex
Tactic:
simp[ofSubformula, toSubformula]
State after:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.ex.bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p

State before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.ex.bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p
Tactic:
exact ofSubformula_toSubformula p (by simp only [bv_ex] at h; exact Nat.le_add_of_sub_le h)
State after:
no goals

State before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.ex.bv ≤ x✝
⊢ p.bv ≤ x✝ + 1
Tactic:
simp only [bv_ex] at h
State after:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.bv.pred ≤ x✝
⊢ p.bv ≤ x✝ + 1