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

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

Tactic:
obtain (⟨b', h, rfl⟩ | ⟨c', h, rfl⟩) := exists_of_lt_add hx <;>
  rw [Nimber.mul_add a', Nimber.mul_add a, Nimber.mul_add a']

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 * 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

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
⊢ x * b + a * y + x * y + a * c ≠ a * (b + c)

Tactic:
have H := mul_ne_of_lt _ hx _ 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 + c) + a * (y + c) + x * (y + c) ≠ a * (b + c)
⊢ x * b + a * y + x * y + a * c ≠ 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 < b
hx' : x * b + a * y + x * y < a * b
h : b + c < y + c
z : Nimber
hz : z < y
hz' : z + c = b + c
⊢ x * b + a * y + x * y + a * c ≠ a * (b + c)

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

Result:
no goals

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
⊢ x * b + a * y + x * y + a * c ≠ a * (b + c)

Tactic:
have := add_eq_iff_eq_add.1 hc'

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'
⊢ x * b + a * y + x * y + a * c ≠ a * (b + c)

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

Tactic:
obtain h | h | h := lt_trichotomy (y + c) (b + c)

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
⊢ x * b + a * y + x * y + a * c ≠ a * (b + c)

case a.h₁.intro.intro.intro.intro.inr.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
⊢ x * b + a * y + x * y + a * c ≠ a * (b + c)

case a.h₁.intro.intro.intro.intro.inr.inr
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
⊢ x * b + a * y + x * y + 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 < c
hx' : x * c + a * y + x * y < a * c
h : b + y < b + c
H : x * (b + c) + a * (b + y) + x * (b + y) ≠ a * (b + c)
⊢ a * b + (x * c + a * y + x * y) ≠ 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 < 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)

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 * c + a * y + x * y) ≠ a * (b + c)

Tactic:
rw [← hb', Nimber.mul_add a b', ← add_ne_add_left (a * y), ← add_ne_add_left (a * b),
  ← add_ne_add_left (a * b'), ← hb'', Nimber.mul_add x, Nimber.mul_add x]

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 * 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'

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

Tactic:
apply add_le_of_forall_ne <;>
  (intro x' hx'; obtain ⟨x, hx, y, hy, rfl⟩ := exists_of_lt_mul hx')

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

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

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

Tactic:
obtain ⟨x, hx, y, hy, rfl⟩ := exists_of_lt_mul hx'

Result:
case a.h₂.intro.intro.intro.intro
a b c x : Nimber
hx : x < a
y : Nimber
hy : y < c
hx' : x * c + a * y + x * y < a * c
⊢ a * b + (x * c + 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
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))

Tactic:
simpa only [two_zsmul, add_zero, zero_add] using H

Result:
no goals

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 * c + (a * c' + (x * c' + (2 • (a * c) + (2 • (x * y) + 2 • (a * y))))) = 2 • (a * c') + (a * c + 2 • (a * y))

Tactic:
simpa only [two_zsmul, add_zero, zero_add] using H

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 * 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

Tactic:
on_goal 2 => rw [← add_ne_add_left (a * b)]

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 * b + a * c + a * b

Proof state:
case a.h₂.intro.intro.intro.intro.inr.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
⊢ a * b + (x * c + a * y + x * y) ≠ a * (b + c)

Tactic:
exact (hy.ne <| add_right_injective _ h).elim

Result:
no goals

Proof state:
case a.h₁.intro.intro.intro.intro.inr.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
⊢ x * b + a * y + x * y + a * c ≠ a * (b + c)

Tactic:
exact (hy.ne <| add_left_injective _ h).elim

Result:
no goals