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

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

State before:
α : Type
inst : Model α
s t : α
f : Form
h₁ : s ≤ t
g : Form
h₂ : s⊨~g
p : Model.primes
h₃ : t ≤ ↑p
h₄ : ↑(p*)⊨g
⊢ False
Tactic:
exact h₂ (le_trans h₁ h₃) h₄
State after:
no goals

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨f&g
Tactic:
apply And.intro
State after:
case left
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨f

case right
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨g

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨f
Tactic:
case left => exact upwardsClosure h₁ h₂.left
State after:
no goals

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨g
Tactic:
case right => exact upwardsClosure h₁ h₂.right
State after:
no goals

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨f
Tactic:
exact upwardsClosure h₁ h₂.left
State after:
no goals

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨g
Tactic:
exact upwardsClosure h₁ h₂.right
State after:
no goals

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
⊢ t⊨f¦g
Tactic:
intros p h₃
State after:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
apply Or.elim (h₂ (le_trans' h₃ h₁))
State after:
case left
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨f → ↑p⊨f ∨ ↑p⊨g

case right
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨g → ↑p⊨f ∨ ↑p⊨g

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨f → ↑p⊨f ∨ ↑p⊨g
Tactic:
case left => intro h₄; exact Or.inl h₄
State after:
no goals

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨g → ↑p⊨f ∨ ↑p⊨g
Tactic:
case right => intro h₄; exact Or.inr h₄
State after:
no goals

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨f → ↑p⊨f ∨ ↑p⊨g
Tactic:
intro h₄
State after:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
h₄ : ↑p⊨f
⊢ ↑p⊨f ∨ ↑p⊨g

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
h₄ : ↑p⊨f
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
exact Or.inl h₄
State after:
no goals

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
⊢ ↑p⊨g → ↑p⊨f ∨ ↑p⊨g
Tactic:
intro h₄
State after:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
h₄ : ↑p⊨g
⊢ ↑p⊨f ∨ ↑p⊨g

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f¦g
p : Model.primes
h₃ : t ≤ ↑p
h₄ : ↑p⊨g
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
exact Or.inr h₄
State after:
no goals

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
⊢ t⊨f⊃g
Tactic:
intros u h₃
State after:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
u : α
h₃ : u⊨f
⊢ t∙u⊨g

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
u : α
h₃ : u⊨f
⊢ t∙u⊨g
Tactic:
have l₁ : s ∙ u ≤ t ∙ u := inst.appMonotoneRight u h₁
State after:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
u : α
h₃ : u⊨f
l₁ : s∙u ≤ t∙u
⊢ t∙u⊨g

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
u : α
h₃ : u⊨f
l₁ : s∙u ≤ t∙u
⊢ t∙u⊨g
Tactic:
have l₂ : (s ∙ u) ⊨ g := h₂ h₃
State after:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
u : α
h₃ : u⊨f
l₁ : s∙u ≤ t∙u
l₂ : s∙u⊨g
⊢ t∙u⊨g

State before:
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f⊃g
u : α
h₃ : u⊨f
l₁ : s∙u ≤ t∙u
l₂ : s∙u⊨g
⊢ t∙u⊨g
Tactic:
exact upwardsClosure l₁ l₂
State after:
no goals