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

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

State before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : p*⊨f
h₂ : p⊨~f
⊢ False
Tactic:
unfold psatisfies at h₂
State after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : p*⊨f
h₂ : ↑p⊨~f
⊢ False

State before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : p*⊨f
h₂ : ↑p⊨~f
⊢ False
Tactic:
unfold satisfies at h₂
State after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : p*⊨f
h₂ : ∀ {p_1 : Model.primes}, ↑p ≤ ↑p_1 → ¬↑(p_1*)⊨f
⊢ False

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