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

Proof state:
case a.h₂.intro.intro.intro.intro.inr.inr.inl.intro.intro
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < c
hx' : x * c + a * y + x * y < a * c
h : b + c < b + y
b' : Nimber
hb : b' < b
hb' : b' + y = b + c
⊢ a * b + (x * c + a * y + x * y) ≠ a * (b + c)

Tactic:
have H := mul_ne_of_lt _ hx _ hb

Result:
case a.h₂.intro.intro.intro.intro.inr.inr.inl.intro.intro
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < c
hx' : x * c + a * y + x * y < a * c
h : b + c < b + y
b' : Nimber
hb : b' < b
hb' : b' + y = b + c
H : x * b + a * b' + x * b' ≠ a * b
⊢ a * b + (x * c + a * y + x * y) ≠ a * (b + c)

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

Tactic:
apply le_antisymm

Result:
case a
a b c : Nimber
⊢ a * (b + c) ≤ a * b + a * c

case a
a b c : Nimber
⊢ a * b + a * c ≤ a * (b + c)

Proof state:
case a.h₁.intro.intro.intro.intro.inl
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < b
hx' : x * b + a * y + x * y < a * b
h : y + c < b + c
H : x * b + (2 • (x * c) + (a * y + (a * c + x * y))) ≠ a * (b + c)
⊢ ¬x * b + (a * y + (a * c + x * y)) = a * (b + c)

Tactic:
simpa only [two_zsmul, zero_add] using H

Result:
no goals

Proof state:
case a.h₂.intro.intro.intro.intro.inl
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < c
hx' : x * c + a * y + x * y < a * c
h : b + y < b + c
H : x * b + x * c + (a * b + a * y) + (x * b + x * y) ≠ a * (b + c)
⊢ a * b + (x * c + a * y + x * y) ≠ a * (b + c)

Tactic:
abel_nf at H ⊢

Result:
case a.h₂.intro.intro.intro.intro.inl
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < c
hx' : x * c + a * y + x * y < a * c
h : b + y < b + c
H : 2 • (x * b) + (x * c + (a * b + (a * y + x * y))) ≠ a * (b + c)
⊢ ¬x * c + (a * b + (a * y + x * y)) = a * (b + c)

Proof state:
case a.h₂.intro.intro.intro.intro.inr.inr.inl.intro.intro
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < c
hx' : x * c + a * y + x * y < a * c
h : b + c < b + y
b' : Nimber
hb : b' < b
hb' : b' + y = b + c
H : x * b + a * b' + x * b' ≠ a * b
⊢ a * b + (x * c + a * y + x * y) ≠ a * (b + c)

