-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem lt_nmul_iff₃ : d < a ⨳ b ⨳ c ↔ ∃ a' < a, ∃ b' < b, ∃ c' < c,
    d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤
      a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'

Proof state:
case refine_1.intro.intro.intro.intro
a b c d : Ordinal.{u}
h : d < a ⨳ b ⨳ c
e : Ordinal.{u}
he : e < a ⨳ b
c' : Ordinal.{u}
hc : c' < c
H₁ : d ♯ e ⨳ c' ≤ e ⨳ c ♯ a ⨳ b ⨳ c'
⊢ ∃ a' < a,
    ∃ b' < b,
      ∃ c' < c, d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'

Tactic:
rcases lt_nmul_iff.1 he with ⟨a', ha, b', hb, H₂⟩

Result:
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro
a b c d : Ordinal.{u}
h : d < a ⨳ b ⨳ c
e : Ordinal.{u}
he : e < a ⨳ b
c' : Ordinal.{u}
hc : c' < c
H₁ : d ♯ e ⨳ c' ≤ e ⨳ c ♯ a ⨳ b ⨳ c'
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
H₂ : e ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
⊢ ∃ a' < a,
    ∃ b' < b,
      ∃ c' < c, d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'

Proof state:
case refine_2
a b c d : Ordinal.{u}
x✝ :
  ∃ a' < a,
    ∃ b' < b,
      ∃ c' < c, d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
h : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
this : d < a ⨳ b ⨳ c
⊢ d < a ⨳ b ⨳ c

Tactic:
assumption

Result:
no goals

Proof state:
case refine_2
a b c d : Ordinal.{u}
x✝ :
  ∃ a' < a,
    ∃ b' < b,
      ∃ c' < c, d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
h : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
this : d ♯ a' ⨳ b' ⨳ c < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c
⊢ d < a ⨳ b ⨳ c

Tactic:
rw [nadd_lt_nadd_iff_right] at this

Result:
case refine_2
a b c d : Ordinal.{u}
x✝ :
  ∃ a' < a,
    ∃ b' < b,
      ∃ c' < c, d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
h : d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
this : d < a ⨳ b ⨳ c
⊢ d < a ⨳ b ⨳ c

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro
a b c d : Ordinal.{u}
h : d < a ⨳ b ⨳ c
e : Ordinal.{u}
he : e < a ⨳ b
c' : Ordinal.{u}
hc : c' < c
H₁ : d ♯ e ⨳ c' ≤ e ⨳ c ♯ a ⨳ b ⨳ c'
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
H₂ : e ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
⊢ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'

Tactic:
have := nadd_le_nadd H₁ (nmul_nadd_le H₂ hc.le)

Result:
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro
a b c d : Ordinal.{u}
h : d < a ⨳ b ⨳ c
e : Ordinal.{u}
he : e < a ⨳ b
c' : Ordinal.{u}
hc : c' < c
H₁ : d ♯ e ⨳ c' ≤ e ⨳ c ♯ a ⨳ b ⨳ c'
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
H₂ : e ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this :
  d ♯ e ⨳ c' ♯ ((e ♯ a' ⨳ b') ⨳ c ♯ (a' ⨳ b ♯ a ⨳ b') ⨳ c') ≤
    e ⨳ c ♯ a ⨳ b ⨳ c' ♯ ((a' ⨳ b ♯ a ⨳ b') ⨳ c ♯ (e ♯ a' ⨳ b') ⨳ c')
⊢ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'