a✝ b✝ c✝ : Ordinal
a b c : Ordinal
⊢ 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')))

case hf
a✝ b✝ c✝ : Ordinal
a b c : Ordinal
⊢ ∀ {i j : Ordinal}, i < b ♯ c → j < b ♯ c → i ≤ j → a ♯ i ≤ a ♯ j

case hf
a✝ b✝ c✝ : Ordinal
a b c : Ordinal
⊢ ∀ {i j : Ordinal}, i < a ♯ b → j < a ♯ b → i ≤ j → i ♯ c ≤ j ♯ c
a✝ b✝ c✝ : Ordinal
a b c : Ordinal
⊢ a ♯ b ♯ c = a ♯ (b ♯ c)
rw [nadd_def a (b ♯ c), nadd_def, blsub_nadd_of_mono, blsub_nadd_of_mono, max_assoc]
no goals
a✝ b✝ c✝ : Ordinal
a b c : Ordinal
⊢ 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')))
congr <;> ext (d hd) <;> apply nadd_assoc
no goals
case hf
a✝ b✝ c✝ : Ordinal
a b c : Ordinal
⊢ ∀ {i j : Ordinal}, i < b ♯ c → j < b ♯ c → i ≤ j → a ♯ i ≤ a ♯ j
exact fun  _ _ h => nadd_le_nadd_left h a
no goals
case hf
a✝ b✝ c✝ : Ordinal
a b c : Ordinal
⊢ ∀ {i j : Ordinal}, i < a ♯ b → j < a ♯ b → i ≤ j → i ♯ c ≤ j ♯ c
exact fun  _ _ h => nadd_le_nadd_right h c