Theorem: sat_double_neq_invariant (Bml/Semantics.lean)

State before:
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {~~φ}) ↔ Satisfiable (X ∪ {φ})
Tactic:
constructor
State after:
case mp
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {~~φ}) → Satisfiable (X ∪ {φ})

case mpr
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {φ}) → Satisfiable (X ∪ {~~φ})

State before:
case mp
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {~~φ}) → Satisfiable (X ∪ {φ})

case mpr
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {φ}) → Satisfiable (X ∪ {~~φ})
Tactic:
all_goals rintro ⟨W,M,w,satX⟩
State after:
case mp.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {φ})

case mpr.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {~~φ})

State before:
case mp.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {φ})

case mpr.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {~~φ})
Tactic:
all_goals use W, M, w
State after:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
⊢ ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1

case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1

State before:
case mpr
X : Finset Formula
φ : Formula
⊢ Satisfiable (X ∪ {φ}) → Satisfiable (X ∪ {~~φ})
Tactic:
rintro ⟨W,M,w,satX⟩
State after:
case mpr.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {~~φ})

State before:
case mpr.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {~~φ})
Tactic:
use W, M, w
State after:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1

State before:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
⊢ ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
Tactic:
intro φ' is_in
State after:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∪ {φ}
⊢ Evaluate (M, w) φ'

State before:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∪ {φ}
⊢ Evaluate (M, w) φ'
Tactic:
simp at is_in
State after:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∨ φ' = φ
⊢ Evaluate (M, w) φ'

State before:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∨ φ' = φ
⊢ Evaluate (M, w) φ'
Tactic:
cases is_in
State after:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' ∈ X
⊢ Evaluate (M, w) φ'

case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' = φ
⊢ Evaluate (M, w) φ'

State before:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' ∈ X
⊢ Evaluate (M, w) φ'
Tactic:
specialize satX φ'
State after:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {~~φ} → Evaluate (M, w) φ'
⊢ Evaluate (M, w) φ'

State before:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {~~φ} → Evaluate (M, w) φ'
⊢ Evaluate (M, w) φ'
Tactic:
apply satX
State after:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {~~φ} → Evaluate (M, w) φ'
⊢ φ' ∈ X ∪ {~~φ}

State before:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {~~φ} → Evaluate (M, w) φ'
⊢ φ' ∈ X ∪ {~~φ}
Tactic:
aesop
State after:
no goals

State before:
case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' = φ
⊢ Evaluate (M, w) φ'
Tactic:
specialize satX (~~φ)
State after:
case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' = φ
satX : ~~φ ∈ X ∪ {~~φ} → Evaluate (M, w) (~~φ)
⊢ Evaluate (M, w) φ'

State before:
case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' = φ
satX : ~~φ ∈ X ∪ {~~φ} → Evaluate (M, w) (~~φ)
⊢ Evaluate (M, w) φ'
Tactic:
aesop
State after:
no goals

State before:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
Tactic:
intro φ' is_in
State after:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∪ {~~φ}
⊢ Evaluate (M, w) φ'

State before:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∪ {~~φ}
⊢ Evaluate (M, w) φ'
Tactic:
simp at is_in
State after:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∨ φ' = ~~φ
⊢ Evaluate (M, w) φ'

State before:
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
is_in : φ' ∈ X ∨ φ' = ~~φ
⊢ Evaluate (M, w) φ'
Tactic:
cases is_in
State after:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' ∈ X
⊢ Evaluate (M, w) φ'

case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' = ~~φ
⊢ Evaluate (M, w) φ'

State before:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' ∈ X
⊢ Evaluate (M, w) φ'
Tactic:
specialize satX φ'
State after:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {φ} → Evaluate (M, w) φ'
⊢ Evaluate (M, w) φ'

State before:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {φ} → Evaluate (M, w) φ'
⊢ Evaluate (M, w) φ'
Tactic:
apply satX
State after:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {φ} → Evaluate (M, w) φ'
⊢ φ' ∈ X ∪ {φ}

State before:
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {φ} → Evaluate (M, w) φ'
⊢ φ' ∈ X ∪ {φ}
Tactic:
aesop
State after:
no goals

State before:
case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
φ' : Formula
h✝ : φ' = ~~φ
⊢ Evaluate (M, w) φ'
Tactic:
specialize satX φ
State after:
case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' = ~~φ
satX : φ ∈ X ∪ {φ} → Evaluate (M, w) φ
⊢ Evaluate (M, w) φ'

State before:
case h.inr
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' = ~~φ
satX : φ ∈ X ∪ {φ} → Evaluate (M, w) φ
⊢ Evaluate (M, w) φ'
Tactic:
aesop
State after:
no goals