Theorem: theoryValuationBounding (Fine/SystemB/CanonicalModel.lean)

State before:
⊢ ∀ (t : Th) (x : ℕ), (∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p) → x ∈ theoryValuation t
Tactic:
intros t x h₁
State after:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ x ∈ theoryValuation t

State before:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ x ∈ theoryValuation t
Tactic:
change #x ∈ t.val
State after:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ #x ∈ ↑t

State before:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ #x ∈ ↑t
Tactic:
rw [primeAnalysis t]
State after:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ #x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }

State before:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ #x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
apply Set.mem_interₛ.mpr
State after:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ ∀ (t_1 : Set Form), t_1 ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p } → #x ∈ t_1

State before:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ ∀ (t_1 : Set Form), t_1 ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p } → #x ∈ t_1
Tactic:
intros r h₂
State after:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
r : Set Form
h₂ : r ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ #x ∈ r

State before:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
r : Set Form
h₂ : r ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ #x ∈ r
Tactic:
exact h₁ ⟨⟨r,h₂.right.right⟩,h₂.left⟩ h₂.right.left
State after:
no goals