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

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
p : Bool
⊢ polarity (mkLit L x p) = p
Tactic:
dsimp [mkLit]
State after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
p : Bool
⊢ polarity (if p = true then mkPos x else mkNeg x) = p

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
p : Bool
⊢ polarity (if p = true then mkPos x else mkNeg x) = p
Tactic:
split <;> simp_all
State after:
no goals