-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem iSup_nadd_of_monotone {a b} (f : Ordinal.{u} → Ordinal.{u}) (h : Monotone f) :
    ⨆ x : Iio (a ♯ b), f x = max (⨆ a' : Iio a, f (a'.1 ♯ b)) (⨆ b' : Iio b, f (a ♯ b'.1))

Proof state:
case mk.inl.intro.intro
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
i : Ordinal.{u}
hi✝ : i ∈ Iio (a ♯ b)
x : Ordinal.{u}
hx : x < a
hi : i ≤ x ♯ b
⊢ f ↑⟨i, hi✝⟩ ≤ (⨆ a', f (↑a' ♯ b)) ⊔ ⨆ b', f (a ♯ ↑b')

Tactic:
exact le_max_of_le_left ((h hi).trans <| Ordinal.le_iSup (fun x : Iio a ↦ _) ⟨x, hx⟩)

Result:
no goals

Proof state:
case mk.inr.intro.intro
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
i : Ordinal.{u}
hi✝ : i ∈ Iio (a ♯ b)
x : Ordinal.{u}
hx : x < b
hi : i ≤ a ♯ x
⊢ f ↑⟨i, hi✝⟩ ≤ (⨆ a', f (↑a' ♯ b)) ⊔ ⨆ b', f (a ♯ ↑b')

Tactic:
exact le_max_of_le_right ((h hi).trans <| Ordinal.le_iSup (fun x : Iio b ↦ _) ⟨x, hx⟩)

Result:
no goals

Proof state:
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
⊢ ∀ (i : ↑(Iio (a ♯ b))), f ↑i ≤ (⨆ a', f (↑a' ♯ b)) ⊔ ⨆ b', f (a ♯ ↑b')

Tactic:
rintro ⟨i, hi⟩

Result:
case mk
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
i : Ordinal.{u}
hi : i ∈ Iio (a ♯ b)
⊢ f ↑⟨i, hi⟩ ≤ (⨆ a', f (↑a' ♯ b)) ⊔ ⨆ b', f (a ♯ ↑b')

Proof state:
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
⊢ ⨆ x, f ↑x = (⨆ a', f (↑a' ♯ b)) ⊔ ⨆ b', f (a ♯ ↑b')

Tactic:
apply (max_le _ _).antisymm'

Result:
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
⊢ ⨆ x, f ↑x ≤ (⨆ a', f (↑a' ♯ b)) ⊔ ⨆ b', f (a ♯ ↑b')

a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
⊢ ⨆ a', f (↑a' ♯ b) ≤ ⨆ x, f ↑x

a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
⊢ ⨆ b', f (a ♯ ↑b') ≤ ⨆ x, f ↑x

Proof state:
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
⊢ ⨆ b', f (a ♯ ↑b') ≤ ⨆ x, f ↑x

Tactic:
apply csSup_le_csSup' (bddAbove_of_small _)

Result:
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
⊢ (range fun b' => f (a ♯ ↑b')) ⊆ range fun x => f ↑x

Proof state:
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
⊢ ⨆ x, f ↑x ≤ (⨆ a', f (↑a' ♯ b)) ⊔ ⨆ b', f (a ♯ ↑b')

Tactic:
rw [Ordinal.iSup_le_iff]

Result:
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
⊢ ∀ (i : ↑(Iio (a ♯ b))), f ↑i ≤ (⨆ a', f (↑a' ♯ b)) ⊔ ⨆ b', f (a ♯ ↑b')

Proof state:
case intro.mk
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
c : Ordinal.{u}
hc : c ∈ Iio b
⊢ (fun b' => f (a ♯ ↑b')) ⟨c, hc⟩ ∈ range fun x => f ↑x

Tactic:
refine mem_range_self (⟨_, ?_⟩ : Iio _)

Result:
case intro.mk
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
c : Ordinal.{u}
hc : c ∈ Iio b
⊢ a ♯ ↑⟨c, hc⟩ ∈ Iio (a ♯ b)

Proof state:
case mk
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
i : Ordinal.{u}
hi : i ∈ Iio (a ♯ b)
⊢ f ↑⟨i, hi⟩ ≤ (⨆ a', f (↑a' ♯ b)) ⊔ ⨆ b', f (a ♯ ↑b')

Tactic:
obtain ⟨x, hx, hi⟩ | ⟨x, hx, hi⟩ := lt_nadd_iff.1 hi

Result:
case mk.inl.intro.intro
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
i : Ordinal.{u}
hi✝ : i ∈ Iio (a ♯ b)
x : Ordinal.{u}
hx : x < a
hi : i ≤ x ♯ b
⊢ f ↑⟨i, hi✝⟩ ≤ (⨆ a', f (↑a' ♯ b)) ⊔ ⨆ b', f (a ♯ ↑b')

case mk.inr.intro.intro
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
i : Ordinal.{u}
hi✝ : i ∈ Iio (a ♯ b)
x : Ordinal.{u}
hx : x < b
hi : i ≤ a ♯ x
⊢ f ↑⟨i, hi✝⟩ ≤ (⨆ a', f (↑a' ♯ b)) ⊔ ⨆ b', f (a ♯ ↑b')

Proof state:
case intro.mk
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
c : Ordinal.{u}
hc : c ∈ Iio b
⊢ a ♯ ↑⟨c, hc⟩ ∈ Iio (a ♯ b)

Tactic:
apply_rules [nadd_lt_nadd_left, nadd_lt_nadd_right]

Result:
no goals

Proof state:
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
⊢ ⨆ a', f (↑a' ♯ b) ≤ ⨆ x, f ↑x

a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
⊢ ⨆ b', f (a ♯ ↑b') ≤ ⨆ x, f ↑x

Tactic:
all_goals
  apply csSup_le_csSup' (bddAbove_of_small _)
  rintro _ ⟨⟨c, hc⟩, rfl⟩
  refine mem_range_self (⟨_, ?_⟩ : Iio _)
  apply_rules [nadd_lt_nadd_left, nadd_lt_nadd_right]

Result:
no goals

Proof state:
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
⊢ (range fun b' => f (a ♯ ↑b')) ⊆ range fun x => f ↑x

Tactic:
rintro _ ⟨⟨c, hc⟩, rfl⟩

Result:
case intro.mk
a b : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : Monotone f
c : Ordinal.{u}
hc : c ∈ Iio b
⊢ (fun b' => f (a ♯ ↑b')) ⟨c, hc⟩ ∈ range fun x => f ↑x