Theorem: LeanSAT.Model.PropFun.eq_bot_of_eqsat (LeanSAT/Model/PropFun.lean)

State before:
ν : Type u_1
F C : PropFun ν
⊢ eqsat F (F ⊓ C) → F ⊓ C = ⊥ → F = ⊥
Tactic:
rintro ⟨h₁, _⟩ hFC
State after:
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable (F ⊓ C)
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
⊢ F = ⊥

State before:
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable (F ⊓ C)
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
⊢ F = ⊥
Tactic:
rw [hFC] at h₁
State after:
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable ⊥
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
⊢ F = ⊥

State before:
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable ⊥
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
⊢ F = ⊥
Tactic:
have := mt h₁ bot_not_satisfiable
State after:
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable ⊥
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
this : ¬satisfiable F
⊢ F = ⊥

State before:
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable ⊥
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
this : ¬satisfiable F
⊢ F = ⊥
Tactic:
exact not_satisfiable_iff_eq_bot.mp (mt h₁ bot_not_satisfiable)
State after:
no goals