α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
⊢ ∀ (i : α ⊕ β), f i ≤ max (sup fun a => f (Sum.inl a)) (sup fun b => f (Sum.inr b))

α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
⊢ (sup fun a => f (Sum.inl a)) ≤ sup f

α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
⊢ (sup fun b => f (Sum.inr b)) ≤ sup f
α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
⊢ sup f = max (sup fun a => f (Sum.inl a)) (sup fun b => f (Sum.inr b))
apply (sup_le_iff.2 _).antisymm (max_le_iff.2 ⟨_, _⟩)
no goals
α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
⊢ (sup fun a => f (Sum.inl a)) ≤ sup f

α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
⊢ (sup fun b => f (Sum.inr b)) ≤ sup f
all_goals
  apply sup_le_of_range_subset.{_, max u v, w}
  rintro i ⟨a, rfl⟩
  apply mem_range_self
case inl
α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
i : α
⊢ f (Sum.inl i) ≤ max (sup fun a => f (Sum.inl a)) (sup fun b => f (Sum.inr b))

case inr
α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
i : β
⊢ f (Sum.inr i) ≤ max (sup fun a => f (Sum.inl a)) (sup fun b => f (Sum.inr b))
α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
⊢ ∀ (i : α ⊕ β), f i ≤ max (sup fun a => f (Sum.inl a)) (sup fun b => f (Sum.inr b))
rintro (i | i)
no goals
case inl
α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
i : α
⊢ f (Sum.inl i) ≤ max (sup fun a => f (Sum.inl a)) (sup fun b => f (Sum.inr b))
exact le_max_of_le_left (le_sup _ i)
no goals
case inr
α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
i : β
⊢ f (Sum.inr i) ≤ max (sup fun a => f (Sum.inl a)) (sup fun b => f (Sum.inr b))
exact le_max_of_le_right (le_sup _ i)
α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
⊢ (range fun b => f (Sum.inr b)) ⊆ range f
α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
⊢ (sup fun b => f (Sum.inr b)) ≤ sup f
apply sup_le_of_range_subset.{_, max u v, w}
case intro
α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
a : β
⊢ (fun b => f (Sum.inr b)) a ∈ range f
α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
⊢ (range fun b => f (Sum.inr b)) ⊆ range f
rintro i ⟨a, rfl⟩
no goals
case intro
α✝ : Type ?u.289176
β✝ : Type ?u.289179
γ : Type ?u.289182
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
f : α ⊕ β → Ordinal
a : β
⊢ (fun b => f (Sum.inr b)) a ∈ range f
apply mem_range_self