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

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

Tactic:
exact nmul_nadd_lt₃' ha hb hc

Result:
no goals

Proof state:
a b c : Ordinal.{u_1}
⊢ a ⨳ b ⨳ c = a ⨳ (b ⨳ c)

Tactic:
apply le_antisymm

Result:
case a
a b c : Ordinal.{u_1}
⊢ a ⨳ b ⨳ c ≤ a ⨳ (b ⨳ c)

case a
a b c : Ordinal.{u_1}
⊢ a ⨳ (b ⨳ c) ≤ a ⨳ b ⨳ c

Proof state:
case a
a b c : Ordinal.{u_1}
⊢ a ⨳ b ⨳ c ≤ a ⨳ (b ⨳ c)

Tactic:
rw [nmul_le_iff₃]

Result:
case a
a b c : Ordinal.{u_1}
⊢ ∀ a' < a,
    ∀ b' < b,
      ∀ c' < c,
        a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ (b ⨳ c) ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'

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

Tactic:
rw [nmul_assoc]

Result:
case a
a b c a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
c' : Ordinal.{u_1}
hc : c' < c
⊢ a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
    a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')

Proof state:
case a
a b c a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
c' : Ordinal.{u_1}
hc : c' < c
⊢ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'

Tactic:
exact nmul_nadd_lt₃ ha hb hc

Result:
no goals

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

Tactic:
repeat rw [nmul_assoc]

Result:
case a
a b c a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
c' : Ordinal.{u_1}
hc : c' < c
⊢ a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
    a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')

Proof state:
case a
a b c : Ordinal.{u_1}
⊢ a ⨳ (b ⨳ c) ≤ a ⨳ b ⨳ c

Tactic:
rw [nmul_le_iff₃']

Result:
case a
a b c : Ordinal.{u_1}
⊢ ∀ a' < a,
    ∀ b' < b,
      ∀ c' < c,
        a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
          a ⨳ b ⨳ c ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')

Proof state:
case a
a b c : Ordinal.{u_1}
⊢ ∀ a' < a,
    ∀ b' < b,
      ∀ c' < c,
        a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ (b ⨳ c) ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'

Tactic:
intro a' ha b' hb c' hc

Result:
case a
a b c a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
c' : Ordinal.{u_1}
hc : c' < c
⊢ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ (b ⨳ c) ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'

Proof state:
case a
a b c : Ordinal.{u_1}
⊢ ∀ a' < a,
    ∀ b' < b,
      ∀ c' < c,
        a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
          a ⨳ b ⨳ c ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')

Tactic:
intro a' ha b' hb c' hc

Result:
case a
a b c a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
c' : Ordinal.{u_1}
hc : c' < c
⊢ a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
    a ⨳ b ⨳ c ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')

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

Tactic:
repeat rw [← nmul_assoc]

Result:
case a
a b c a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
c' : Ordinal.{u_1}
hc : c' < c
⊢ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'

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

Tactic:
rw [← nmul_assoc]

Result:
case a
a b c a' : Ordinal.{u_1}
ha : a' < a
b' : Ordinal.{u_1}
hb : b' < b
c' : Ordinal.{u_1}
hc : c' < c
⊢ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'