-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem iSup_sum {α β} (f : α ⊕ β → Ordinal.{u}) [Small.{u} α] [Small.{u} β]:
    iSup f = max (⨆ a, f (Sum.inl a)) (⨆ b, f (Sum.inr b))

Proof state:
case intro
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
a : β
⊢ (fun b => f (Sum.inr b)) a ∈ range f

Tactic:
apply mem_range_self

Result:
no goals

Proof state:
case inr
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
i : β
⊢ f (Sum.inr i) ≤ (⨆ a, f (Sum.inl a)) ⊔ ⨆ b, f (Sum.inr b)

Tactic:
exact le_max_of_le_right (Ordinal.le_iSup (fun x ↦ f (Sum.inr x)) i)

Result:
no goals

Proof state:
case inl
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
i : α
⊢ f (Sum.inl i) ≤ (⨆ a, f (Sum.inl a)) ⊔ ⨆ b, f (Sum.inr b)

Tactic:
exact le_max_of_le_left (Ordinal.le_iSup (fun x ↦ f (Sum.inl x)) i)

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
⊢ iSup f = (⨆ a, f (Sum.inl a)) ⊔ ⨆ b, f (Sum.inr b)

Tactic:
apply (Ordinal.iSup_le _).antisymm (max_le _ _)

Result:
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
⊢ ∀ (i : α ⊕ β), f i ≤ (⨆ a, f (Sum.inl a)) ⊔ ⨆ b, f (Sum.inr b)

α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
⊢ ⨆ a, f (Sum.inl a) ≤ iSup f

α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
⊢ ⨆ b, f (Sum.inr b) ≤ iSup f

Proof state:
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
⊢ ∀ (i : α ⊕ β), f i ≤ (⨆ a, f (Sum.inl a)) ⊔ ⨆ b, f (Sum.inr b)

Tactic:
rintro (i | i)

Result:
case inl
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
i : α
⊢ f (Sum.inl i) ≤ (⨆ a, f (Sum.inl a)) ⊔ ⨆ b, f (Sum.inr b)

case inr
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
i : β
⊢ f (Sum.inr i) ≤ (⨆ a, f (Sum.inl a)) ⊔ ⨆ b, f (Sum.inr b)

Proof state:
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
⊢ (range fun b => f (Sum.inr b)) ⊆ range f

Tactic:
rintro i ⟨a, rfl⟩

Result:
case intro
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
a : β
⊢ (fun b => f (Sum.inr b)) a ∈ range f

Proof state:
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
⊢ ⨆ a, f (Sum.inl a) ≤ iSup f

α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
⊢ ⨆ b, f (Sum.inr b) ≤ iSup f

Tactic:
all_goals
  apply csSup_le_csSup' (bddAbove_of_small _)
  rintro i ⟨a, rfl⟩
  apply mem_range_self

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
⊢ ⨆ b, f (Sum.inr b) ≤ iSup f

Tactic:
apply csSup_le_csSup' (bddAbove_of_small _)

Result:
α : Type u_4
β : Type u_5
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_4} α
inst✝ : Small.{u, u_5} β
⊢ (range fun b => f (Sum.inr b)) ⊆ range f