α : Type u_1
r✝ r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : (#↑s) < StrictOrder.cof r
h : ∀ (x : Set α), x ∈ s → ¬Unbounded r x
⊢ False
α : Type u_1
r✝ r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : (#↑s) < StrictOrder.cof r
⊢ ∃ x, x ∈ s ∧ Unbounded r x
by_contra' h
α : Type u_1
r✝ r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : (#↑s) < StrictOrder.cof r
h : ∀ (x : Set α), x ∈ s → Bounded r x
⊢ False
α : Type u_1
r✝ r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : (#↑s) < StrictOrder.cof r
h : ∀ (x : Set α), x ∈ s → ¬Unbounded r x
⊢ False
simp_rw [not_unbounded_iff] at h
α : Type u_1
r✝ r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : (#↑s) < StrictOrder.cof r
h : ∀ (x : Set α), x ∈ s → Bounded r x
f : ↑s → α := fun x => WellFounded.sup (_ : WellFounded r) ↑x (_ : Bounded r ↑x)
⊢ False
α : Type u_1
r✝ r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : (#↑s) < StrictOrder.cof r
h : ∀ (x : Set α), x ∈ s → Bounded r x
⊢ False
let f : s → α := fun x : s => wo.wf.sup x (h x.1 x.2)
α : Type u_1
r✝ r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : (#↑s) < StrictOrder.cof r
h : ∀ (x : Set α), x ∈ s → Bounded r x
f : ↑s → α := fun x => WellFounded.sup (_ : WellFounded r) ↑x (_ : Bounded r ↑x)
x : α
⊢ ∃ b, b ∈ range f ∧ (swap rᶜ) x b
α : Type u_1
r✝ r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : (#↑s) < StrictOrder.cof r
h : ∀ (x : Set α), x ∈ s → Bounded r x
f : ↑s → α := fun x => WellFounded.sup (_ : WellFounded r) ↑x (_ : Bounded r ↑x)
⊢ False
refine' h₂.not_le (le_trans (csInf_le' ⟨range f, fun x => _, rfl⟩) mk_range_le)
case intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : (#↑s) < StrictOrder.cof r
h : ∀ (x : Set α), x ∈ s → Bounded r x
f : ↑s → α := fun x => WellFounded.sup (_ : WellFounded r) ↑x (_ : Bounded r ↑x)
x y : α
hxy : ¬r y x
c : Set α
hc : c ∈ s
hy : y ∈ c
⊢ ∃ b, b ∈ range f ∧ (swap rᶜ) x b
α : Type u_1
r✝ r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : (#↑s) < StrictOrder.cof r
h : ∀ (x : Set α), x ∈ s → Bounded r x
f : ↑s → α := fun x => WellFounded.sup (_ : WellFounded r) ↑x (_ : Bounded r ↑x)
x : α
⊢ ∃ b, b ∈ range f ∧ (swap rᶜ) x b
rcases h₁ x with ⟨y, ⟨c, hc, hy⟩, hxy⟩
no goals
case intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
wo : IsWellOrder α r
s : Set (Set α)
h₁ : Unbounded r (⋃₀ s)
h₂ : (#↑s) < StrictOrder.cof r
h : ∀ (x : Set α), x ∈ s → Bounded r x
f : ↑s → α := fun x => WellFounded.sup (_ : WellFounded r) ↑x (_ : Bounded r ↑x)
x y : α
hxy : ¬r y x
c : Set α
hc : c ∈ s
hy : y ∈ c
⊢ ∃ b, b ∈ range f ∧ (swap rᶜ) x b
exact ⟨f ⟨c, hc⟩, mem_range_self _, fun hxz => hxy (Trans.trans (wo.wf.lt_sup _ hy) hxz)⟩