-- 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:
a b c d : Ordinal.{u}
⊢ 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'

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨a', ha, b', hb, c', hc, h⟩ ↦ ?_⟩

Result:
case refine_1
a b c d : Ordinal.{u}
h : 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'

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'
⊢ 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'
⊢ ∃ 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:
refine ⟨a', ha, b', hb, c', hc, ?_⟩

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'
⊢ 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
a b c d : Ordinal.{u}
h : 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'

Tactic:
rcases lt_nmul_iff.1 h with ⟨e, he, c', hc, H₁⟩

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

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' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
⊢ d < a ⨳ b ⨳ c

Tactic:
repeat 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_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'
⊢ d < a ⨳ b ⨳ c

Tactic:
have := h.trans_lt (nmul_nadd_lt₃ ha hb hc)

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 ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ 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'
this :
  d ♯ (e ⨳ c' ♯ (e ⨳ c ♯ (a' ⨳ b' ⨳ c ♯ (a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c')))) ≤
    e ⨳ c ♯ (a ⨳ b ⨳ c' ♯ (a' ⨳ b ⨳ c ♯ (a ⨳ b' ⨳ c ♯ (e ⨳ c' ♯ 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'

Tactic:
rw [nadd_left_comm, nadd_left_comm d, nadd_left_comm, nadd_le_nadd_iff_left,
  nadd_left_comm (a ⨳ b' ⨳ c), nadd_left_comm (a' ⨳ b ⨳ c), nadd_left_comm (a ⨳ b ⨳ c'),
  nadd_le_nadd_iff_left, nadd_left_comm (a ⨳ b ⨳ c'), nadd_left_comm (a ⨳ b ⨳ c')] at this

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 ♯ (a' ⨳ b' ⨳ c ♯ (a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c')) ≤ a' ⨳ b ⨳ c ♯ (a ⨳ b' ⨳ c ♯ (a ⨳ b ⨳ c' ♯ 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'

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'
this : d ♯ (a' ⨳ b' ⨳ c ♯ (a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c')) ≤ a' ⨳ b ⨳ c ♯ (a ⨳ b' ⨳ c ♯ (a ⨳ b ⨳ c' ♯ 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'

Tactic:
simpa only [nadd_assoc]

Result:
no goals

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

Tactic:
simp only [nadd_nmul, nadd_assoc] at this

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 ⨳ c ♯ (a' ⨳ b' ⨳ c ♯ (a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c')))) ≤
    e ⨳ c ♯ (a ⨳ b ⨳ c' ♯ (a' ⨳ b ⨳ c ♯ (a ⨳ b' ⨳ c ♯ (e ⨳ c' ♯ 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'