Tactic:
have hb'' := add_eq_iff_eq_add.2 (add_comm b c ▸ hb')

Result:
case a.h₂.intro.intro.intro.intro.inr.inr.inl.intro.intro
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < c
hx' : x * c + a * y + x * y < a * c
h : b + c < b + y
b' : Nimber
hb : b' < b
hb' : b' + y = b + c
H : x * b + a * b' + x * b' ≠ a * b
hb'' : b' + y + b = c
⊢ a * b + (x * c + a * y + x * y) ≠ a * (b + c)

Proof state:
case a.h₂.intro.intro.intro.intro.inr.inr.inr.intro.intro
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < c
hx' : x * c + a * y + x * y < a * c
h : b + c < b + y
z : Nimber
hz : z < y
hz' : b + z = b + c
⊢ a * b + (x * c + a * y + x * y) ≠ a * (b + c)

Tactic:
exact ((hz.trans hy).ne <| add_right_injective _ hz').elim

Result:
no goals

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

case a.inr.intro.intro
a b c a' : Nimber
ha : a' < a
c' : Nimber
h : c' < c
hx : b + c' < b + c
⊢ a' * b + a' * c + (a * b + a * c') + (a' * b + a' * c') ≠ a * b + a * c

Tactic:
on_goal 1 => rw [← add_ne_add_left (a * c)]

Result:
case a.inl.intro.intro
a b c a' : Nimber
ha : a' < a
b' : Nimber
h : b' < b
hx : b' + c < b + c
⊢ a' * b + a' * c + (a * b' + a * c) + (a' * b' + a' * c) + a * c ≠ a * b + a * c + a * c

case a.inr.intro.intro
a b c a' : Nimber
ha : a' < a
c' : Nimber
h : c' < c
hx : b + c' < b + c
⊢ a' * b + a' * c + (a * b + a * c') + (a' * b + a' * c') ≠ a * b + a * c

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

Tactic:
rw [Nimber.mul_add x, Nimber.mul_add a, Nimber.mul_add x] at H

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

Proof state:
case a.inr.intro.intro
a b c a' : Nimber
ha : a' < a
c' : Nimber
h : c' < c
hx : b + c' < b + c
⊢ ¬a' * c + (a * c' + a' * c') = a * c

Tactic:
rw [← add_assoc]

Result:
case a.inr.intro.intro
a b c a' : Nimber
ha : a' < a
c' : Nimber
h : c' < c
hx : b + c' < b + c
⊢ ¬a' * c + a * c' + a' * c' = a * c

Proof state:
case a.h₂.intro.intro.intro.intro.inr.inr.inl.intro.intro
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < c
hx' : x * c + a * y + x * y < a * c
h : b + c < b + y
b' : Nimber
hb : b' < b
hb' : b' + y = b + c
H : x * b + a * b' + x * b' ≠ a * b
hb'' : b' + y + b = c
⊢ a * b + (x * b' + x * y + x * b + a * y + x * y) + a * y + a * b + a * b' ≠ a * b' + a * y + a * y + a * b + a * b'

Tactic:
abel_nf at H ⊢

Result:
case a.h₂.intro.intro.intro.intro.inr.inr.inl.intro.intro
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < c
hx' : x * c + a * y + x * y < a * c
h : b + c < b + y
b' : Nimber
hb : b' < b
hb' : b' + y = b + c
hb'' : b' + y + b = c
H : x * b + (a * b' + x * b') ≠ a * b
⊢ ¬x * b + (a * b' + (x * b' + (2 • (a * b) + (2 • (x * y) + 2 • (a * y))))) = 2 • (a * b') + (a * b + 2 • (a * y))

Proof state:
case a.h₁.intro.intro.intro.intro.inr.inr.inr.intro.intro
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < b
hx' : x * b + a * y + x * y < a * b
h : b + c < y + c
c' : Nimber
hc : c' < c
hc' : y + c' = b + c
this : y = b + c + c'
H : x * c + a * c' + x * c' ≠ a * c
⊢ x * b + a * y + x * y + a * c ≠ a * (b + c)

Tactic:
rw [← hc', Nimber.mul_add a y c', ← add_ne_add_left (a * y), ← add_ne_add_left (a * c),
  ← add_ne_add_left (a * c'), ← add_eq_iff_eq_add.2 hc', Nimber.mul_add x,
  Nimber.mul_add x]

Result:
case a.h₁.intro.intro.intro.intro.inr.inr.inr.intro.intro
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < b
hx' : x * b + a * y + x * y < a * b
h : b + c < y + c
c' : Nimber
hc : c' < c
hc' : y + c' = b + c
this : y = b + c + c'
H : x * c + a * c' + x * c' ≠ a * c
⊢ x * y + x * c' + x * c + a * y + x * y + a * c + a * y + a * c + a * c' ≠ a * y + a * c' + a * y + a * c + a * c'

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

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

Result:
case a.inl.intro.intro
a b c a' : Nimber
ha : a' < a
b' : Nimber
h : b' < b
hx : b' + c < b + c
⊢ a' * b + a' * c + (a * b' + a * c) + (a' * b' + a' * c) + a * c ≠ a * b + a * c + a * c