-- Mathlib/SetTheory/Nimber/Field.lean
theorem mul_assoc (a b c : Nimber) : a * b * c = a * (b * c)

Proof state:
case a.intro.intro.intro.intro
a b c x : Nimber
hx : x < a
b' : Nimber
hb : b' < b
c' : Nimber
hc : c' < c
hy : b' * c + b * c' + b' * c' < b * c
⊢ x * (b * c) + a * (b' * c + b * c' + b' * c') + x * (b' * c + b * c' + b' * c') ≠ a * b * c

Tactic:
have H : (a + x) * (b + b') * (c + c') ≠ 0 := by
  apply mul_ne_zero (mul_ne_zero _ _) <;> apply add_ne_zero_of_lt
  assumption'

Result:
case a.intro.intro.intro.intro
a b c x : Nimber
hx : x < a
b' : Nimber
hb : b' < b
c' : Nimber
hc : c' < c
hy : b' * c + b * c' + b' * c' < b * c
H : (a + x) * (b + b') * (c + c') ≠ 0
⊢ x * (b * c) + a * (b' * c + b * c' + b' * c') + x * (b' * c + b * c' + b' * c') ≠ a * b * c

Proof state:
case a.intro.intro.intro.intro
a b c y : Nimber
hy : y < c
a' : Nimber
ha : a' < a
b' : Nimber
hb : b' < b
hx : a' * b + a * b' + a' * b' < a * b
H :
  a * (b * c) +
      (a' * (b * c) +
        (a * (b' * c) + (a' * (b' * c) + (a * (b * y) + (a' * (b * y) + (a * (b' * y) + a' * (b' * y))))))) ≠
    0
⊢ ¬a * (b * c) +
        (a' * (b * c) +
          (a * (b' * c) + (a' * (b' * c) + (a * (b * y) + (a' * (b * y) + (a * (b' * y) + a' * (b' * y))))))) =
      2 • (a * (b * c))

Tactic:
simpa only [two_zsmul, zero_add] using H

Result:
no goals

Proof state:
case a.intro.intro.intro.intro
a b c y : Nimber
hy : y < c
a' : Nimber
ha : a' < a
b' : Nimber
hb : b' < b
hx : a' * b + a * b' + a' * b' < a * b
H :
  a * (b * c) + a' * (b * c) + (a * (b' * c) + a' * (b' * c)) +
      (a * (b * y) + a' * (b * y) + (a * (b' * y) + a' * (b' * y))) ≠
    0
⊢ a' * b * c + a * b' * c + a' * b' * c + a * b * y + (a' * b * y + a * b' * y + a' * b' * y) ≠ a * (b * c)

Tactic:
iterate 7 rw [Nimber.mul_assoc]

Result:
case a.intro.intro.intro.intro
a b c y : Nimber
hy : y < c
a' : Nimber
ha : a' < a
b' : Nimber
hb : b' < b
hx : a' * b + a * b' + a' * b' < a * b
H :
  a * (b * c) + a' * (b * c) + (a * (b' * c) + a' * (b' * c)) +
      (a * (b * y) + a' * (b * y) + (a * (b' * y) + a' * (b' * y))) ≠
    0
⊢ a' * (b * c) + a * (b' * c) + a' * (b' * c) + a * (b * y) + (a' * (b * y) + a * (b' * y) + a' * (b' * y)) ≠
    a * (b * c)

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

Tactic:
apply le_antisymm <;> refine mul_le_of_forall_ne fun x hx y hy ↦ ?_

Result:
case a
a b c x : Nimber
hx : x < a * b
y : Nimber
hy : y < c
⊢ x * c + a * b * y + x * y ≠ a * (b * c)

case a
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < b * c
⊢ x * (b * c) + a * y + x * y ≠ a * b * c

Proof state:
case a.intro.intro.intro.intro
a b c x : Nimber
hx : x < a
b' : Nimber
hb : b' < b
c' : Nimber
hc : c' < c
hy : b' * c + b * c' + b' * c' < b * c
H : a * b * c + x * b * c + (a * b' * c + x * b' * c) + (a * b * c' + x * b * c' + (a * b' * c' + x * b' * c')) ≠ 0
⊢ x * b * c + (a * b' * c + a * b * c' + a * b' * c') + (x * b' * c + x * b * c' + x * b' * c') + a * b * c ≠
    a * b * c + a * b * c

Tactic:
abel_nf at H ⊢

Result:
case a.intro.intro.intro.intro
a b c x : Nimber
hx : x < a
b' : Nimber
hb : b' < b
c' : Nimber
hc : c' < c
hy : b' * c + b * c' + b' * c' < b * c
H :
  a * b * c + (x * b * c + (a * b' * c + (x * b' * c + (a * b * c' + (x * b * c' + (a * b' * c' + x * b' * c')))))) ≠ 0
⊢ ¬a * b * c + (x * b * c + (a * b' * c + (x * b' * c + (a * b * c' + (x * b * c' + (a * b' * c' + x * b' * c')))))) =
      2 • (a * b * c)

Proof state:
case a.intro.intro.intro.intro
a b c y : Nimber
hy : y < c
a' : Nimber
ha : a' < a
b' : Nimber
hb : b' < b
hx : a' * b + a * b' + a' * b' < a * b
H : (a + a') * ((b + b') * (c + y)) ≠ 0
⊢ (a' * b + a * b' + a' * b') * c + a * b * y + (a' * b + a * b' + a' * b') * y ≠ a * (b * c)

Tactic:
simp only [Nimber.add_mul, Nimber.mul_add] at H ⊢

