-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem blsub_nadd_of_mono {f : ∀ c < a ♯ b, Ordinal.{max u v}}
    (hf : ∀ {i j} (hi hj), i ≤ j → f i hi ≤ f j hj) :
    blsub.{u,v} _ f =
      max (blsub.{u, v} a fun a' ha' => f (a' ♯ b) <| nadd_lt_nadd_right ha' b)
        (blsub.{u, v} b fun b' hb' => f (a ♯ b') <| nadd_lt_nadd_left hb' a)

Proof state:
a b : 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
⊢ (a.blsub fun a' ha' => f (a' ♯ b) ⋯) ≤ (a ♯ b).blsub f

a b : 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
⊢ (b.blsub fun b' hb' => f (a ♯ b') ⋯) ≤ (a ♯ b).blsub f

Tactic:
all_goals
  apply blsub_le_of_brange_subset.{u, u, v}
  rintro c ⟨d, hd, rfl⟩
  apply mem_brange_self

Result:
no goals

Proof state:
a b : 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
⊢ (a ♯ b).blsub f = (a.blsub fun a' ha' => f (a' ♯ b) ⋯) ⊔ b.blsub fun b' hb' => f (a ♯ b') ⋯

Tactic:
apply (blsub_le_iff.2 fun i h => _).antisymm (max_le _ _)

Result:
a b : 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 < (a.blsub fun a' ha' => f (a' ♯ b) ⋯) ⊔ b.blsub fun b' hb' => f (a ♯ b') ⋯

a b : 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
⊢ (a.blsub fun a' ha' => f (a' ♯ b) ⋯) ≤ (a ♯ b).blsub f

a b : 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
⊢ (b.blsub fun b' hb' => f (a ♯ b') ⋯) ≤ (a ♯ b).blsub f

Proof state:
a b : 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
⊢ (b.brange fun b' hb' => f (a ♯ b') ⋯) ⊆ (a ♯ b).brange f

Tactic:
rintro c ⟨d, hd, rfl⟩

Result:
case intro.intro
a b : 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 b' hb' => f (a ♯ b') ⋯) d hd ∈ (a ♯ b).brange f

Proof state:
case intro.intro
a b : 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 b' hb' => f (a ♯ b') ⋯) d hd ∈ (a ♯ b).brange f

Tactic:
apply mem_brange_self

Result:
no goals

Proof state:
case inr.intro.intro
a b : 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 < (a.blsub fun a' ha' => f (a' ♯ b) ⋯) ⊔ b.blsub fun b' hb' => f (a ♯ b') ⋯

Tactic:
exact lt_max_of_lt_right ((hf h (nadd_lt_nadd_left hb' a) hi).trans_lt (lt_blsub _ _ hb'))

Result:
no goals

Proof state:
a b : 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 < (a.blsub fun a' ha' => f (a' ♯ b) ⋯) ⊔ b.blsub fun b' hb' => f (a ♯ b') ⋯

Tactic:
rcases lt_nadd_iff.1 h with (⟨a', ha', hi⟩ | ⟨b', hb', hi⟩)

Result:
case inl.intro.intro
a b : 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 < (a.blsub fun a' ha' => f (a' ♯ b) ⋯) ⊔ b.blsub fun b' hb' => f (a ♯ b') ⋯

case inr.intro.intro
a b : 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 < (a.blsub fun a' ha' => f (a' ♯ b) ⋯) ⊔ b.blsub fun b' hb' => f (a ♯ b') ⋯

Proof state:
a b : 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 < (a.blsub fun a' ha' => f (a' ♯ b) ⋯) ⊔ b.blsub fun b' hb' => f (a ♯ b') ⋯

Tactic:
intro i h

Result:
a b : 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 < (a.blsub fun a' ha' => f (a' ♯ b) ⋯) ⊔ b.blsub fun b' hb' => f (a ♯ b') ⋯

Proof state:
case inl.intro.intro
a b : 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 < (a.blsub fun a' ha' => f (a' ♯ b) ⋯) ⊔ b.blsub fun b' hb' => f (a ♯ b') ⋯

Tactic:
exact lt_max_of_lt_left ((hf h (nadd_lt_nadd_right ha' b) hi).trans_lt (lt_blsub _ _ ha'))

Result:
no goals

Proof state:
a b : 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
⊢ (b.blsub fun b' hb' => f (a ♯ b') ⋯) ≤ (a ♯ b).blsub f

Tactic:
apply blsub_le_of_brange_subset.{u, u, v}

Result:
a b : 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
⊢ (b.brange fun b' hb' => f (a ♯ b') ⋯) ⊆ (a ♯ b).brange f