Theorem: LeanSAT.LitVar.neg_eq_neg (LeanSAT/Data/Cnf.lean)

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ -l1 = -l2 ↔ l1 = l2
Tactic:
constructor
State after:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ -l1 = -l2 → l1 = l2

case mpr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ l1 = l2 → -l1 = -l2

State before:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ -l1 = -l2 → l1 = l2
Tactic:
rw [ext_iff, ext_iff (L := L)]
State after:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ toVar (-l1) = toVar (-l2) ∧ polarity (-l1) = polarity (-l2) → toVar l1 = toVar l2 ∧ polarity l1 = polarity l2

State before:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ toVar (-l1) = toVar (-l2) ∧ polarity (-l1) = polarity (-l2) → toVar l1 = toVar l2 ∧ polarity l1 = polarity l2
Tactic:
simp
State after:
no goals

State before:
case mpr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ l1 = l2 → -l1 = -l2
Tactic:
rintro rfl
State after:
case mpr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 : L
⊢ -l1 = -l1

State before:
case mpr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 : L
⊢ -l1 = -l1
Tactic:
rfl
State after:
no goals