Theorem: negation_not_cosatisfiable (Bml/Semantics.lean)

State before:
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
⊢ ¬Satisfiable X
Tactic:
rintro ⟨W,M,w,satX⟩
State after:
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
⊢ False

State before:
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
⊢ False
Tactic:
have := satX φ phi_in
State after:
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
this : Evaluate (M, w) φ
⊢ False

State before:
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
this : Evaluate (M, w) φ
⊢ False
Tactic:
have := satX (~φ) notPhi_in
State after:
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
this✝ : Evaluate (M, w) φ
this : Evaluate (M, w) (~φ)
⊢ False

State before:
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
this✝ : Evaluate (M, w) φ
this : Evaluate (M, w) (~φ)
⊢ False
Tactic:
tauto
State after:
no goals