-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_nadd (a b c : Ordinal) : a ⨳ (b ♯ c) = a ⨳ b ♯ a ⨳ c

Proof state:
case refine_2.intro.intro.intro.intro
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ b
a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
hd : d ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
⊢ d ♯ a ⨳ c < a ⨳ (b ♯ c)

Tactic:
have := nadd_lt_nadd_of_le_of_lt hd (nmul_nadd_lt ha (nadd_lt_nadd_right hb c))

Result:
case refine_2.intro.intro.intro.intro
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ b
a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
hd : d ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : d ♯ a' ⨳ b' ♯ (a' ⨳ (b ♯ c) ♯ a ⨳ (b' ♯ c)) < a' ⨳ b ♯ a ⨳ b' ♯ (a ⨳ (b ♯ c) ♯ a' ⨳ (b' ♯ c))
⊢ d ♯ a ⨳ c < a ⨳ (b ♯ c)

Proof state:
case refine_1
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd : d < b ♯ c
⊢ a' ⨳ (b ♯ c) ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d

Tactic:
rw [nmul_nadd]

Result:
case refine_1
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd : d < b ♯ c
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d

Proof state:
case refine_1.inr.intro.intro
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
c' : Ordinal.{u_1}
hc : c' < c
hd : d ≤ b ♯ c'
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d

Tactic:
have := nadd_lt_nadd_of_le_of_lt (nmul_nadd_le ha.le hd) (nmul_nadd_lt ha hc)

