Theorem: Sat.unsat_of_limplies_and_incompatible (LeanSAT/Sat/Basic.lean)

State before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ limplies α f1 f2 → incompatible α f1 f2 → unsatisfiable α f1
Tactic:
intro h1 h2 p pf1
State after:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
⊢ False

State before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
⊢ False
Tactic:
cases h2 p
State after:
case inl
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f1)
⊢ False

case inr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f2)
⊢ False

State before:
case inl
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f1)
⊢ False

case inr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f2)
⊢ False
Tactic:
. next h2 =>
  exact h2 pf1
State after:
case inr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f2)
⊢ False

State before:
case inr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f2)
⊢ False
Tactic:
. next h2 =>
  exact h2 $ h1 p pf1
State after:
no goals

State before:
case inl
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f1)
⊢ False
Tactic:
next h2 =>
exact h2 pf1
State after:
no goals

State before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2✝ : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h2 : ¬(p ⊨ f1)
⊢ False
Tactic:
exact h2 pf1
State after:
no goals

State before:
case inr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2 : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h✝ : ¬(p ⊨ f2)
⊢ False
Tactic:
next h2 =>
exact h2 $ h1 p pf1
State after:
no goals

State before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h1 : limplies α f1 f2
h2✝ : incompatible α f1 f2
p : α → Bool
pf1 : p ⊨ f1
h2 : ¬(p ⊨ f2)
⊢ False
Tactic:
exact h2 $ h1 p pf1
State after:
no goals