-- Mathlib/SetTheory/Nimber/Basic.lean
theorem add_trichotomy {a b c : Nimber} (h : a + b + c ≠ 0) :
    b + c < a ∨ c + a < b ∨ a + b < c

Proof state:
case inr.intro.intro
a b c : Nimber
h : 0 < a + b + c
x : Nimber
hx : a + b < c
hx' : a + b = x
⊢ b + c < a ∨ c + a < b ∨ a + b < c

Tactic:
exact Or.inr <| Or.inr hx

Result:
no goals

Proof state:
case inl.intro.intro.inl.intro.intro
a b c : Nimber
h : 0 < a + b + c
x✝ : Nimber
hx✝ : x✝ < a + b
hx'✝ : x✝ = c
x : Nimber
hx : x < a
hx' : x + b = c
⊢ b + c < a ∨ c + a < b ∨ a + b < c

Tactic:
rw [← hx', add_comm, add_cancel_right]

Result:
case inl.intro.intro.inl.intro.intro
a b c : Nimber
h : 0 < a + b + c
x✝ : Nimber
hx✝ : x✝ < a + b
hx'✝ : x✝ = c
x : Nimber
hx : x < a
hx' : x + b = c
⊢ x < a ∨ x + b + a < b ∨ a + b < x + b

Proof state:
case inl.intro.intro.inr.intro.intro
a b c : Nimber
h : 0 < a + b + c
x✝ : Nimber
hx✝ : x✝ < a + b
hx'✝ : x✝ = c
x : Nimber
hx : x < b
hx' : a + x = c
⊢ b + (x + a) < a ∨ x < b ∨ a + b < x + a

Tactic:
exact Or.inr <| Or.inl hx

Result:
no goals

Proof state:
case inr.intro.intro
a b c : Nimber
h : 0 < a + b + c
x : Nimber
hx : x < c
hx' : a + b = x
⊢ b + c < a ∨ c + a < b ∨ a + b < c

Tactic:
rw [← hx'] at hx

Result:
case inr.intro.intro
a b c : Nimber
h : 0 < a + b + c
x : Nimber
hx : a + b < c
hx' : a + b = x
⊢ b + c < a ∨ c + a < b ∨ a + b < c

Proof state:
case inl.intro.intro.inr.intro.intro
a b c : Nimber
h : 0 < a + b + c
x✝ : Nimber
hx✝ : x✝ < a + b
hx'✝ : x✝ = c
x : Nimber
hx : x < b
hx' : a + x = c
⊢ b + c < a ∨ c + a < b ∨ a + b < c

Tactic:
rw [← hx', add_comm a, add_cancel_right]

Result:
case inl.intro.intro.inr.intro.intro
a b c : Nimber
h : 0 < a + b + c
x✝ : Nimber
hx✝ : x✝ < a + b
hx'✝ : x✝ = c
x : Nimber
hx : x < b
hx' : a + x = c
⊢ b + (x + a) < a ∨ x < b ∨ a + b < x + a

Proof state:
case inl.intro.intro
a b c : Nimber
h : 0 < a + b + c
x : Nimber
hx : x < a + b
hx' : x = c
⊢ b + c < a ∨ c + a < b ∨ a + b < c

Tactic:
obtain ⟨x, hx, hx'⟩ | ⟨x, hx, hx'⟩ := exists_of_lt_add (hx' ▸ hx)

Result:
case inl.intro.intro.inl.intro.intro
a b c : Nimber
h : 0 < a + b + c
x✝ : Nimber
hx✝ : x✝ < a + b
hx'✝ : x✝ = c
x : Nimber
hx : x < a
hx' : x + b = c
⊢ b + c < a ∨ c + a < b ∨ a + b < c

case inl.intro.intro.inr.intro.intro
a b c : Nimber
h : 0 < a + b + c
x✝ : Nimber
hx✝ : x✝ < a + b
hx'✝ : x✝ = c
x : Nimber
hx : x < b
hx' : a + x = c
⊢ b + c < a ∨ c + a < b ∨ a + b < c

Proof state:
a b c : Nimber
h : 0 < a + b + c
⊢ b + c < a ∨ c + a < b ∨ a + b < c

Tactic:
obtain ⟨x, hx, hx'⟩ | ⟨x, hx, hx'⟩ := exists_of_lt_add h <;>
rw [add_eq_zero] at hx'

Result:
case inl.intro.intro
a b c : Nimber
h : 0 < a + b + c
x : Nimber
hx : x < a + b
hx' : x = c
⊢ b + c < a ∨ c + a < b ∨ a + b < c

case inr.intro.intro
a b c : Nimber
h : 0 < a + b + c
x : Nimber
hx : x < c
hx' : a + b = x
⊢ b + c < a ∨ c + a < b ∨ a + b < c

Proof state:
a b c : Nimber
h : a + b + c ≠ 0
⊢ b + c < a ∨ c + a < b ∨ a + b < c

Tactic:
rw [← Nimber.pos_iff_ne_zero] at h

Result:
a b c : Nimber
h : 0 < a + b + c
⊢ b + c < a ∨ c + a < b ∨ a + b < c

Proof state:
case inl.intro.intro.inl.intro.intro
a b c : Nimber
h : 0 < a + b + c
x✝ : Nimber
hx✝ : x✝ < a + b
hx'✝ : x✝ = c
x : Nimber
hx : x < a
hx' : x + b = c
⊢ x < a ∨ x + b + a < b ∨ a + b < x + b

Tactic:
exact Or.inl hx

Result:
no goals