Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq (LeanSAT/Data/ICnf.lean)

State before:
l₁ l₂ : ILit
⊢ ILit.index l₁ = ILit.index l₂ ↔ l₁ = l₂ ∨ negate l₁ = l₂
Tactic:
constructor
State after:
case mp
l₁ l₂ : ILit
⊢ ILit.index l₁ = ILit.index l₂ → l₁ = l₂ ∨ negate l₁ = l₂

case mpr
l₁ l₂ : ILit
⊢ l₁ = l₂ ∨ negate l₁ = l₂ → ILit.index l₁ = ILit.index l₂

State before:
case mp
l₁ l₂ : ILit
⊢ ILit.index l₁ = ILit.index l₂ → l₁ = l₂ ∨ negate l₁ = l₂
Tactic:
intro hlit
State after:
case mp
l₁ l₂ : ILit
hlit : ILit.index l₁ = ILit.index l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂

State before:
case mp
l₁ l₂ : ILit
hlit : ILit.index l₁ = ILit.index l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂
Tactic:
simp at hlit
State after:
case mp
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂

State before:
case mp
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂
Tactic:
by_cases hpol : polarity l₁ = polarity l₂
State after:
case pos
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂

case neg
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂

State before:
case pos
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂
Tactic:
left
State after:
case pos.h
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ l₁ = l₂

State before:
case pos.h
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ l₁ = l₂
Tactic:
ext
State after:
case pos.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ toVar l₁ = toVar l₂

case pos.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ polarity l₁ = polarity l₂

State before:
case pos.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ toVar l₁ = toVar l₂
Tactic:
exact hlit
State after:
no goals

State before:
case pos.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ polarity l₁ = polarity l₂
Tactic:
exact hpol
State after:
no goals

State before:
case neg
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂
Tactic:
right
State after:
case neg.h
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ negate l₁ = l₂

State before:
case neg.h
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ negate l₁ = l₂
Tactic:
ext
State after:
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ toVar (negate l₁) = toVar l₂

case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ polarity (negate l₁) = polarity l₂

State before:
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ toVar (negate l₁) = toVar l₂
Tactic:
simpa
State after:
no goals

State before:
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ polarity (negate l₁) = polarity l₂
Tactic:
rw [← Bool.bnot_eq] at hpol
State after:
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : (!polarity l₁) = polarity l₂
⊢ polarity (negate l₁) = polarity l₂

State before:
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : (!polarity l₁) = polarity l₂
⊢ polarity (negate l₁) = polarity l₂
Tactic:
simp [hpol]
State after:
no goals

State before:
case mpr
l₁ l₂ : ILit
⊢ l₁ = l₂ ∨ negate l₁ = l₂ → ILit.index l₁ = ILit.index l₂
Tactic:
rintro (rfl | rfl)
State after:
case mpr.inl
l₁ : ILit
⊢ ILit.index l₁ = ILit.index l₁

case mpr.inr
l₁ : ILit
⊢ ILit.index l₁ = ILit.index (negate l₁)

State before:
case mpr.inl
l₁ : ILit
⊢ ILit.index l₁ = ILit.index l₁
Tactic:
rfl
State after:
no goals

State before:
case mpr.inr
l₁ : ILit
⊢ ILit.index l₁ = ILit.index (negate l₁)
Tactic:
simp
State after:
no goals