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

State before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ¬a < b → a = b ∨ a > b
Tactic:
apply trichot_cases (r:=LT.lt) (motive:=λ a b => ¬ a < b → a=b ∨ a > b)
State after:
case of_rfl
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a : α), ¬a < a → a = a ∨ a > a

case of_rel
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a b : α), a < b → ¬a < b → a = b ∨ a > b

case of_opp
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a b : α), b < a → ¬a < b → a = b ∨ a > b

State before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a : α), ¬a < a → a = a ∨ a > a
Tactic:
case of_rfl => exact λ _ _ => Or.inl rfl
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a b : α), a < b → ¬a < b → a = b ∨ a > b
Tactic:
case of_rel => exact λ _ _ => absurd
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a b : α), b < a → ¬a < b → a = b ∨ a > b
Tactic:
case of_opp => exact λ _ _ h _ => Or.inr h
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a : α), ¬a < a → a = a ∨ a > a
Tactic:
exact λ _ _ => Or.inl rfl
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a b : α), a < b → ¬a < b → a = b ∨ a > b
Tactic:
exact λ _ _ => absurd
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearLT α
a b : α
⊢ ∀ (a b : α), b < a → ¬a < b → a = b ∨ a > b
Tactic:
exact λ _ _ h _ => Or.inr h
State after:
no goals

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

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

case inr
α : Type u_1
inst✝ : LinearLT α
a b : α
hlt : a < b
h✝ : a > b
⊢ False

State before:
α : Type u_1
inst✝ : LinearLT α
a b : α
hlt : a < b
heq : a = b
⊢ False
Tactic:
case inl heq => cases heq; exact Irreflective.irrefl _ hlt
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearLT α
a b : α
hlt : a < b
hgt : a > b
⊢ False
Tactic:
case inr hgt => exact Asymmetry.asymm _ _ hlt hgt
State after:
no goals

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

State before:
case refl
α : Type u_1
inst✝ : LinearLT α
a : α
hlt : a < a
⊢ False
Tactic:
exact Irreflective.irrefl _ hlt
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearLT α
a b : α
hlt : a < b
hgt : a > b
⊢ False
Tactic:
exact Asymmetry.asymm _ _ hlt hgt
State after:
no goals