[GOAL]
a✝ b✝ c a b : Ordinal.{u}
⊢ a ♯ b = max (blsub a fun a' x => a' ♯ b) (blsub b fun b' x => a ♯ b')
[PROOFSTEP]
rw [nadd]
[GOAL]
a b c : Ordinal.{u}
⊢ a < b ♯ c ↔ (∃ b', b' < b ∧ a ≤ b' ♯ c) ∨ ∃ c', c' < c ∧ a ≤ b ♯ c'
[PROOFSTEP]
rw [nadd_def]
[GOAL]
a b c : Ordinal.{u}
⊢ a < max (blsub b fun a' x => a' ♯ c) (blsub c fun b' x => b ♯ b') ↔
    (∃ b', b' < b ∧ a ≤ b' ♯ c) ∨ ∃ c', c' < c ∧ a ≤ b ♯ c'
[PROOFSTEP]
simp [lt_blsub_iff]
[GOAL]
a b c : Ordinal.{u}
⊢ b ♯ c ≤ a ↔ (∀ (b' : Ordinal.{u}), b' < b → b' ♯ c < a) ∧ ∀ (c' : Ordinal.{u}), c' < c → b ♯ c' < a
[PROOFSTEP]
rw [nadd_def]
[GOAL]
a b c : Ordinal.{u}
⊢ max (blsub b fun a' x => a' ♯ c) (blsub c fun b' x => b ♯ b') ≤ a ↔
    (∀ (b' : Ordinal.{u}), b' < b → b' ♯ c < a) ∧ ∀ (c' : Ordinal.{u}), c' < c → b ♯ c' < a
[PROOFSTEP]
simp [blsub_le_iff]
[GOAL]
a✝ b c : Ordinal.{u}
h : b ≤ c
a : Ordinal.{u}
⊢ a ♯ b ≤ a ♯ c
[PROOFSTEP]
rcases lt_or_eq_of_le h with (h | rfl)
[GOAL]
case inl
a✝ b c : Ordinal.{u}
h✝ : b ≤ c
a : Ordinal.{u}
h : b < c
⊢ a ♯ b ≤ a ♯ c
[PROOFSTEP]
exact (nadd_lt_nadd_left h a).le
[GOAL]
case inr
a✝ b a : Ordinal.{u}
h : b ≤ b
⊢ a ♯ b ≤ a ♯ b
[PROOFSTEP]
exact le_rfl
[GOAL]
a✝ b c : Ordinal.{u}
h : b ≤ c
a : Ordinal.{u}
⊢ b ♯ a ≤ c ♯ a
[PROOFSTEP]
rcases lt_or_eq_of_le h with (h | rfl)
[GOAL]
case inl
a✝ b c : Ordinal.{u}
h✝ : b ≤ c
a : Ordinal.{u}
h : b < c
⊢ b ♯ a ≤ c ♯ a
[PROOFSTEP]
exact (nadd_lt_nadd_right h a).le
[GOAL]
case inr
a✝ b a : Ordinal.{u}
h : b ≤ b
⊢ b ♯ a ≤ b ♯ a
[PROOFSTEP]
exact le_rfl
[GOAL]
a✝ b✝ c : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ a ♯ b = b ♯ a
[PROOFSTEP]
rw [nadd_def, nadd_def, max_comm]
[GOAL]
a✝ b✝ c : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ max (blsub b fun b' x => a ♯ b') (blsub a fun a' x => a' ♯ b) =
    max (blsub b fun a' x => a' ♯ a) (blsub a fun b' x => b ♯ b')
[PROOFSTEP]
congr
[GOAL]
case e_a.e_f
a✝ b✝ c : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ (fun b' x => a ♯ b') = fun a' x => a' ♯ a
[PROOFSTEP]
ext
[GOAL]
case e_a.e_f
a✝ b✝ c : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ (fun a' x => a' ♯ b) = fun b' x => b ♯ b'
[PROOFSTEP]
ext
[GOAL]
case e_a.e_f.h.h
a✝ b✝ c : Ordinal.{u}
a b x✝¹ : Ordinal.{u_1}
x✝ : x✝¹ < b
⊢ a ♯ x✝¹ = x✝¹ ♯ a
[PROOFSTEP]
apply nadd_comm
[GOAL]
case e_a.e_f.h.h
a✝ b✝ c : Ordinal.{u}
a b x✝¹ : Ordinal.{u_1}
x✝ : x✝¹ < a
⊢ x✝¹ ♯ b = b ♯ x✝¹
[PROOFSTEP]
apply nadd_comm
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ blsub (a ♯ b) f =
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
[PROOFSTEP]
apply (blsub_le_iff.2 fun i h => _).antisymm (max_le _ _)
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ ∀ (i : Ordinal.{u}) (h : i < a ♯ b),
    f i h <
      max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b))
        (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) ≤ blsub (a ♯ b) f
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) ≤ blsub (a ♯ b) f
[PROOFSTEP]
intro i h
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
i : Ordinal.{u}
h : i < a ♯ b
⊢ f i h <
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
[PROOFSTEP]
rcases lt_nadd_iff.1 h with (⟨a', ha', hi⟩ | ⟨b', hb', hi⟩)
[GOAL]
case inl.intro.intro
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
i : Ordinal.{u}
h : i < a ♯ b
a' : Ordinal.{u}
ha' : a' < a
hi : i ≤ a' ♯ b
⊢ f i h <
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
[PROOFSTEP]
exact lt_max_of_lt_left ((hf h (nadd_lt_nadd_right ha' b) hi).trans_lt (lt_blsub _ _ ha'))
[GOAL]
case inr.intro.intro
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
i : Ordinal.{u}
h : i < a ♯ b
b' : Ordinal.{u}
hb' : b' < b
hi : i ≤ a ♯ b'
⊢ f i h <
    max (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b))
[PROOFSTEP]
exact lt_max_of_lt_right ((hf h (nadd_lt_nadd_left hb' a) hi).trans_lt (lt_blsub _ _ hb'))
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) ≤ blsub (a ♯ b) f
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) ≤ blsub (a ♯ b) f
[PROOFSTEP]
all_goals
  apply blsub_le_of_brange_subset.{u, u, v}
  rintro c ⟨d, hd, rfl⟩
  apply mem_brange_self
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub a fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) ≤ blsub (a ♯ b) f
[PROOFSTEP]
apply blsub_le_of_brange_subset.{u, u, v}
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (brange a fun a_1 ha => (fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) a_1 ha) ⊆
    brange (a ♯ b) fun a_1 ha => f a_1 ha
[PROOFSTEP]
rintro c ⟨d, hd, rfl⟩
[GOAL]
case intro.intro
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
d : Ordinal.{u}
hd : d < a
⊢ (fun a_1 ha => (fun a' ha' => f (a' ♯ b) (_ : a' ♯ b < a ♯ b)) a_1 ha) d hd ∈ brange (a ♯ b) fun a_1 ha => f a_1 ha
[PROOFSTEP]
apply mem_brange_self
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (blsub b fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) ≤ blsub (a ♯ b) f
[PROOFSTEP]
apply blsub_le_of_brange_subset.{u, u, v}
[GOAL]
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
⊢ (brange b fun a_1 ha => (fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) a_1 ha) ⊆
    brange (a ♯ b) fun a_1 ha => f a_1 ha
