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

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

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

State before:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ l1 = l2 → toVar l1 = toVar l2 ∧ polarity l1 = polarity l2
Tactic:
rintro rfl
State after:
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 : L
⊢ toVar l1 = toVar l1 ∧ polarity l1 = polarity l1

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

State before:
case mpr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ toVar l1 = toVar l2 ∧ polarity l1 = polarity l2 → l1 = l2
Tactic:
aesop
State after:
no goals