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

State before:
α : Type
inst : Model α
p : Model.primes
f : Form
⊢ ¬p⊨~f → p*⊨f
Tactic:
intros h₁
State after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
⊢ p*⊨f

State before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
⊢ p*⊨f
Tactic:
have ⟨x, l₁⟩ := nonconstruction h₁
State after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
⊢ p*⊨f

State before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
⊢ p*⊨f
Tactic:
have ⟨l₂,l₃⟩ := nonconstruction l₁
State after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
l₂ : ↑p ≤ ↑x
l₃ : ¬¬↑(x*)⊨f
⊢ p*⊨f

State before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
l₂ : ↑p ≤ ↑x
l₃ : ¬¬↑(x*)⊨f
⊢ p*⊨f
Tactic:
have l₄ := byContradiction l₃
State after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
l₂ : ↑p ≤ ↑x
l₃ : ¬¬↑(x*)⊨f
l₄ : ↑(x*)⊨f
⊢ p*⊨f

State before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
l₂ : ↑p ≤ ↑x
l₃ : ¬¬↑(x*)⊨f
l₄ : ↑(x*)⊨f
⊢ p*⊨f
Tactic:
have l₅ := inst.starAntitone l₂
State after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
l₂ : ↑p ≤ ↑x
l₃ : ¬¬↑(x*)⊨f
l₄ : ↑(x*)⊨f
l₅ : x* ≤ p*
⊢ p*⊨f

State before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
l₂ : ↑p ≤ ↑x
l₃ : ¬¬↑(x*)⊨f
l₄ : ↑(x*)⊨f
l₅ : x* ≤ p*
⊢ p*⊨f
Tactic:
exact upwardsClosure l₅ l₄
State after:
no goals