Theorem: primeDetermination (Fine/Semantics/Satisfaction.lean)

State before:
α : Type
inst : Model α
t : α
f✝ f : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨~f
⊢ t⊨~f
Tactic:
intros p h₂ h₃
State after:
α : Type
inst : Model α
t : α
f✝ f : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨~f
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False

State before:
α : Type
inst : Model α
t : α
f✝ f : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨~f
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False
Tactic:
exact h₁ p h₂ (le_refl p.val) h₃
State after:
no goals

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨f&g
Tactic:
apply And.intro
State after:
case left
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨f

case right
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨g

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨f
Tactic:
case left => 
  have l₁ : ∀p : inst.primes, t ≤ p → p ⊨ f := by
    intros p h₂
    exact (h₁ p h₂).left
  exact primeDetermination l₁
State after:
no goals

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨g
Tactic:
case right =>
  have l₁ : ∀p : inst.primes, t ≤ p → p ⊨ g := by
    intros p h₂
    exact (h₁ p h₂).right
  exact primeDetermination l₁
State after:
no goals

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨f
Tactic:
have l₁ : ∀p : inst.primes, t ≤ p → p ⊨ f := by
  intros p h₂
  exact (h₁ p h₂).left
State after:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
l₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f
⊢ t⊨f

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
l₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f
⊢ t⊨f
Tactic:
exact primeDetermination l₁
State after:
no goals

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ ∀ (p : Model.primes), t ≤ ↑p → p⊨f
Tactic:
intros p h₂
State after:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
p : Model.primes
h₂ : t ≤ ↑p
⊢ p⊨f

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
p : Model.primes
h₂ : t ≤ ↑p
⊢ p⊨f
Tactic:
exact (h₁ p h₂).left
State after:
no goals

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨g
Tactic:
have l₁ : ∀p : inst.primes, t ≤ p → p ⊨ g := by
  intros p h₂
  exact (h₁ p h₂).right
State after:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
l₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨g
⊢ t⊨g

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
l₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨g
⊢ t⊨g
Tactic:
exact primeDetermination l₁
State after:
no goals

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ ∀ (p : Model.primes), t ≤ ↑p → p⊨g
Tactic:
intros p h₂
State after:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
p : Model.primes
h₂ : t ≤ ↑p
⊢ p⊨g

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
p : Model.primes
h₂ : t ≤ ↑p
⊢ p⊨g
Tactic:
exact (h₁ p h₂).right
State after:
no goals

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
⊢ t⊨f¦g
Tactic:
intros p h₂
State after:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
cases h₁ p h₂ (le_refl p.val)
State after:
case inl
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨f
⊢ ↑p⊨f ∨ ↑p⊨g

case inr
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨g
⊢ ↑p⊨f ∨ ↑p⊨g

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨f
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
case inl => apply Or.inl; assumption
State after:
no goals

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨g
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
case inr => apply Or.inr; assumption
State after:
no goals

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨f
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
apply Or.inl
State after:
case h
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨f
⊢ ↑p⊨f

State before:
case h
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨f
⊢ ↑p⊨f
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨g
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
apply Or.inr
State after:
case h
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨g
⊢ ↑p⊨g

State before:
case h
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f¦g
p : Model.primes
h₂ : t ≤ ↑p
h✝ : ↑p⊨g
⊢ ↑p⊨g
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
⊢ t⊨f⊃g
Tactic:
intros u h₂
State after:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
⊢ t∙u⊨g

State before:
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
⊢ t∙u⊨g
Tactic:
apply primeDetermination
State after:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
⊢ ∀ (p : Model.primes), t∙u ≤ ↑p → p⊨g

State before:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
⊢ ∀ (p : Model.primes), t∙u ≤ ↑p → p⊨g
Tactic:
intros p h₃
State after:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
⊢ p⊨g

State before:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
⊢ p⊨g
Tactic:
have ⟨q, _, l₃,_,l₄,_⟩ : ∃q r : inst.primes, t ≤ q ∧ u ≤ r ∧ (↑q ∙ u) ≤ p ∧ (t ∙ r) ≤ p.val := inst.appBounding t u p h₃
State after:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
q w✝ : Subtype Model.prime
l₃ : t ≤ ↑q
left✝ : u ≤ ↑w✝
l₄ : ↑q∙u ≤ ↑p
right✝ : t∙↑w✝ ≤ ↑p
⊢ p⊨g

State before:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
q w✝ : Subtype Model.prime
l₃ : t ≤ ↑q
left✝ : u ≤ ↑w✝
l₄ : ↑q∙u ≤ ↑p
right✝ : t∙↑w✝ ≤ ↑p
⊢ p⊨g
Tactic:
have l₅ : (↑q ∙ u) ⊨ g  := h₁ q l₃ h₂
State after:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
q w✝ : Subtype Model.prime
l₃ : t ≤ ↑q
left✝ : u ≤ ↑w✝
l₄ : ↑q∙u ≤ ↑p
right✝ : t∙↑w✝ ≤ ↑p
l₅ : ↑q∙u⊨g
⊢ p⊨g

State before:
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
q w✝ : Subtype Model.prime
l₃ : t ≤ ↑q
left✝ : u ≤ ↑w✝
l₄ : ↑q∙u ≤ ↑p
right✝ : t∙↑w✝ ≤ ↑p
l₅ : ↑q∙u⊨g
⊢ p⊨g
Tactic:
exact upwardsClosure l₄ l₅
State after:
no goals