Theorem: Sat.incompatible.symm (LeanSAT/Sat/Basic.lean)

State before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f1 f2 ↔ incompatible α f2 f1
Tactic:
constructor
State after:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f1 f2 → incompatible α f2 f1

case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f2 f1 → incompatible α f1 f2

State before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f1 f2 → incompatible α f2 f1

case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f2 f1 → incompatible α f1 f2
Tactic:
. intro h p
  exact Or.symm $ h p
State after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f2 f1 → incompatible α f1 f2

State before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f2 f1 → incompatible α f1 f2
Tactic:
. intro h p
  exact Or.symm $ h p
State after:
no goals

State before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f1 f2 → incompatible α f2 f1
Tactic:
intro h p
State after:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : incompatible α f1 f2
p : α → Bool
⊢ ¬(p ⊨ f2) ∨ ¬(p ⊨ f1)

State before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : incompatible α f1 f2
p : α → Bool
⊢ ¬(p ⊨ f2) ∨ ¬(p ⊨ f1)
Tactic:
exact Or.symm $ h p
State after:
no goals

State before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ incompatible α f2 f1 → incompatible α f1 f2
Tactic:
intro h p
State after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : incompatible α f2 f1
p : α → Bool
⊢ ¬(p ⊨ f1) ∨ ¬(p ⊨ f2)

State before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : incompatible α f2 f1
p : α → Bool
⊢ ¬(p ⊨ f1) ∨ ¬(p ⊨ f2)
Tactic:
exact Or.symm $ h p
State after:
no goals