-- Mathlib/SetTheory/Nimber/Basic.lean
theorem add_assoc (a b c : Nimber) : a + b + c = a + (b + c)

Proof state:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ y ≠ b

case a.h₂
a b c x : Nimber
hx : x < c
⊢ a + b + x ≠ a + (b + c)

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x + (b + c) ≠ a + b + c

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ a + (y + c) ≠ a + b + c

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Tactic:
on_goal 3 => rw [Nimber.add_assoc _ _ x, add_ne_add_right, add_ne_add_right]

Result:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ y ≠ b

case a.h₂
a b c x : Nimber
hx : x < c
⊢ x ≠ c

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x + (b + c) ≠ a + b + c

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ a + (y + c) ≠ a + b + c

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Proof state:
case a.h₂.inr.intro.intro.h
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ y < c

Tactic:
assumption

Result:
no goals

Proof state:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ y ≠ b

case a.h₂
a b c x : Nimber
hx : x < c
⊢ x ≠ c

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x ≠ a

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ y ≠ b

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Tactic:
on_goal 6 => rw [← Nimber.add_assoc _ _ y, add_ne_add_right]

Result:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ y ≠ b

case a.h₂
a b c x : Nimber
hx : x < c
⊢ x ≠ c

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x ≠ a

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ y ≠ b

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ y ≠ c

Proof state:
case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Tactic:
rw [← Nimber.add_assoc _ _ y, add_ne_add_right]

Result:
case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ y ≠ c

Proof state:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ y ≠ b

case a.h₂
a b c x : Nimber
hx : x < c
⊢ x ≠ c

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x ≠ a

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ a + (y + c) ≠ a + b + c

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Tactic:
on_goal 5 => rw [← Nimber.add_assoc _ y, add_ne_add_left, add_ne_add_right]

Result:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ y ≠ b

case a.h₂
a b c x : Nimber
hx : x < c
⊢ x ≠ c

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x ≠ a

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ y ≠ b

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Proof state:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ y ≠ b

case a.h₂
a b c x : Nimber
hx : x < c
⊢ x ≠ c

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x ≠ a

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ y ≠ b

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ y ≠ c

Tactic:
all_goals apply ne_of_lt; assumption

Result:
no goals

Proof state:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y + b + c ≠ a + (b + c)

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ a + y + c ≠ a + (b + c)

case a.h₂
a b c x : Nimber
hx : x < c
⊢ a + b + x ≠ a + (b + c)

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x + (b + c) ≠ a + b + c

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ a + (y + c) ≠ a + b + c

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Tactic:
on_goal 1 => rw [Nimber.add_assoc y, add_ne_add_left]

Result:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ a + y + c ≠ a + (b + c)

case a.h₂
a b c x : Nimber
hx : x < c
⊢ a + b + x ≠ a + (b + c)

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x + (b + c) ≠ a + b + c

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ a + (y + c) ≠ a + b + c

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Proof state:
case a.h₂
a b c x : Nimber
hx : x < b + c
⊢ a + x ≠ a + b + c

Tactic:
obtain ⟨y, hy, rfl⟩ | ⟨y, hy, rfl⟩ := exists_of_lt_add hx

Result:
case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ a + (y + c) ≠ a + b + c

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Proof state:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ y ≠ b

case a.h₂
a b c x : Nimber
hx : x < c
⊢ x ≠ c

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x + (b + c) ≠ a + b + c

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ a + (y + c) ≠ a + b + c

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Tactic:
on_goal 4 => rw [← Nimber.add_assoc x, add_ne_add_left, add_ne_add_left]

Result:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ y ≠ b

case a.h₂
a b c x : Nimber
hx : x < c
⊢ x ≠ c

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x ≠ a

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ a + (y + c) ≠ a + b + c

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Proof state:
a b c : Nimber
⊢ a + b + c = a + (b + c)

Tactic:
apply le_antisymm <;>
  apply add_le_of_forall_ne <;>
  intro x hx <;>
  try obtain ⟨y, hy, rfl⟩ | ⟨y, hy, rfl⟩ := exists_of_lt_add hx

Result:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y + b + c ≠ a + (b + c)

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ a + y + c ≠ a + (b + c)

case a.h₂
a b c x : Nimber
hx : x < c
⊢ a + b + x ≠ a + (b + c)

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x + (b + c) ≠ a + b + c

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ a + (y + c) ≠ a + b + c

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Proof state:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y + b + c ≠ a + (b + c)

Tactic:
rw [Nimber.add_assoc y, add_ne_add_left]

Result:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

Proof state:
case a.h₁
a b c x : Nimber
hx : x < a
⊢ x + (b + c) ≠ a + b + c

Tactic:
rw [← Nimber.add_assoc x, add_ne_add_left, add_ne_add_left]

Result:
case a.h₁
a b c x : Nimber
hx : x < a
⊢ x ≠ a

Proof state:
case a.h₂
a b c x : Nimber
hx : x < c
⊢ a + b + x ≠ a + (b + c)

Tactic:
rw [Nimber.add_assoc _ _ x, add_ne_add_right, add_ne_add_right]

Result:
case a.h₂
a b c x : Nimber
hx : x < c
⊢ x ≠ c