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

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ l = mkPos (toVar l) ∨ l = mkNeg (toVar l)
Tactic:
rw [← eta l]
State after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) (polarity l) = mkPos (toVar (mkLit L (toVar l) (polarity l))) ∨
    mkLit L (toVar l) (polarity l) = mkNeg (toVar (mkLit L (toVar l) (polarity l)))

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) (polarity l) = mkPos (toVar (mkLit L (toVar l) (polarity l))) ∨
    mkLit L (toVar l) (polarity l) = mkNeg (toVar (mkLit L (toVar l) (polarity l)))
Tactic:
cases polarity l
State after:
case false
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) false = mkPos (toVar (mkLit L (toVar l) false)) ∨
    mkLit L (toVar l) false = mkNeg (toVar (mkLit L (toVar l) false))

case true
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true)) ∨
    mkLit L (toVar l) true = mkNeg (toVar (mkLit L (toVar l) true))

State before:
case false
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) false = mkPos (toVar (mkLit L (toVar l) false)) ∨
    mkLit L (toVar l) false = mkNeg (toVar (mkLit L (toVar l) false))

case true
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true)) ∨
    mkLit L (toVar l) true = mkNeg (toVar (mkLit L (toVar l) true))
Tactic:
. apply Or.inr
  simp [mkLit]
State after:
case true
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true)) ∨
    mkLit L (toVar l) true = mkNeg (toVar (mkLit L (toVar l) true))

State before:
case true
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true)) ∨
    mkLit L (toVar l) true = mkNeg (toVar (mkLit L (toVar l) true))
Tactic:
. apply Or.inl
  simp [mkLit]
State after:
no goals

State before:
case false
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) false = mkPos (toVar (mkLit L (toVar l) false)) ∨
    mkLit L (toVar l) false = mkNeg (toVar (mkLit L (toVar l) false))
Tactic:
apply Or.inr
State after:
case false.h
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) false = mkNeg (toVar (mkLit L (toVar l) false))

State before:
case false.h
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) false = mkNeg (toVar (mkLit L (toVar l) false))
Tactic:
simp [mkLit]
State after:
no goals

State before:
case true
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true)) ∨
    mkLit L (toVar l) true = mkNeg (toVar (mkLit L (toVar l) true))
Tactic:
apply Or.inl
State after:
case true.h
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true))

State before:
case true.h
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true))
Tactic:
simp [mkLit]
State after:
no goals