Theorem: LawfulLT.eq_or_lt_trans (Algdata/Init/LawfulLT.lean)

State before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
⊢ a = b ∨ a < b → b = c ∨ b < c → a = c ∨ a < c
Tactic:
intro hab hbc
State after:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a = b ∨ a < b
hbc : b = c ∨ b < c
⊢ a = c ∨ a < c

State before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a = b ∨ a < b
hbc : b = c ∨ b < c
⊢ a = c ∨ a < c
Tactic:
cases hab
State after:
case inl
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
h✝ : a = b
⊢ a = c ∨ a < c

case inr
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
h✝ : a < b
⊢ a = c ∨ a < c

State before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haeqb : a = b
⊢ a = c ∨ a < c
Tactic:
case inl haeqb => cases haeqb; exact hbc
State after:
no goals

State before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haltb : a < b
⊢ a = c ∨ a < c
Tactic:
case inr haltb =>
  apply Or.inr
  cases hbc
  case inl hbeqc => cases hbeqc; exact haltb
  case inr hbltc => exact trans haltb hbltc
State after:
no goals

State before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haeqb : a = b
⊢ a = c ∨ a < c
Tactic:
cases haeqb
State after:
case refl
α : Type u_1
inst✝ : LawfulLT α
a c : α
hbc : a = c ∨ a < c
⊢ a = c ∨ a < c

State before:
case refl
α : Type u_1
inst✝ : LawfulLT α
a c : α
hbc : a = c ∨ a < c
⊢ a = c ∨ a < c
Tactic:
exact hbc
State after:
no goals

State before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haltb : a < b
⊢ a = c ∨ a < c
Tactic:
apply Or.inr
State after:
case h
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haltb : a < b
⊢ a < c

State before:
case h
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haltb : a < b
⊢ a < c
Tactic:
cases hbc
State after:
case h.inl
α : Type u_1
inst✝ : LawfulLT α
a b c : α
haltb : a < b
h✝ : b = c
⊢ a < c

case h.inr
α : Type u_1
inst✝ : LawfulLT α
a b c : α
haltb : a < b
h✝ : b < c
⊢ a < c

State before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
haltb : a < b
hbeqc : b = c
⊢ a < c
Tactic:
case inl hbeqc => cases hbeqc; exact haltb
State after:
no goals

State before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
haltb : a < b
hbltc : b < c
⊢ a < c
Tactic:
case inr hbltc => exact trans haltb hbltc
State after:
no goals

State before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
haltb : a < b
hbeqc : b = c
⊢ a < c
Tactic:
cases hbeqc
State after:
case refl
α : Type u_1
inst✝ : LawfulLT α
a b : α
haltb : a < b
⊢ a < b

State before:
case refl
α : Type u_1
inst✝ : LawfulLT α
a b : α
haltb : a < b
⊢ a < b
Tactic:
exact haltb
State after:
no goals

State before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
haltb : a < b
hbltc : b < c
⊢ a < c
Tactic:
exact trans haltb hbltc
State after:
no goals