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

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

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

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

case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ unsatisfiable α f2 → unsatisfiable α f1
Tactic:
. intros f1_unsat p p_entails_f2
  rw [← h p] at p_entails_f2
  exact f1_unsat p p_entails_f2
State after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ unsatisfiable α f2 → unsatisfiable α f1

State before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ unsatisfiable α f2 → unsatisfiable α f1
Tactic:
. intros f2_unsat p p_entails_f1
  rw [h p] at p_entails_f1
  exact f2_unsat p p_entails_f1
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
h : liff α f1 f2
⊢ unsatisfiable α f1 → unsatisfiable α f2
Tactic:
intros f1_unsat p p_entails_f2
State after:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f1_unsat : unsatisfiable α f1
p : α → Bool
p_entails_f2 : p ⊨ f2
⊢ False

State before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f1_unsat : unsatisfiable α f1
p : α → Bool
p_entails_f2 : p ⊨ f2
⊢ False
Tactic:
rw [← h p] at p_entails_f2
State after:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f1_unsat : unsatisfiable α f1
p : α → Bool
p_entails_f2 : p ⊨ f1
⊢ False

State before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f1_unsat : unsatisfiable α f1
p : α → Bool
p_entails_f2 : p ⊨ f1
⊢ False
Tactic:
exact f1_unsat p p_entails_f2
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
h : liff α f1 f2
⊢ unsatisfiable α f2 → unsatisfiable α f1
Tactic:
intros f2_unsat p p_entails_f1
State after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f2_unsat : unsatisfiable α f2
p : α → Bool
p_entails_f1 : p ⊨ f1
⊢ False

State before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f2_unsat : unsatisfiable α f2
p : α → Bool
p_entails_f1 : p ⊨ f1
⊢ False
Tactic:
rw [h p] at p_entails_f1
State after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f2_unsat : unsatisfiable α f2
p : α → Bool
p_entails_f1 : p ⊨ f2
⊢ False

State before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
f2_unsat : unsatisfiable α f2
p : α → Bool
p_entails_f1 : p ⊨ f2
⊢ False
Tactic:
exact f2_unsat p p_entails_f1
State after:
no goals