α✝ : Type ?u.108841
r✝ : α✝ → α✝ → Prop
α β : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : β → Set α
h₁ : Unbounded r (⋃₀ range fun x => s x)
h₂ : (#β) < StrictOrder.cof r
⊢ ∃ x, Unbounded r (s x)
α✝ : Type ?u.108841
r✝ : α✝ → α✝ → Prop
α β : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : β → Set α
h₁ : Unbounded r (⋃ (x : β), s x)
h₂ : (#β) < StrictOrder.cof r
⊢ ∃ x, Unbounded r (s x)
rw [← sUnion_range] at h₁
case intro.intro.intro
α✝ : Type ?u.108841
r✝ : α✝ → α✝ → Prop
α β : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : β → Set α
h₁ : Unbounded r (⋃₀ range fun x => s x)
h₂ : (#β) < StrictOrder.cof r
x : β
u : Unbounded r ((fun x => s x) x)
⊢ ∃ x, Unbounded r (s x)
α✝ : Type ?u.108841
r✝ : α✝ → α✝ → Prop
α β : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : β → Set α
h₁ : Unbounded r (⋃₀ range fun x => s x)
h₂ : (#β) < StrictOrder.cof r
⊢ ∃ x, Unbounded r (s x)
rcases unbounded_of_unbounded_sUnion r h₁ (mk_range_le.trans_lt h₂) with ⟨_, ⟨x, rfl⟩, u⟩
no goals
case intro.intro.intro
α✝ : Type ?u.108841
r✝ : α✝ → α✝ → Prop
α β : Type u
r : α → α → Prop
wo : IsWellOrder α r
s : β → Set α
h₁ : Unbounded r (⋃₀ range fun x => s x)
h₂ : (#β) < StrictOrder.cof r
x : β
u : Unbounded r ((fun x => s x) x)
⊢ ∃ x, Unbounded r (s x)
exact ⟨x, u⟩