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

State before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ liff α f1 f2 ↔ limplies α f1 f2 ∧ limplies α 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
⊢ liff α f1 f2 → limplies α f1 f2 ∧ limplies α f2 f1

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

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

case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ limplies α f1 f2 ∧ limplies α f2 f1 → liff α f1 f2
Tactic:
. intro h
  constructor
  . intro p
    rw [h p]
    exact id
  . intro p
    rw [h p]
    exact id
State after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ limplies α f1 f2 ∧ limplies α f2 f1 → liff α f1 f2

State before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ limplies α f1 f2 ∧ limplies α f2 f1 → liff α f1 f2
Tactic:
. intros h p
  constructor
  . exact h.1 p
  . exact h.2 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
⊢ liff α f1 f2 → limplies α f1 f2 ∧ limplies α f2 f1
Tactic:
intro h
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
⊢ limplies α f1 f2 ∧ limplies α f2 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
⊢ limplies α f1 f2 ∧ limplies α f2 f1
Tactic:
constructor
State after:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f1 f2

case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f2 f1

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

case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f2 f1
Tactic:
. intro p
  rw [h p]
  exact id
State after:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f2 f1

State before:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f2 f1
Tactic:
. intro p
  rw [h p]
  exact id
State after:
no goals

State before:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f1 f2
Tactic:
intro p
State after:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f1 → p ⊨ f2

State before:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f1 → p ⊨ f2
Tactic:
rw [h p]
State after:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f2

State before:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f2
Tactic:
exact id
State after:
no goals

State before:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f2 f1
Tactic:
intro p
State after:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1

State before:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1
Tactic:
rw [h p]
State after:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f2

State before:
case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f2
Tactic:
exact id
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
⊢ limplies α f1 f2 ∧ limplies α f2 f1 → liff α f1 f2
Tactic:
intros 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 : limplies α f1 f2 ∧ limplies α 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 : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f1 ↔ p ⊨ f2
Tactic:
constructor
State after:
case mpr.mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f1 → p ⊨ f2

case mpr.mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1

State before:
case mpr.mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f1 → p ⊨ f2

case mpr.mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1
Tactic:
. exact h.1 p
State after:
case mpr.mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1

State before:
case mpr.mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1
Tactic:
. exact h.2 p
State after:
no goals

State before:
case mpr.mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f1 → p ⊨ f2
Tactic:
exact h.1 p
State after:
no goals

State before:
case mpr.mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f1 f2 ∧ limplies α f2 f1
p : α → Bool
⊢ p ⊨ f2 → p ⊨ f1
Tactic:
exact h.2 p
State after:
no goals