Result:
case refine_1.inr.intro.intro
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
c' : Ordinal.{u_1}
hc : c' < c
hd : d ≤ b ♯ c'
this : a' ⨳ (b ♯ c') ♯ a ⨳ d ♯ (a' ⨳ c ♯ a ⨳ c') < a ⨳ (b ♯ c') ♯ a' ⨳ d ♯ (a ⨳ c ♯ a' ⨳ c')
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d

Proof state:
case refine_1
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd : d < b ♯ c
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d

Tactic:
rcases lt_nadd_iff.1 hd with (⟨b', hb, hd⟩ | ⟨c', hc, hd⟩)

Result:
case refine_1.inl.intro.intro
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
b' : Ordinal.{u_1}
hb : b' < b
hd : d ≤ b' ♯ c
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d

case refine_1.inr.intro.intro
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
c' : Ordinal.{u_1}
hc : c' < c
hd : d ≤ b ♯ c'
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d

Proof state:
case refine_1.inl.intro.intro
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
b' : Ordinal.{u_1}
hb : b' < b
hd : d ≤ b' ♯ c
this : a' ⨳ b ♯ (a ⨳ b' ♯ (a' ⨳ b' ♯ (a' ⨳ c ♯ a ⨳ d))) < a ⨳ b ♯ (a' ⨳ b' ♯ (a ⨳ b' ♯ (a ⨳ c ♯ a' ⨳ d)))
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d

Tactic:
rwa [nadd_left_comm, nadd_left_comm _ (a ⨳ b'), nadd_left_comm (a ⨳ b),
  nadd_lt_nadd_iff_left, nadd_left_comm (a' ⨳ b), nadd_left_comm (a ⨳ b),
  nadd_lt_nadd_iff_left, ← nadd_assoc, ← nadd_assoc] at this

Result:
no goals

Proof state:
case refine_1.inr.intro.intro
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
c' : Ordinal.{u_1}
hc : c' < c
hd : d ≤ b ♯ c'
this : a' ⨳ (b ♯ c') ♯ a ⨳ d ♯ (a' ⨳ c ♯ a ⨳ c') < a ⨳ (b ♯ c') ♯ a' ⨳ d ♯ (a ⨳ c ♯ a' ⨳ c')
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d

Tactic:
rw [nmul_nadd, nmul_nadd] at this

Result:
case refine_1.inr.intro.intro
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
c' : Ordinal.{u_1}
hc : c' < c
hd : d ≤ b ♯ c'
this : a' ⨳ b ♯ a' ⨳ c' ♯ a ⨳ d ♯ (a' ⨳ c ♯ a ⨳ c') < a ⨳ b ♯ a ⨳ c' ♯ a' ⨳ d ♯ (a ⨳ c ♯ a' ⨳ c')
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d

Proof state:
case refine_2.intro.intro.intro.intro
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ b
a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
hd : d ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : d ♯ a' ⨳ b' ♯ (a' ⨳ b ♯ a' ⨳ c ♯ (a ⨳ b' ♯ a ⨳ c)) < a' ⨳ b ♯ a ⨳ b' ♯ (a ⨳ (b ♯ c) ♯ (a' ⨳ b' ♯ a' ⨳ c))
⊢ d ♯ a ⨳ c < a ⨳ (b ♯ c)

Tactic:
simp only [nadd_assoc] at this

Result:
case refine_2.intro.intro.intro.intro
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ b
a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
hd : d ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : d ♯ (a' ⨳ b' ♯ (a' ⨳ b ♯ (a' ⨳ c ♯ (a ⨳ b' ♯ a ⨳ c)))) < a' ⨳ b ♯ (a ⨳ b' ♯ (a ⨳ (b ♯ c) ♯ (a' ⨳ b' ♯ a' ⨳ c)))
⊢ d ♯ a ⨳ c < a ⨳ (b ♯ c)

Proof state:
case refine_1.inr.intro.intro
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
c' : Ordinal.{u_1}
hc : c' < c
hd : d ≤ b ♯ c'
this : a' ⨳ b ♯ a' ⨳ c' ♯ a ⨳ d ♯ (a' ⨳ c ♯ a ⨳ c') < a ⨳ b ♯ a ⨳ c' ♯ a' ⨳ d ♯ (a ⨳ c ♯ a' ⨳ c')
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d

Tactic:
simp only [nadd_assoc] at this

Result:
case refine_1.inr.intro.intro
a b c a' : Ordinal.{u_1}
ha : a' < a
d : Ordinal.{u_1}
hd✝ : d < b ♯ c
c' : Ordinal.{u_1}
hc : c' < c
hd : d ≤ b ♯ c'
this : a' ⨳ b ♯ (a' ⨳ c' ♯ (a ⨳ d ♯ (a' ⨳ c ♯ a ⨳ c'))) < a ⨳ b ♯ (a ⨳ c' ♯ (a' ⨳ d ♯ (a ⨳ c ♯ a' ⨳ c')))
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d

Proof state:
case refine_3.intro.intro.intro.intro
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ c
a' : Ordinal.{u_1}
ha : a' < a
c' : Ordinal.{u_1}
hc : c' < c
hd : d ♯ a' ⨳ c' ≤ a' ⨳ c ♯ a ⨳ c'
this : a' ⨳ b ♯ a' ⨳ c ♯ (a ⨳ b ♯ a ⨳ c') ♯ (d ♯ a' ⨳ c') < a ⨳ (b ♯ c) ♯ (a' ⨳ b ♯ a' ⨳ c') ♯ (a' ⨳ c ♯ a ⨳ c')
⊢ a ⨳ b ♯ d < a ⨳ (b ♯ c)

Tactic:
simp only [nadd_assoc] at this

Result:
case refine_3.intro.intro.intro.intro
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ c
a' : Ordinal.{u_1}
ha : a' < a
c' : Ordinal.{u_1}
hc : c' < c
hd : d ♯ a' ⨳ c' ≤ a' ⨳ c ♯ a ⨳ c'
this : a' ⨳ b ♯ (a' ⨳ c ♯ (a ⨳ b ♯ (a ⨳ c' ♯ (d ♯ a' ⨳ c')))) < a ⨳ (b ♯ c) ♯ (a' ⨳ b ♯ (a' ⨳ c' ♯ (a' ⨳ c ♯ a ⨳ c')))
⊢ a ⨳ b ♯ d < a ⨳ (b ♯ c)

Proof state:
case refine_2.intro.intro.intro.intro
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ b
a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
hd : d ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : d ♯ a' ⨳ b' ♯ (a' ⨳ (b ♯ c) ♯ a ⨳ (b' ♯ c)) < a' ⨳ b ♯ a ⨳ b' ♯ (a ⨳ (b ♯ c) ♯ a' ⨳ (b' ♯ c))
⊢ d ♯ a ⨳ c < a ⨳ (b ♯ c)

Tactic:
rw [nmul_nadd, nmul_nadd, nmul_nadd a'] at this

Result:
case refine_2.intro.intro.intro.intro
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ b
a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
hd : d ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : d ♯ a' ⨳ b' ♯ (a' ⨳ b ♯ a' ⨳ c ♯ (a ⨳ b' ♯ a ⨳ c)) < a' ⨳ b ♯ a ⨳ b' ♯ (a ⨳ (b ♯ c) ♯ (a' ⨳ b' ♯ a' ⨳ c))
⊢ d ♯ a ⨳ c < a ⨳ (b ♯ c)

Proof state:
case refine_3.intro.intro.intro.intro
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ c
a' : Ordinal.{u_1}
ha : a' < a
c' : Ordinal.{u_1}
hc : c' < c
hd : d ♯ a' ⨳ c' ≤ a' ⨳ c ♯ a ⨳ c'
⊢ a ⨳ b ♯ d < a ⨳ (b ♯ c)

Tactic:
have := nadd_lt_nadd_of_lt_of_le (nmul_nadd_lt ha (nadd_lt_nadd_left hc b)) hd

Result:
case refine_3.intro.intro.intro.intro
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ c
a' : Ordinal.{u_1}
ha : a' < a
c' : Ordinal.{u_1}
hc : c' < c
hd : d ♯ a' ⨳ c' ≤ a' ⨳ c ♯ a ⨳ c'
this : a' ⨳ (b ♯ c) ♯ a ⨳ (b ♯ c') ♯ (d ♯ a' ⨳ c') < a ⨳ (b ♯ c) ♯ a' ⨳ (b ♯ c') ♯ (a' ⨳ c ♯ a ⨳ c')
⊢ a ⨳ b ♯ d < a ⨳ (b ♯ c)

Proof state:
case refine_3.intro.intro.intro.intro
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ c
a' : Ordinal.{u_1}
ha : a' < a
c' : Ordinal.{u_1}
hc : c' < c
hd : d ♯ a' ⨳ c' ≤ a' ⨳ c ♯ a ⨳ c'
this : a' ⨳ (b ♯ c) ♯ a ⨳ (b ♯ c') ♯ (d ♯ a' ⨳ c') < a ⨳ (b ♯ c) ♯ a' ⨳ (b ♯ c') ♯ (a' ⨳ c ♯ a ⨳ c')
⊢ a ⨳ b ♯ d < a ⨳ (b ♯ c)

Tactic:
rw [nmul_nadd, nmul_nadd, nmul_nadd a'] at this

Result:
case refine_3.intro.intro.intro.intro
a b c d : Ordinal.{u_1}
hd✝ : d < a ⨳ c
a' : Ordinal.{u_1}
ha : a' < a
c' : Ordinal.{u_1}
hc : c' < c
hd : d ♯ a' ⨳ c' ≤ a' ⨳ c ♯ a ⨳ c'
this : a' ⨳ b ♯ a' ⨳ c ♯ (a ⨳ b ♯ a ⨳ c') ♯ (d ♯ a' ⨳ c') < a ⨳ (b ♯ c) ♯ (a' ⨳ b ♯ a' ⨳ c') ♯ (a' ⨳ c ♯ a ⨳ c')
⊢ a ⨳ b ♯ d < a ⨳ (b ♯ c)