-- Mathlib/SetTheory/Nimber/Field.lean
theorem mul_add (a b c : Nimber) : a * (b + c) = a * b + 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 * 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

Tactic:
all_goals
  abel_nf
  simp only [two_zsmul, zero_add]
  rw [← add_assoc]
  exact mul_ne_of_lt _ ha _ 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 : 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)

Tactic:
simpa only [two_zsmul, zero_add] using H

Result:
no goals

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

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

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

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
⊢ ¬2 • (a' * b) + (a' * c + (2 • (a * b) + (a * c' + a' * c'))) = 2 • (a * b) + a * c

Tactic:
simp only [two_zsmul, zero_add]

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

Tactic:
obtain ⟨b', hb, hb'⟩ | ⟨z, hz, hz'⟩ := exists_of_lt_add 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
⊢ a * b + (x * c + a * y + x * y) ≠ a * (b + c)

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)

Proof state:
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)

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

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

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)

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

Tactic:
abel_nf

Result:
case a.inr.intro.intro
a b c a' : Nimber
ha : a' < a
c' : Nimber
h : c' < c
hx : b + c' < b + c
⊢ ¬2 • (a' * b) + (a' * c + (2 • (a * b) + (a * c' + a' * c'))) = 2 • (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 < 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:
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 < 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)

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:
exact mul_ne_of_lt _ ha _ h

Result:
no goals

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

Tactic:
refine mul_le_of_forall_ne fun a' ha x hx ↦ ?_

Result:
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

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

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

Proof state:
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)

Tactic:
obtain ⟨z, hz, hz'⟩ | ⟨c', hc, hc'⟩ := exists_of_lt_add 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 < 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)

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)

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

Tactic:
intro x' hx'

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

Tactic:
abel_nf at H ⊢

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

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