Result:
case a.intro.intro.intro.intro
a b c y : Nimber
hy : y < c
a' : Nimber
ha : a' < a
b' : Nimber
hb : b' < b
hx : a' * b + a * b' + a' * b' < a * b
H :
  a * (b * c) + a' * (b * c) + (a * (b' * c) + a' * (b' * c)) +
      (a * (b * y) + a' * (b * y) + (a * (b' * y) + a' * (b' * y))) ≠
    0
⊢ a' * b * c + a * b' * c + a' * b' * c + a * b * y + (a' * b * y + a * b' * y + a' * b' * y) ≠ a * (b * c)

Proof state:
case a.intro.intro.intro.intro
a b c y : Nimber
hy : y < c
a' : Nimber
ha : a' < a
b' : Nimber
hb : b' < b
hx : a' * b + a * b' + a' * b' < a * b
⊢ (a' * b + a * b' + a' * b') * c + a * b * y + (a' * b + a * b' + a' * b') * y ≠ a * (b * c)

Tactic:
have H : (a + a') * ((b + b') * (c + y)) ≠ 0 := by
  apply mul_ne_zero _ (mul_ne_zero _ _) <;> apply add_ne_zero_of_lt
  assumption'

Result:
case a.intro.intro.intro.intro
a b c y : Nimber
hy : y < c
a' : Nimber
ha : a' < a
b' : Nimber
hb : b' < b
hx : a' * b + a * b' + a' * b' < a * b
H : (a + a') * ((b + b') * (c + y)) ≠ 0
⊢ (a' * b + a * b' + a' * b') * c + a * b * y + (a' * b + a * b' + a' * b') * y ≠ a * (b * c)

Proof state:
case a.intro.intro.intro.intro
a b c x : Nimber
hx : x < a
b' : Nimber
hb : b' < b
c' : Nimber
hc : c' < c
hy : b' * c + b * c' + b' * c' < b * c
H : (a + x) * (b + b') * (c + c') ≠ 0
⊢ x * (b * c) + a * (b' * c + b * c' + b' * c') + x * (b' * c + b * c' + b' * c') ≠ a * b * c

Tactic:
simp only [Nimber.add_mul, Nimber.mul_add] at H ⊢

Result:
case a.intro.intro.intro.intro
a b c x : Nimber
hx : x < a
b' : Nimber
hb : b' < b
c' : Nimber
hc : c' < c
hy : b' * c + b * c' + b' * c' < b * c
H : a * b * c + x * b * c + (a * b' * c + x * b' * c) + (a * b * c' + x * b * c' + (a * b' * c' + x * b' * c')) ≠ 0
⊢ x * (b * c) + (a * (b' * c) + a * (b * c') + a * (b' * c')) + (x * (b' * c) + x * (b * c') + x * (b' * c')) ≠
    a * b * c

Proof state:
case a.intro.intro.intro.intro
a b c y : Nimber
hy : y < c
a' : Nimber
ha : a' < a
b' : Nimber
hb : b' < b
hx : a' * b + a * b' + a' * b' < a * b
H :
  a * (b * c) + a' * (b * c) + (a * (b' * c) + a' * (b' * c)) +
      (a * (b * y) + a' * (b * y) + (a * (b' * y) + a' * (b' * y))) ≠
    0
⊢ a' * (b * c) + a * (b' * c) + a' * (b' * c) + a * (b * y) + (a' * (b * y) + a * (b' * y) + a' * (b' * y)) ≠
    a * (b * c)

Tactic:
rw [← add_ne_add_left (a * (b * c))]

Result:
case a.intro.intro.intro.intro
a b c y : Nimber
hy : y < c
a' : Nimber
ha : a' < a
b' : Nimber
hb : b' < b
hx : a' * b + a * b' + a' * b' < a * b
H :
  a * (b * c) + a' * (b * c) + (a * (b' * c) + a' * (b' * c)) +
      (a * (b * y) + a' * (b * y) + (a * (b' * y) + a' * (b' * y))) ≠
    0
⊢ a' * (b * c) + a * (b' * c) + a' * (b' * c) + a * (b * y) + (a' * (b * y) + a * (b' * y) + a' * (b' * y)) +
      a * (b * c) ≠
    a * (b * c) + a * (b * c)

Proof state:
a b c x : Nimber
hx : x < a
b' : Nimber
hb : b' < b
c' : Nimber
hc : c' < c
hy : b' * c + b * c' + b' * c' < b * c
⊢ (a + x) * (b + b') * (c + c') ≠ 0

Tactic:
apply mul_ne_zero (mul_ne_zero _ _) <;> apply add_ne_zero_of_lt

Result:
case h
a b c x : Nimber
hx : x < a
b' : Nimber
hb : b' < b
c' : Nimber
hc : c' < c
hy : b' * c + b * c' + b' * c' < b * c
⊢ c' < c

case h
a b c x : Nimber
hx : x < a
b' : Nimber
hb : b' < b
c' : Nimber
hc : c' < c
hy : b' * c + b * c' + b' * c' < b * c
⊢ x < a

case h
a b c x : Nimber
hx : x < a
b' : Nimber
hb : b' < b
c' : Nimber
hc : c' < c
hy : b' * c + b * c' + b' * c' < b * c
⊢ b' < b

Proof state:
case a
a b c x : Nimber
hx : x < a * b
y : Nimber
hy : y < c
⊢ x * c + a * b * y + x * y ≠ a * (b * c)

Tactic:
obtain ⟨a', ha, b', hb, rfl⟩ := exists_of_lt_mul hx

Result:
case a.intro.intro.intro.intro
a b c y : Nimber
hy : y < c
a' : Nimber
ha : a' < a
b' : Nimber
hb : b' < b
hx : a' * b + a * b' + a' * b' < a * b
⊢ (a' * b + a * b' + a' * b') * c + a * b * y + (a' * b + a * b' + a' * b') * y ≠ a * (b * c)