Theorem: LinearLT.not_eq_iff_lt_or_gt (Algdata/Init/LawfulLT.lean)

State before:
α : Type u_1
inst✝ : LinearLT α
a b : α
hor : a < b ∨ a > b
⊢ a ≠ b
Tactic:
intro heq
State after:
α : Type u_1
inst✝ : LinearLT α
a b : α
hor : a < b ∨ a > b
heq : a = b
⊢ False

State before:
α : Type u_1
inst✝ : LinearLT α
a b : α
hor : a < b ∨ a > b
heq : a = b
⊢ False
Tactic:
cases heq
State after:
case refl
α : Type u_1
inst✝ : LinearLT α
a : α
hor : a < a ∨ a > a
⊢ False

State before:
case refl
α : Type u_1
inst✝ : LinearLT α
a : α
hor : a < a ∨ a > a
⊢ False
Tactic:
cases hor
State after:
case refl.inl
α : Type u_1
inst✝ : LinearLT α
a : α
h✝ : a < a
⊢ False

case refl.inr
α : Type u_1
inst✝ : LinearLT α
a : α
h✝ : a > a
⊢ False

State before:
α : Type u_1
inst✝ : LinearLT α
a : α
h : a < a
⊢ False
Tactic:
case inl h => exact LinearLT.toLawfulLT.irrefl _ h
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearLT α
a : α
h : a > a
⊢ False
Tactic:
case inr h => exact LinearLT.toLawfulLT.irrefl _ h
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearLT α
a : α
h : a < a
⊢ False
Tactic:
exact LinearLT.toLawfulLT.irrefl _ h
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearLT α
a : α
h : a > a
⊢ False
Tactic:
exact LinearLT.toLawfulLT.irrefl _ h
State after:
no goals