[PROOFSTEP]
rintro c ⟨d, hd, rfl⟩
[GOAL]
case intro.intro
a b c : Ordinal.{u}
f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj
d : Ordinal.{u}
hd : d < b
⊢ (fun a_1 ha => (fun b' hb' => f (a ♯ b') (_ : a ♯ b' < a ♯ b)) a_1 ha) d hd ∈ brange (a ♯ b) fun a_1 ha => f a_1 ha
[PROOFSTEP]
apply mem_brange_self
[GOAL]
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ a ♯ b ♯ c = a ♯ (b ♯ c)
[PROOFSTEP]
rw [nadd_def a (b ♯ c), nadd_def, blsub_nadd_of_mono, blsub_nadd_of_mono, max_assoc]
[GOAL]
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ max (blsub a fun a' ha' => a' ♯ b ♯ c) (max (blsub b fun b' hb' => a ♯ b' ♯ c) (blsub c fun b' x => a ♯ b ♯ b')) =
    max (blsub a fun a' x => a' ♯ (b ♯ c))
      (max (blsub b fun a' ha' => a ♯ (a' ♯ c)) (blsub c fun b' hb' => a ♯ (b ♯ b')))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_f
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ (fun a' ha' => a' ♯ b ♯ c) = fun a' x => a' ♯ (b ♯ c)
[PROOFSTEP]
ext (d hd)
[GOAL]
case e_a.e_a.e_f
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ (fun b' hb' => a ♯ b' ♯ c) = fun a' ha' => a ♯ (a' ♯ c)
[PROOFSTEP]
ext (d hd)
[GOAL]
case e_a.e_a.e_f
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ (fun b' x => a ♯ b ♯ b') = fun b' hb' => a ♯ (b ♯ b')
[PROOFSTEP]
ext (d hd)
[GOAL]
case e_a.e_f.h.h
a✝ b✝ c✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd : d < a
⊢ d ♯ b ♯ c = d ♯ (b ♯ c)
[PROOFSTEP]
apply nadd_assoc
[GOAL]
case e_a.e_a.e_f.h.h
a✝ b✝ c✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd : d < b
⊢ a ♯ d ♯ c = a ♯ (d ♯ c)
[PROOFSTEP]
apply nadd_assoc
[GOAL]
case e_a.e_a.e_f.h.h
a✝ b✝ c✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd : d < c
⊢ a ♯ b ♯ d = a ♯ (b ♯ d)
[PROOFSTEP]
apply nadd_assoc
[GOAL]
case hf
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ ∀ {i j : Ordinal.{u_1}}, i < b ♯ c → j < b ♯ c → i ≤ j → a ♯ i ≤ a ♯ j
[PROOFSTEP]
exact fun _ _ h => nadd_le_nadd_left h a
[GOAL]
case hf
a✝ b✝ c✝ : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ ∀ {i j : Ordinal.{u_1}}, i < a ♯ b → j < a ♯ b → i ≤ j → i ♯ c ≤ j ♯ c
[PROOFSTEP]
exact fun _ _ h => nadd_le_nadd_right h c
[GOAL]
a b c : Ordinal.{u}
⊢ a ♯ 0 = a
[PROOFSTEP]
induction' a using Ordinal.induction with a IH
[GOAL]
case h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 0 = k
⊢ a ♯ 0 = a
[PROOFSTEP]
rw [nadd_def, blsub_zero, max_zero_right]
[GOAL]
case h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 0 = k
⊢ (blsub a fun a' x => a' ♯ 0) = a
[PROOFSTEP]
convert blsub_id a
[GOAL]
case h.e'_2.h.e'_2.h.h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 0 = k
x✝¹ : Ordinal.{u}
x✝ : x✝¹ < a
⊢ x✝¹ ♯ 0 = x✝¹
[PROOFSTEP]
rename_i hb
[GOAL]
case h.e'_2.h.e'_2.h.h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 0 = k
x✝ : Ordinal.{u}
hb : x✝ < a
⊢ x✝ ♯ 0 = x✝
[PROOFSTEP]
exact IH _ hb
[GOAL]
a b c : Ordinal.{u}
⊢ 0 ♯ a = a
[PROOFSTEP]
rw [nadd_comm, nadd_zero]
[GOAL]
a b c : Ordinal.{u}
⊢ a ♯ 1 = succ a
[PROOFSTEP]
induction' a using Ordinal.induction with a IH
[GOAL]
case h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 1 = succ k
⊢ a ♯ 1 = succ a
[PROOFSTEP]
rw [nadd_def, blsub_one, nadd_zero, max_eq_right_iff, blsub_le_iff]
[GOAL]
case h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 1 = succ k
⊢ ∀ (i : Ordinal.{u}), i < a → i ♯ 1 < succ a
[PROOFSTEP]
intro i hi
[GOAL]
case h
a✝ b c a : Ordinal.{u}
IH : ∀ (k : Ordinal.{u}), k < a → k ♯ 1 = succ k
i : Ordinal.{u}
hi : i < a
⊢ i ♯ 1 < succ a
[PROOFSTEP]
rwa [IH i hi, succ_lt_succ_iff]
[GOAL]
a b c : Ordinal.{u}
⊢ 1 ♯ a = succ a
[PROOFSTEP]
rw [nadd_comm, nadd_one]
[GOAL]
a b c : Ordinal.{u}
⊢ a ♯ succ b = succ (a ♯ b)
[PROOFSTEP]
rw [← nadd_one (a ♯ b), nadd_assoc, nadd_one]
[GOAL]
a b c : Ordinal.{u}
⊢ succ a ♯ b = succ (a ♯ b)
[PROOFSTEP]
rw [← one_nadd (a ♯ b), ← nadd_assoc, one_nadd]
[GOAL]
a b c : Ordinal.{u}
n : ℕ
⊢ a ♯ ↑n = a + ↑n
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
a b c : Ordinal.{u}
⊢ a ♯ ↑Nat.zero = a + ↑Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
a b c : Ordinal.{u}
n : ℕ
hn : a ♯ ↑n = a + ↑n
⊢ a ♯ ↑(Nat.succ n) = a + ↑(Nat.succ n)
[PROOFSTEP]
rw [Nat.cast_succ, add_one_eq_succ, nadd_succ, add_succ, hn]
[GOAL]
a b c : Ordinal.{u}
n : ℕ
⊢ ↑n ♯ a = a + ↑n
[PROOFSTEP]
rw [nadd_comm, nadd_nat]
[GOAL]
a b c : Ordinal.{u}
⊢ a + b ≤ a ♯ b
[PROOFSTEP]
induction b using limitRecOn with
| H₁ => simp
| H₂ c h => rwa [add_succ, nadd_succ, succ_le_succ_iff]
| H₃ c hc H =>
  simp_rw [← IsNormal.blsub_eq.{u, u} (add_isNormal a) hc, blsub_le_iff]
  exact fun i hi => (H i hi).trans_lt (nadd_lt_nadd_left hi a)
[GOAL]
a b c : Ordinal.{u}
⊢ a + b ≤ a ♯ b
[PROOFSTEP]
induction b using limitRecOn with
| H₁ => simp
| H₂ c h => rwa [add_succ, nadd_succ, succ_le_succ_iff]
| H₃ c hc H =>
  simp_rw [← IsNormal.blsub_eq.{u, u} (add_isNormal a) hc, blsub_le_iff]
  exact fun i hi => (H i hi).trans_lt (nadd_lt_nadd_left hi a)
[GOAL]
case H₁
a b c : Ordinal.{u}
⊢ a + 0 ≤ a ♯ 0
[PROOFSTEP]

| H₁ => simp
[GOAL]
case H₁
a b c : Ordinal.{u}
⊢ a + 0 ≤ a ♯ 0
[PROOFSTEP]
simp
[GOAL]
case H₂
a b c✝ c : Ordinal.{u}
h : a + c ≤ a ♯ c
⊢ a + succ c ≤ a ♯ succ c
[PROOFSTEP]

| H₂ c h => rwa [add_succ, nadd_succ, succ_le_succ_iff]
[GOAL]
case H₂
a b c✝ c : Ordinal.{u}
h : a + c ≤ a ♯ c
⊢ a + succ c ≤ a ♯ succ c
[PROOFSTEP]
rwa [add_succ, nadd_succ, succ_le_succ_iff]
[GOAL]
case H₃
a b c✝ c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a + o' ≤ a ♯ o'
⊢ a + c ≤ a ♯ c
[PROOFSTEP]

| H₃ c hc H =>
  simp_rw [← IsNormal.blsub_eq.{u, u} (add_isNormal a) hc, blsub_le_iff]
  exact fun i hi => (H i hi).trans_lt (nadd_lt_nadd_left hi a)
[GOAL]
case H₃
a b c✝ c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a + o' ≤ a ♯ o'
⊢ a + c ≤ a ♯ c
[PROOFSTEP]
simp_rw [← IsNormal.blsub_eq.{u, u} (add_isNormal a) hc, blsub_le_iff]
[GOAL]
case H₃
a b c✝ c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a + o' ≤ a ♯ o'
⊢ ∀ (i : Ordinal.{u}), i < c → a + i < a ♯ c
[PROOFSTEP]
exact fun i hi => (H i hi).trans_lt (nadd_lt_nadd_left hi a)
[GOAL]
a b c : NatOrdinal
h : a + b ≤ a + c
⊢ b ≤ c
[PROOFSTEP]
by_contra' h'
[GOAL]
a b c : NatOrdinal
h : a + b ≤ a + c
h' : c < b
⊢ False
[PROOFSTEP]
exact h.not_lt (add_lt_add_left h' a)
[GOAL]
n : ℕ
⊢ ↑toOrdinal ↑n = ↑n
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
⊢ ↑toOrdinal ↑Nat.zero = ↑Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
n : ℕ
hn : ↑toOrdinal ↑n = ↑n
⊢ ↑toOrdinal ↑(Nat.succ n) = ↑(Nat.succ n)
[PROOFSTEP]
change (toOrdinal n) ♯ 1 = n + 1
[GOAL]
case succ
n : ℕ
hn : ↑toOrdinal ↑n = ↑n
⊢ ↑toOrdinal ↑n ♯ 1 = ↑n + 1
[PROOFSTEP]
rw [hn]
[GOAL]
case succ
n : ℕ
hn : ↑toOrdinal ↑n = ↑n
⊢ ↑n ♯ 1 = ↑n + 1
[PROOFSTEP]
exact nadd_one n
[GOAL]
n : ℕ
⊢ ↑toNatOrdinal ↑n = ↑n
[PROOFSTEP]
rw [← toOrdinal_cast_nat n]
[GOAL]
n : ℕ
⊢ ↑toNatOrdinal (↑toOrdinal ↑n) = ↑n
[PROOFSTEP]
rfl
[GOAL]
a b : Ordinal.{u_1}
⊢ a ≤ b ♯ a
[PROOFSTEP]
simpa using nadd_le_nadd_right (Ordinal.zero_le b) a
[GOAL]
a b : Ordinal.{u_1}
⊢ a ≤ a ♯ b
[PROOFSTEP]
simpa using nadd_le_nadd_left (Ordinal.zero_le b) a
[GOAL]
a✝ b✝ c d : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ a ⨳ b = sInf {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
[PROOFSTEP]
rw [nmul]
[GOAL]
a b c d a' b' : Ordinal.{u}
ha : a' < a
hb : b' < b
⊢ a' ⨳ b ♯ a ⨳ b' < a ⨳ b ♯ a' ⨳ b'
[PROOFSTEP]
rw [nmul_def a b]
[GOAL]
a b c d a' b' : Ordinal.{u}
ha : a' < a
hb : b' < b
⊢ a' ⨳ b ♯ a ⨳ b' <
    sInf {c | ∀ (a' : Ordinal.{u}), a' < a → ∀ (b' : Ordinal.{u}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} ♯ a' ⨳ b'
[PROOFSTEP]
exact csInf_mem (nmul_nonempty a b) a' ha b' hb
[GOAL]
a b c d a' b' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
⊢ a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'
[PROOFSTEP]
rcases lt_or_eq_of_le ha with (ha | rfl)
[GOAL]
case inl
a b c d a' b' : Ordinal.{u}
ha✝ : a' ≤ a
hb : b' ≤ b
ha : a' < a
⊢ a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'
[PROOFSTEP]
rcases lt_or_eq_of_le hb with (hb | rfl)
[GOAL]
case inl.inl
a b c d a' b' : Ordinal.{u}
ha✝ : a' ≤ a
hb✝ : b' ≤ b
ha : a' < a
hb : b' < b
⊢ a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'
[PROOFSTEP]
exact (nmul_nadd_lt ha hb).le
[GOAL]
case inl.inr
a c d a' b' : Ordinal.{u}
ha✝ : a' ≤ a
ha : a' < a
hb : b' ≤ b'
⊢ a' ⨳ b' ♯ a ⨳ b' ≤ a ⨳ b' ♯ a' ⨳ b'
[PROOFSTEP]
rw [nadd_comm]
[GOAL]
case inr
b c d a' b' : Ordinal.{u}
hb : b' ≤ b
ha : a' ≤ a'
⊢ a' ⨳ b ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a' ⨳ b'
[PROOFSTEP]
exact le_rfl
[GOAL]
a b c d : Ordinal.{u}
⊢ c < a ⨳ b ↔ ∃ a', a' < a ∧ ∃ b', b' < b ∧ c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
a b c d : Ordinal.{u}
h : c < a ⨳ b
⊢ ∃ a', a' < a ∧ ∃ b', b' < b ∧ c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
[PROOFSTEP]
rw [nmul] at h 
[GOAL]
case refine'_1
a b c d : Ordinal.{u}
h : c < sInf {c | ∀ (a' : Ordinal.{u}), a' < a → ∀ (b' : Ordinal.{u}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
⊢ ∃ a', a' < a ∧ ∃ b', b' < b ∧ c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
[PROOFSTEP]
simpa using not_mem_of_lt_csInf h ⟨0, fun _ _ => bot_le⟩
[GOAL]
case refine'_2
a b c d : Ordinal.{u}
⊢ (∃ a', a' < a ∧ ∃ b', b' < b ∧ c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b') → c < a ⨳ b
[PROOFSTEP]
rintro ⟨a', ha, b', hb, h⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
a b c d a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
h : c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
⊢ c < a ⨳ b
[PROOFSTEP]
have := h.trans_lt (nmul_nadd_lt ha hb)
[GOAL]
case refine'_2.intro.intro.intro.intro
a b c d a' : Ordinal.{u}
ha : a' < a
b' : Ordinal.{u}
hb : b' < b
h : c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
this : c ♯ a' ⨳ b' < a ⨳ b ♯ a' ⨳ b'
⊢ c < a ⨳ b
[PROOFSTEP]
rwa [nadd_lt_nadd_iff_right] at this 
[GOAL]
a b c d : Ordinal.{u}
⊢ a ⨳ b ≤ c ↔ ∀ (a' : Ordinal.{u}), a' < a → ∀ (b' : Ordinal.{u}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
a b c d : Ordinal.{u}
⊢ ¬a ⨳ b ≤ c ↔ ¬∀ (a' : Ordinal.{u}), a' < a → ∀ (b' : Ordinal.{u}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'
[PROOFSTEP]
simp [lt_nmul_iff]
[GOAL]
a✝ b✝ c d : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ a ⨳ b = b ⨳ a
[PROOFSTEP]
rw [nmul, nmul]
[GOAL]
a✝ b✝ c d : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ sInf {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} =
    sInf {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
[PROOFSTEP]
congr
[GOAL]
case e_a
a✝ b✝ c d : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} =
    {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
[PROOFSTEP]
ext x
[GOAL]
case e_a.h
a✝ b✝ c d : Ordinal.{u}
a b x : Ordinal.{u_1}
⊢ x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} ↔
    x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
[PROOFSTEP]
constructor
[GOAL]
case e_a.h.mp
a✝ b✝ c d : Ordinal.{u}
a b x : Ordinal.{u_1}
⊢ x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} →
    x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
[PROOFSTEP]
intro H c hc d hd
[GOAL]
case e_a.h.mpr
a✝ b✝ c d : Ordinal.{u}
a b x : Ordinal.{u_1}
⊢ x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'} →
    x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
[PROOFSTEP]
intro H c hc d hd
[GOAL]
case e_a.h.mp
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < b
d : Ordinal.{u_1}
hd : d < a
⊢ c ⨳ a ♯ b ⨳ d < x ♯ c ⨳ d
[PROOFSTEP]
rw [nadd_comm, ← nmul_comm d b, ← nmul_comm a c, ← nmul_comm d]
[GOAL]
case e_a.h.mp
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < b → a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < b
d : Ordinal.{u_1}
hd : d < a
⊢ d ⨳ b ♯ a ⨳ c < x ♯ d ⨳ c
[PROOFSTEP]
exact H _ hd _ hc
[GOAL]
case e_a.h.mpr
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
⊢ c ⨳ b ♯ a ⨳ d < x ♯ c ⨳ d
[PROOFSTEP]
rw [nadd_comm, nmul_comm a d, nmul_comm c, nmul_comm c]
[GOAL]
case e_a.h.mpr
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < b → ∀ (b' : Ordinal.{u_1}), b' < a → a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
⊢ d ⨳ a ♯ b ⨳ c < x ♯ d ⨳ c
[PROOFSTEP]
exact H _ hd _ hc
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ a ⨳ 0 = 0
[PROOFSTEP]
rw [← Ordinal.le_zero, nmul_le_iff]
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < 0 → a' ⨳ 0 ♯ a ⨳ b' < 0 ♯ a' ⨳ b'
[PROOFSTEP]
exact fun _ _ a ha => (Ordinal.not_lt_zero a ha).elim
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ 0 ⨳ a = 0
[PROOFSTEP]
rw [nmul_comm, nmul_zero]
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ a ⨳ 1 = a
[PROOFSTEP]
rw [nmul]
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ sInf {c | ∀ (a' : Ordinal.{u_1}), a' < a → ∀ (b' : Ordinal.{u_1}), b' < 1 → a' ⨳ 1 ♯ a ⨳ b' < c ♯ a' ⨳ b'} = a
[PROOFSTEP]
simp only [lt_one_iff_zero, forall_eq, nmul_zero, nadd_zero]
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ sInf {c | ∀ (a' : Ordinal.{u_1}), a' < a → a' ⨳ 1 < c} = a
[PROOFSTEP]
convert csInf_Ici (α := Ordinal)
[GOAL]
case h.e'_2.h.e'_3
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ {c | ∀ (a' : Ordinal.{u_1}), a' < a → a' ⨳ 1 < c} = Set.Ici a
[PROOFSTEP]
ext b
[GOAL]
case h.e'_2.h.e'_3.h
a✝ b✝ c d : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ b ∈ {c | ∀ (a' : Ordinal.{u_1}), a' < a → a' ⨳ 1 < c} ↔ b ∈ Set.Ici a
[PROOFSTEP]
simp only [Set.mem_setOf_eq, Set.mem_Ici]
[GOAL]
case h.e'_2.h.e'_3.h
a✝ b✝ c d : Ordinal.{u}
a b : Ordinal.{u_1}
⊢ (∀ (a' : Ordinal.{u_1}), a' < a → a' ⨳ 1 < b) ↔ a ≤ b
[PROOFSTEP]
refine'
  ⟨fun H => le_of_forall_lt fun c hc => _, fun ha c hc => _⟩
    -- Porting note: had to add arguments to `nmul_one` in the next two lines
      -- for the termination checker.
[GOAL]
case h.e'_2.h.e'_3.h.refine'_1
a✝ b✝ c✝ d : Ordinal.{u}
a b : Ordinal.{u_1}
H : ∀ (a' : Ordinal.{u_1}), a' < a → a' ⨳ 1 < b
c : Ordinal.{u_1}
hc : c < a
⊢ c < b
[PROOFSTEP]
simpa only [nmul_one c] using H c hc
[GOAL]
case h.e'_2.h.e'_3.h.refine'_2
a✝ b✝ c✝ d : Ordinal.{u}
a b : Ordinal.{u_1}
ha : a ≤ b
c : Ordinal.{u_1}
hc : c < a
⊢ c ⨳ 1 < b
[PROOFSTEP]
simpa only [nmul_one c] using hc.trans_le ha
[GOAL]
a✝ b c d : Ordinal.{u}
a : Ordinal.{u_1}
⊢ 1 ⨳ a = a
[PROOFSTEP]
rw [nmul_comm, nmul_one]
[GOAL]
a b c d : Ordinal.{u}
h₁ : a < b
h₂ : 0 < c
⊢ c ⨳ a ♯ 0 ⨳ a ≤ 0 ⨳ b ♯ c ⨳ a
[PROOFSTEP]
simp
[GOAL]
a b c d : Ordinal.{u}
h₁ : a < b
h₂ : 0 < c
⊢ a ⨳ c ♯ a ⨳ 0 ≤ a ⨳ c ♯ b ⨳ 0
[PROOFSTEP]
simp
[GOAL]
a b c d : Ordinal.{u}
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ c ⨳ a ≤ c ⨳ b
[PROOFSTEP]
rcases lt_or_eq_of_le h₁ with (h₁ | rfl)
[GOAL]
case inl
a b c d : Ordinal.{u}
h₁✝ : a ≤ b
h₂ : 0 ≤ c
h₁ : a < b
⊢ c ⨳ a ≤ c ⨳ b
[PROOFSTEP]
rcases lt_or_eq_of_le h₂ with (h₂ | rfl)
[GOAL]
case inr
a c d : Ordinal.{u}
h₂ : 0 ≤ c
h₁ : a ≤ a
⊢ c ⨳ a ≤ c ⨳ a
[PROOFSTEP]
rcases lt_or_eq_of_le h₂ with (h₂ | rfl)
[GOAL]
case inl.inl
a b c d : Ordinal.{u}
h₁✝ : a ≤ b
h₂✝ : 0 ≤ c
h₁ : a < b
h₂ : 0 < c
⊢ c ⨳ a ≤ c ⨳ b
[PROOFSTEP]
exact (nmul_lt_nmul_of_pos_left h₁ h₂).le
[GOAL]
case inl.inr
a b d : Ordinal.{u}
h₁✝ : a ≤ b
h₁ : a < b
h₂ : 0 ≤ 0
⊢ 0 ⨳ a ≤ 0 ⨳ b
case inr.inl
a c d : Ordinal.{u}
h₂✝ : 0 ≤ c
h₁ : a ≤ a
h₂ : 0 < c
⊢ c ⨳ a ≤ c ⨳ a
case inr.inr a d : Ordinal.{u} h₁ : a ≤ a h₂ : 0 ≤ 0 ⊢ 0 ⨳ a ≤ 0 ⨳ a
[PROOFSTEP]
all_goals simp
[GOAL]
case inl.inr
a b d : Ordinal.{u}
h₁✝ : a ≤ b
h₁ : a < b
h₂ : 0 ≤ 0
⊢ 0 ⨳ a ≤ 0 ⨳ b
[PROOFSTEP]
simp
[GOAL]
case inr.inl
a c d : Ordinal.{u}
h₂✝ : 0 ≤ c
h₁ : a ≤ a
h₂ : 0 < c
⊢ c ⨳ a ≤ c ⨳ a
[PROOFSTEP]
simp
[GOAL]
case inr.inr
a d : Ordinal.{u}
h₁ : a ≤ a
h₂ : 0 ≤ 0
⊢ 0 ⨳ a ≤ 0 ⨳ a
[PROOFSTEP]
simp
[GOAL]
a b c d : Ordinal.{u}
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ a ⨳ c ≤ b ⨳ c
[PROOFSTEP]
rw [nmul_comm, nmul_comm b]
[GOAL]
a b c d : Ordinal.{u}
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ c ⨳ a ≤ c ⨳ b
[PROOFSTEP]
exact nmul_le_nmul_of_nonneg_left h₁ h₂
[GOAL]
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ a ⨳ (b ♯ c) = a ⨳ b ♯ a ⨳ c
[PROOFSTEP]
refine le_antisymm (nmul_le_iff.2 fun a' ha d hd => ?_) (nadd_le_iff.2 ⟨fun d hd => ?_, fun d hd => ?_⟩)
[GOAL]
case refine_1
a✝ b✝ c✝ d✝ : Ordinal.{u}
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
[PROOFSTEP]
rw [nmul_nadd a' b c]
[GOAL]
case refine_1
a✝ b✝ c✝ d✝ : Ordinal.{u}
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
[PROOFSTEP]
rcases lt_nadd_iff.1 hd with (⟨b', hb, hd⟩ | ⟨c', hc, hd⟩)
[GOAL]
case refine_1.inl.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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
[PROOFSTEP]
have :=
  nadd_lt_nadd_of_lt_of_le (nmul_nadd_lt ha hb)
    (nmul_nadd_le ha.le hd)
      -- Porting note: adding arguments to `nmul_nadd` for the termination checker.
[GOAL]
case refine_1.inl.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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' ♯ c) ♯ a ⨳ d) < a ⨳ b ♯ a' ⨳ b' ♯ (a ⨳ (b' ♯ c) ♯ a' ⨳ d)
⊢ a' ⨳ b ♯ a' ⨳ c ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d
[PROOFSTEP]
rw [nmul_nadd a' b' c, nmul_nadd a b' c] at this 
[GOAL]
case refine_1.inl.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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
[PROOFSTEP]
simp only [nadd_assoc] at this 
[GOAL]
case refine_1.inl.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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
[PROOFSTEP]
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 
[GOAL]
case refine_1.inr.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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
[PROOFSTEP]
have :=
  nadd_lt_nadd_of_le_of_lt (nmul_nadd_le ha.le hd)
    (nmul_nadd_lt ha hc)
      -- Porting note: adding arguments to `nmul_nadd` for the termination checker.
[GOAL]
case refine_1.inr.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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
[PROOFSTEP]
rw [nmul_nadd a' b c', nmul_nadd a b c'] at this 
[GOAL]
case refine_1.inr.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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
[PROOFSTEP]
simp only [nadd_assoc] at this 
[GOAL]
case refine_1.inr.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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
[PROOFSTEP]
rwa [nadd_left_comm, nadd_comm (a ⨳ c), nadd_left_comm (a' ⨳ d), nadd_left_comm (a ⨳ c'), nadd_left_comm (a ⨳ b),
  nadd_lt_nadd_iff_left, nadd_comm (a' ⨳ c), nadd_left_comm (a ⨳ d), nadd_left_comm (a' ⨳ b), nadd_left_comm (a ⨳ b),
  nadd_lt_nadd_iff_left, nadd_comm (a ⨳ d), nadd_comm (a' ⨳ d), ← nadd_assoc, ← nadd_assoc] at this 
[GOAL]
case refine_2
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd : d < a ⨳ b
⊢ d ♯ a ⨳ c < a ⨳ (b ♯ c)
[PROOFSTEP]
rcases lt_nmul_iff.1 hd with ⟨a', ha, b', hb, hd⟩
[GOAL]
case refine_2.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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)
[PROOFSTEP]
have :=
  nadd_lt_nadd_of_le_of_lt hd
    (nmul_nadd_lt ha (nadd_lt_nadd_right hb c))
      -- Porting note: adding arguments to `nmul_nadd` for the termination checker.
[GOAL]
case refine_2.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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)
[PROOFSTEP]
rw [nmul_nadd a' b c, nmul_nadd a b' c, nmul_nadd a'] at this 
[GOAL]
case refine_2.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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)
[PROOFSTEP]
simp only [nadd_assoc] at this 
[GOAL]
case refine_2.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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)
[PROOFSTEP]
rwa [nadd_left_comm (a' ⨳ b'), nadd_left_comm, nadd_lt_nadd_iff_left, nadd_left_comm, nadd_left_comm _ (a' ⨳ b'),
  nadd_left_comm (a ⨳ b'), nadd_lt_nadd_iff_left, nadd_left_comm (a' ⨳ c), nadd_left_comm, nadd_lt_nadd_iff_left,
  nadd_left_comm, nadd_comm _ (a' ⨳ c), nadd_lt_nadd_iff_left] at this 
[GOAL]
case refine_3
a✝ b✝ c✝ d✝ : Ordinal.{u}
a b c d : Ordinal.{u_1}
hd : d < a ⨳ c
⊢ a ⨳ b ♯ d < a ⨳ (b ♯ c)
[PROOFSTEP]
rcases lt_nmul_iff.1 hd with ⟨a', ha, c', hc, hd⟩
[GOAL]
case refine_3.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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)
[PROOFSTEP]
have := nadd_lt_nadd_of_lt_of_le (nmul_nadd_lt ha (nadd_lt_nadd_left hc b)) hd
[GOAL]
case refine_3.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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)
[PROOFSTEP]
rw [nmul_nadd a' b c, nmul_nadd a b c', nmul_nadd a'] at this 
[GOAL]
case refine_3.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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)
[PROOFSTEP]
simp only [nadd_assoc] at this 
[GOAL]
case refine_3.intro.intro.intro.intro
a✝ b✝ c✝ d✝ : Ordinal.{u}
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)
[PROOFSTEP]
rwa [nadd_left_comm _ (a' ⨳ b), nadd_lt_nadd_iff_left, nadd_left_comm (a' ⨳ c'), nadd_left_comm _ (a' ⨳ c),
  nadd_lt_nadd_iff_left, nadd_left_comm, nadd_comm (a' ⨳ c'), nadd_left_comm _ (a ⨳ c'), nadd_lt_nadd_iff_left,
  nadd_comm _ (a' ⨳ c'), nadd_comm _ (a' ⨳ c'), nadd_left_comm, nadd_lt_nadd_iff_left] at this 
[GOAL]
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ (a ♯ b) ⨳ c = a ⨳ c ♯ b ⨳ c
[PROOFSTEP]
rw [nmul_comm, nmul_nadd, nmul_comm, nmul_comm c]
[GOAL]
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
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'
[PROOFSTEP]
simpa only [nadd_nmul, ← nadd_assoc] using nmul_nadd_lt (nmul_nadd_lt ha hb) hc
[GOAL]
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
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'
[PROOFSTEP]
simpa only [nadd_nmul, ← nadd_assoc] using nmul_nadd_le (nmul_nadd_le ha hb) hc
[GOAL]
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
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')
[PROOFSTEP]
simp only [nmul_comm _ (_ ⨳ _)]
[GOAL]
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' < b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a
[PROOFSTEP]
convert nmul_nadd_lt₃ hb hc ha using 1
[GOAL]
case h.e'_3
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' = b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b ⨳ c ⨳ a' ♯ b' ⨳ c' ⨳ a'
[PROOFSTEP]
simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]
[GOAL]
case h.e'_3
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a')) =
    ↑toOrdinal
      (↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
abel_nf
[GOAL]
case h.e'_4
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a = b ⨳ c ⨳ a ♯ b' ⨳ c' ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a'
[PROOFSTEP]
simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]
[GOAL]
case h.e'_4
a b c d a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a)) =
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a) + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') +
        ↑toNatOrdinal (b ⨳ c' ⨳ a'))
[PROOFSTEP]
abel_nf
[GOAL]
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
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')
[PROOFSTEP]
simp only [nmul_comm _ (_ ⨳ _)]
[GOAL]
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' ≤ b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a
[PROOFSTEP]
convert nmul_nadd_le₃ hb hc ha using 1
[GOAL]
case h.e'_3
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' = b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b ⨳ c ⨳ a' ♯ b' ⨳ c' ⨳ a'
[PROOFSTEP]
simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]
[GOAL]
case h.e'_3
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a')) =
    ↑toOrdinal
      (↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
abel_nf
[GOAL]
case h.e'_4
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a = b ⨳ c ⨳ a ♯ b' ⨳ c' ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a'
[PROOFSTEP]
simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]
[GOAL]
case h.e'_4
a b c d a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a)) =
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a) + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') +
        ↑toNatOrdinal (b ⨳ c' ⨳ a'))
[PROOFSTEP]
abel_nf
[GOAL]
a b c d : Ordinal.{u}
⊢ d < a ⨳ b ⨳ c ↔
    ∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
constructor
[GOAL]
case mp
a b c d : Ordinal.{u}
⊢ d < a ⨳ b ⨳ c →
    ∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
intro h
[GOAL]
case mp
a b c d : Ordinal.{u}
h : d < a ⨳ b ⨳ c
⊢ ∃ a',
    a' < a ∧
      ∃ b',
        b' < b ∧
          ∃ c',
            c' < c ∧ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
rcases lt_nmul_iff.1 h with ⟨e, he, c', hc, H₁⟩
[GOAL]
case mp.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' < a ∧
      ∃ b',
        b' < b ∧
          ∃ c',
            c' < c ∧ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
rcases lt_nmul_iff.1 he with ⟨a', ha, b', hb, H₂⟩
[GOAL]
case mp.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' < a ∧
      ∃ b',
        b' < b ∧
          ∃ c',
            c' < c ∧ d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
[PROOFSTEP]
refine' ⟨a', ha, b', hb, c', hc, _⟩
[GOAL]
case mp.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'
[PROOFSTEP]
have := nadd_le_nadd H₁ (nmul_nadd_le H₂ hc.le)
[GOAL]
case mp.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'
[PROOFSTEP]
simp only [nadd_nmul, nadd_assoc] at this 
[GOAL]
case mp.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'
[PROOFSTEP]
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 
[GOAL]
case mp.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'
[PROOFSTEP]
simpa only [nadd_assoc]
[GOAL]
case mpr
a b c d : Ordinal.{u}
⊢ (∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧
                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
[PROOFSTEP]
rintro ⟨a', ha, b', hb, c', hc, h⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d 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
[PROOFSTEP]
have := h.trans_lt (nmul_nadd_lt₃ ha hb hc)
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d 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
[PROOFSTEP]
repeat' rw [nadd_lt_nadd_iff_right] at this 
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d 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
[PROOFSTEP]
rw [nadd_lt_nadd_iff_right] at this 
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d 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'
⊢ d < a ⨳ b ⨳ c
[PROOFSTEP]
rw [nadd_lt_nadd_iff_right] at this 
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d 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
[PROOFSTEP]
rw [nadd_lt_nadd_iff_right] at this 
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d 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
[PROOFSTEP]
rw [nadd_lt_nadd_iff_right] at this 
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d 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
[PROOFSTEP]
assumption
[GOAL]
a b c d : Ordinal.{u}
⊢ a ⨳ b ⨳ c ≤ d ↔
    ∀ (a' : Ordinal.{u}),
      a' < a →
        ∀ (b' : Ordinal.{u}),
          b' < b →
            ∀ (c' : Ordinal.{u}),
              c' < c → a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
a b c d : Ordinal.{u}
⊢ ¬a ⨳ b ⨳ c ≤ d ↔
    ¬∀ (a' : Ordinal.{u}),
        a' < a →
          ∀ (b' : Ordinal.{u}),
            b' < b →
              ∀ (c' : Ordinal.{u}),
                c' < c →
                  a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
[PROOFSTEP]
simp [lt_nmul_iff₃]
[GOAL]
a b c d : Ordinal.{u}
⊢ d < a ⨳ (b ⨳ c) ↔
    ∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧
                d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c') ≤
                  a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c')
[PROOFSTEP]
simp only [nmul_comm _ (_ ⨳ _), lt_nmul_iff₃, nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]
[GOAL]
a b c d : Ordinal.{u}
⊢ (∃ a',
      a' < b ∧
        ∃ b',
          b' < c ∧
            ∃ c',
              c' < a ∧
                ↑toOrdinal
                    (↑toNatOrdinal d + ↑toNatOrdinal (a' ⨳ b' ⨳ a) + ↑toNatOrdinal (a' ⨳ c ⨳ c') +
                      ↑toNatOrdinal (b ⨳ b' ⨳ c')) ≤
                  ↑toOrdinal
                    (↑toNatOrdinal (a' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ b' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ c') +
                      ↑toNatOrdinal (a' ⨳ b' ⨳ c'))) ↔
    ∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧
                ↑toOrdinal
                    (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') +
                      ↑toNatOrdinal (b' ⨳ c' ⨳ a)) ≤
                  ↑toOrdinal
                    (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
                      ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
constructor
[GOAL]
case mp
a b c d : Ordinal.{u}
⊢ (∃ a',
      a' < b ∧
        ∃ b',
          b' < c ∧
            ∃ c',
              c' < a ∧
                ↑toOrdinal
                    (↑toNatOrdinal d + ↑toNatOrdinal (a' ⨳ b' ⨳ a) + ↑toNatOrdinal (a' ⨳ c ⨳ c') +
                      ↑toNatOrdinal (b ⨳ b' ⨳ c')) ≤
                  ↑toOrdinal
                    (↑toNatOrdinal (a' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ b' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ c') +
                      ↑toNatOrdinal (a' ⨳ b' ⨳ c'))) →
    ∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧
                ↑toOrdinal
                    (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') +
                      ↑toNatOrdinal (b' ⨳ c' ⨳ a)) ≤
                  ↑toOrdinal
                    (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
                      ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
rintro ⟨b', hb, c', hc, a', ha, h⟩
[GOAL]
case mpr
a b c d : Ordinal.{u}
⊢ (∃ a',
      a' < a ∧
        ∃ b',
          b' < b ∧
            ∃ c',
              c' < c ∧
                ↑toOrdinal
                    (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') +
                      ↑toNatOrdinal (b' ⨳ c' ⨳ a)) ≤
                  ↑toOrdinal
                    (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
                      ↑toNatOrdinal (b' ⨳ c' ⨳ a'))) →
    ∃ a',
      a' < b ∧
        ∃ b',
          b' < c ∧
            ∃ c',
              c' < a ∧
                ↑toOrdinal
                    (↑toNatOrdinal d + ↑toNatOrdinal (a' ⨳ b' ⨳ a) + ↑toNatOrdinal (a' ⨳ c ⨳ c') +
                      ↑toNatOrdinal (b ⨳ b' ⨳ c')) ≤
                  ↑toOrdinal
                    (↑toNatOrdinal (a' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ b' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ c') +
                      ↑toNatOrdinal (a' ⨳ b' ⨳ c'))
[PROOFSTEP]
rintro ⟨b', hb, c', hc, a', ha, h⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro
a b c d b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
a' : Ordinal.{u}
ha : a' < a
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a')) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
⊢ ∃ a',
    a' < a ∧
      ∃ b',
        b' < b ∧
          ∃ c',
            c' < c ∧
              ↑toOrdinal
                  (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a') +
                    ↑toNatOrdinal (b' ⨳ c' ⨳ a)) ≤
                ↑toOrdinal
                  (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
                    ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
use a', ha, b', hb, c', hc
[GOAL]
case right
a b c d b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
a' : Ordinal.{u}
ha : a' < a
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a')) ≤
    ↑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)) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
convert h using 1
[GOAL]
case h.e'_3
a b c d b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
a' : Ordinal.{u}
ha : a' < a
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a')) ≤
    ↑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)) =
    ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a'))
[PROOFSTEP]
abel_nf
[GOAL]
case h.e'_4
a b c d b' : Ordinal.{u}
hb : b' < b
c' : Ordinal.{u}
hc : c' < c
a' : Ordinal.{u}
ha : a' < a
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (b' ⨳ c' ⨳ a) + ↑toNatOrdinal (b' ⨳ c ⨳ a') + ↑toNatOrdinal (b ⨳ c' ⨳ a')) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
⊢ ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ a') + ↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a')) =
    ↑toOrdinal
      (↑toNatOrdinal (b' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ c' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ a') +
        ↑toNatOrdinal (b' ⨳ c' ⨳ a'))
[PROOFSTEP]
abel_nf
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
a b c d b' : Ordinal.{u}
hb : b' < a
c' : Ordinal.{u}
hc : c' < b
a' : Ordinal.{u}
ha : a' < c
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b') + ↑toNatOrdinal (c' ⨳ a' ⨳ a)) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ b') + ↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b'))
⊢ ∃ a',
    a' < b ∧
      ∃ b',
        b' < c ∧
          ∃ c',
            c' < a ∧
              ↑toOrdinal
                  (↑toNatOrdinal d + ↑toNatOrdinal (a' ⨳ b' ⨳ a) + ↑toNatOrdinal (a' ⨳ c ⨳ c') +
                    ↑toNatOrdinal (b ⨳ b' ⨳ c')) ≤
                ↑toOrdinal
                  (↑toNatOrdinal (a' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ b' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ c') +
                    ↑toNatOrdinal (a' ⨳ b' ⨳ c'))
[PROOFSTEP]
use c', hc, a', ha, b', hb
[GOAL]
case right
a b c d b' : Ordinal.{u}
hb : b' < a
c' : Ordinal.{u}
hc : c' < b
a' : Ordinal.{u}
ha : a' < c
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b') + ↑toNatOrdinal (c' ⨳ a' ⨳ a)) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ b') + ↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b'))
⊢ ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ a' ⨳ a) + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b')) ≤
    ↑toOrdinal
      (↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ b') +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b'))
[PROOFSTEP]
convert h using 1
[GOAL]
case h.e'_3
a b c d b' : Ordinal.{u}
hb : b' < a
c' : Ordinal.{u}
hc : c' < b
a' : Ordinal.{u}
ha : a' < c
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b') + ↑toNatOrdinal (c' ⨳ a' ⨳ a)) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ b') + ↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b'))
⊢ ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ a' ⨳ a) + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b')) =
    ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b') + ↑toNatOrdinal (c' ⨳ a' ⨳ a))
[PROOFSTEP]
abel_nf
[GOAL]
case h.e'_4
a b c d b' : Ordinal.{u}
hb : b' < a
c' : Ordinal.{u}
hc : c' < b
a' : Ordinal.{u}
ha : a' < c
h :
  ↑toOrdinal
      (↑toNatOrdinal d + ↑toNatOrdinal (c' ⨳ c ⨳ b') + ↑toNatOrdinal (b ⨳ a' ⨳ b') + ↑toNatOrdinal (c' ⨳ a' ⨳ a)) ≤
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ b') + ↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b'))
⊢ ↑toOrdinal
      (↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) + ↑toNatOrdinal (b ⨳ c ⨳ b') +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b')) =
    ↑toOrdinal
      (↑toNatOrdinal (b ⨳ c ⨳ b') + ↑toNatOrdinal (c' ⨳ c ⨳ a) + ↑toNatOrdinal (b ⨳ a' ⨳ a) +
        ↑toNatOrdinal (c' ⨳ a' ⨳ b'))
[PROOFSTEP]
abel_nf
[GOAL]
a b c d : Ordinal.{u}
⊢ a ⨳ (b ⨳ c) ≤ d ↔
    ∀ (a' : Ordinal.{u}),
      a' < a →
        ∀ (b' : Ordinal.{u}),
          b' < b →
            ∀ (c' : Ordinal.{u}),
              c' < c →
                a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
                  d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
a b c d : Ordinal.{u}
⊢ ¬a ⨳ (b ⨳ c) ≤ d ↔
    ¬∀ (a' : Ordinal.{u}),
        a' < a →
          ∀ (b' : Ordinal.{u}),
            b' < b →
              ∀ (c' : Ordinal.{u}),
                c' < c →
                  a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
                    d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
[PROOFSTEP]
simp [lt_nmul_iff₃']
[GOAL]
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ a ⨳ b ⨳ c = a ⨳ (b ⨳ c)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ a ⨳ b ⨳ c ≤ a ⨳ (b ⨳ c)
[PROOFSTEP]
rw [nmul_le_iff₃]
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ ∀ (a' : Ordinal.{u_1}),
    a' < a →
      ∀ (b' : Ordinal.{u_1}),
        b' < b →
          ∀ (c' : Ordinal.{u_1}),
            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'
[PROOFSTEP]
intro a' ha b' hb c' hc
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
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'
[PROOFSTEP]
rw [nmul_assoc a' b c, nmul_assoc a b' c, nmul_assoc a b c', nmul_assoc a' b' c', nmul_assoc a' b' c,
  nmul_assoc a' b c', nmul_assoc a b' c']
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
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')
[PROOFSTEP]
exact nmul_nadd_lt₃' ha hb hc
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ a ⨳ (b ⨳ c) ≤ a ⨳ b ⨳ c
[PROOFSTEP]
rw [nmul_le_iff₃']
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
a b c : Ordinal.{u_1}
⊢ ∀ (a' : Ordinal.{u_1}),
    a' < a →
      ∀ (b' : Ordinal.{u_1}),
        b' < b →
          ∀ (c' : Ordinal.{u_1}),
            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')
[PROOFSTEP]
intro a' ha b' hb c' hc
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
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')
[PROOFSTEP]
rw [← nmul_assoc a' b c, ← nmul_assoc a b' c, ← nmul_assoc a b c', ← nmul_assoc a' b' c', ← nmul_assoc a' b' c, ←
  nmul_assoc a' b c', ← nmul_assoc a b' c']
[GOAL]
case a
a✝ b✝ c✝ d : Ordinal.{u}
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'
[PROOFSTEP]
exact nmul_nadd_lt₃ ha hb hc
[GOAL]
a b : Ordinal.{u_1}
⊢ a ⨳ succ b = a ⨳ b ♯ a
[PROOFSTEP]
rw [← nadd_one, nmul_nadd_one]
[GOAL]
a b : Ordinal.{u_1}
⊢ succ a ⨳ b = a ⨳ b ♯ b
[PROOFSTEP]
rw [← nadd_one, nadd_one_nmul]
[GOAL]
a b : Ordinal.{u}
⊢ a * b ≤ a ⨳ b
[PROOFSTEP]
refine b.limitRecOn ?_ ?_ ?_
[GOAL]
case refine_1
a b : Ordinal.{u}
⊢ a * 0 ≤ a ⨳ 0
[PROOFSTEP]
simp
[GOAL]
case refine_2
a b : Ordinal.{u}
⊢ ∀ (o : Ordinal.{u}), a * o ≤ a ⨳ o → a * succ o ≤ a ⨳ succ o
[PROOFSTEP]
intro c h
[GOAL]
case refine_2
a b c : Ordinal.{u}
h : a * c ≤ a ⨳ c
⊢ a * succ c ≤ a ⨳ succ c
[PROOFSTEP]
rw [mul_succ, nmul_succ]
[GOAL]
case refine_2
a b c : Ordinal.{u}
h : a * c ≤ a ⨳ c
⊢ a * c + a ≤ a ⨳ c ♯ a
[PROOFSTEP]
exact (add_le_nadd _ a).trans (nadd_le_nadd_right h a)
[GOAL]
case refine_3
a b : Ordinal.{u}
⊢ ∀ (o : Ordinal.{u}), IsLimit o → (∀ (o' : Ordinal.{u}), o' < o → a * o' ≤ a ⨳ o') → a * o ≤ a ⨳ o
[PROOFSTEP]
intro c hc H
[GOAL]
case refine_3
a b c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a * o' ≤ a ⨳ o'
⊢ a * c ≤ a ⨳ c
[PROOFSTEP]
rcases eq_zero_or_pos a with (rfl | ha)
[GOAL]
case refine_3.inl
b c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → 0 * o' ≤ 0 ⨳ o'
⊢ 0 * c ≤ 0 ⨳ c
[PROOFSTEP]
simp
[GOAL]
case refine_3.inr
a b c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a * o' ≤ a ⨳ o'
ha : 0 < a
⊢ a * c ≤ a ⨳ c
[PROOFSTEP]
have := IsNormal.blsub_eq.{u, u} (mul_isNormal ha) hc
[GOAL]
case refine_3.inr
a b c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a * o' ≤ a ⨳ o'
ha : 0 < a
this : (blsub c fun x x_1 => (fun x x_2 => x * x_2) a x) = (fun x x_1 => x * x_1) a c
⊢ a * c ≤ a ⨳ c
[PROOFSTEP]
dsimp at this 
[GOAL]
case refine_3.inr
a b c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a * o' ≤ a ⨳ o'
ha : 0 < a
this : (blsub c fun x x_1 => a * x) = a * c
⊢ a * c ≤ a ⨳ c
[PROOFSTEP]
rw [← this, blsub_le_iff]
[GOAL]
case refine_3.inr
a b c : Ordinal.{u}
hc : IsLimit c
H : ∀ (o' : Ordinal.{u}), o' < c → a * o' ≤ a ⨳ o'
ha : 0 < a
this : (blsub c fun x x_1 => a * x) = a * c
⊢ ∀ (i : Ordinal.{u}), i < c → a * i < a ⨳ c
[PROOFSTEP]
exact fun i hi => (H i hi).trans_lt (nmul_lt_nmul_of_pos_left hi ha)
