Theorem: LeanSAT.LitVar.toPropFun.inj (LeanSAT/Data/Cnf.lean)

State before:
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
⊢ Function.Injective toPropFun
Tactic:
intro l1 l2 h
State after:
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
h : toPropFun l1 = toPropFun l2
⊢ l1 = l2

State before:
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
h : toPropFun l1 = toPropFun l2
⊢ l1 = l2
Tactic:
simp [toPropFun] at h
State after:
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
h :
  (if polarity l1 = true then var (toVar l1) else (var (toVar l1))ᶜ) =
    if polarity l2 = true then var (toVar l2) else (var (toVar l2))ᶜ
⊢ l1 = l2

State before:
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
h :
  (if polarity l1 = true then var (toVar l1) else (var (toVar l1))ᶜ) =
    if polarity l2 = true then var (toVar l2) else (var (toVar l2))ᶜ
⊢ l1 = l2
Tactic:
apply LawfulLitVar.ext <;> aesop
State after:
no goals