-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_le_iff₃' : a ⨳ (b ⨳ c) ≤ d ↔ ∀ a' < a, ∀ b' < b, ∀ c' < c,
    a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
      d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')

Proof state:
a b c d : Ordinal.{u}
⊢ a ⨳ (b ⨳ c) ≤ d ↔
    ∀ a' < a,
      ∀ b' < b,
        ∀ c' < c,
          a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
            d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')

Tactic:
simp only [nmul_comm _ (_ ⨳ _), nmul_le_iff₃, nadd_eq_add, toOrdinal_toNatOrdinal]

Result:
a b c d : Ordinal.{u}
⊢ (∀ a' < b,
      ∀ b' < c,
        ∀ c' < a,
          toOrdinal
              (toNatOrdinal (a' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ b' ⨳ a) + toNatOrdinal (b ⨳ c ⨳ c') +
                toNatOrdinal (a' ⨳ b' ⨳ c')) <
            toOrdinal
              (toNatOrdinal d + toNatOrdinal (a' ⨳ b' ⨳ a) + toNatOrdinal (a' ⨳ c ⨳ c') + toNatOrdinal (b ⨳ b' ⨳ c'))) ↔
    ∀ a' < a,
      ∀ b' < b,
        ∀ c' < c,
          toOrdinal
              (toNatOrdinal (b ⨳ c ⨳ a') + toNatOrdinal (b' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ c' ⨳ a) +
                toNatOrdinal (b' ⨳ c' ⨳ a')) <
            toOrdinal
              (toNatOrdinal d + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a') + toNatOrdinal (b' ⨳ c' ⨳ a))

Proof state:
a b c d : Ordinal.{u}
⊢ (∀ a' < b,
      ∀ b' < c,
        ∀ c' < a,
          toOrdinal
              (toNatOrdinal (a' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ b' ⨳ a) + toNatOrdinal (b ⨳ c ⨳ c') +
                toNatOrdinal (a' ⨳ b' ⨳ c')) <
            toOrdinal
              (toNatOrdinal d + toNatOrdinal (a' ⨳ b' ⨳ a) + toNatOrdinal (a' ⨳ c ⨳ c') + toNatOrdinal (b ⨳ b' ⨳ c'))) ↔
    ∀ a' < a,
      ∀ b' < b,
        ∀ c' < c,
          toOrdinal
              (toNatOrdinal (b ⨳ c ⨳ a') + toNatOrdinal (b' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ c' ⨳ a) +
                toNatOrdinal (b' ⨳ c' ⨳ a')) <
            toOrdinal
              (toNatOrdinal d + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a') + toNatOrdinal (b' ⨳ c' ⨳ a))

Tactic:
constructor <;> intro h a' ha b' hb c' hc

Result:
case mp
a b c d : Ordinal.{u}
h :
  ∀ a' < b,
    ∀ b' < c,
      ∀ c' < a,
        toOrdinal
            (toNatOrdinal (a' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ b' ⨳ a) + toNatOrdinal (b ⨳ c ⨳ c') +
              toNatOrdinal (a' ⨳ b' ⨳ c')) <
          toOrdinal
            (toNatOrdinal d + toNatOrdinal (a' ⨳ b' ⨳ a) + toNatOrdinal (a' ⨳ c ⨳ c') + toNatOrdinal (b ⨳ b' ⨳ c'))
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
⊢ toOrdinal
      (toNatOrdinal (b ⨳ c ⨳ a') + toNatOrdinal (b' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ c' ⨳ a) +
        toNatOrdinal (b' ⨳ c' ⨳ a')) <
    toOrdinal (toNatOrdinal d + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a') + toNatOrdinal (b' ⨳ c' ⨳ a))

case mpr
a b c d : Ordinal.{u}
h :
  ∀ a' < a,
    ∀ b' < b,
      ∀ c' < c,
        toOrdinal
            (toNatOrdinal (b ⨳ c ⨳ a') + toNatOrdinal (b' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ c' ⨳ a) +
              toNatOrdinal (b' ⨳ c' ⨳ a')) <
          toOrdinal
            (toNatOrdinal d + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a') + toNatOrdinal (b' ⨳ c' ⨳ a))
a' : Ordinal.{u}
ha : a' < b
b' : Ordinal.{u}
hb : b' < c
c' : Ordinal.{u}
hc : c' < a
⊢ toOrdinal
      (toNatOrdinal (a' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ b' ⨳ a) + toNatOrdinal (b ⨳ c ⨳ c') +
        toNatOrdinal (a' ⨳ b' ⨳ c')) <
    toOrdinal (toNatOrdinal d + toNatOrdinal (a' ⨳ b' ⨳ a) + toNatOrdinal (a' ⨳ c ⨳ c') + toNatOrdinal (b ⨳ b' ⨳ c'))

Proof state:
case mp
a b c d : Ordinal.{u}
h :
  ∀ a' < b,
    ∀ b' < c,
      ∀ c' < a,
        toOrdinal
            (toNatOrdinal (a' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ b' ⨳ a) + toNatOrdinal (b ⨳ c ⨳ c') +
              toNatOrdinal (a' ⨳ b' ⨳ c')) <
          toOrdinal
            (toNatOrdinal d + toNatOrdinal (a' ⨳ b' ⨳ a) + toNatOrdinal (a' ⨳ c ⨳ c') + toNatOrdinal (b ⨳ b' ⨳ c'))
a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
⊢ toOrdinal
      (toNatOrdinal (b ⨳ c ⨳ a') + toNatOrdinal (b' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ c' ⨳ a) +
        toNatOrdinal (b' ⨳ c' ⨳ a')) <
    toOrdinal (toNatOrdinal d + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a') + toNatOrdinal (b' ⨳ c' ⨳ a))

Tactic:
convert h b' hb c' hc a' ha using 1 <;> abel_nf

Result:
no goals

Proof state:
case mpr
a b c d : Ordinal.{u}
h :
  ∀ a' < a,
    ∀ b' < b,
      ∀ c' < c,
        toOrdinal
            (toNatOrdinal (b ⨳ c ⨳ a') + toNatOrdinal (b' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ c' ⨳ a) +
              toNatOrdinal (b' ⨳ c' ⨳ a')) <
          toOrdinal
            (toNatOrdinal d + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a') + toNatOrdinal (b' ⨳ c' ⨳ a))
a' : Ordinal.{u}
ha : a' < b
b' : Ordinal.{u}
hb : b' < c
c' : Ordinal.{u}
hc : c' < a
⊢ toOrdinal
      (toNatOrdinal (a' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ b' ⨳ a) + toNatOrdinal (b ⨳ c ⨳ c') +
        toNatOrdinal (a' ⨳ b' ⨳ c')) <
    toOrdinal (toNatOrdinal d + toNatOrdinal (a' ⨳ b' ⨳ a) + toNatOrdinal (a' ⨳ c ⨳ c') + toNatOrdinal (b ⨳ b' ⨳ c'))

Tactic:
convert h c' hc a' ha b' hb using 1 <;> abel_nf

Result:
no goals