awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
refine : ∀ (h : cof α < ℵ₀), cof α ≤ 1
⊢ cof α < ℵ₀ ↔ cof α ≤ 1

Tactic:
refine ⟨fun h ↦ ?_, (lt_of_le_of_lt · one_lt_aleph0)⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
obtain : ∀ (s : Set α) (hs : IsCofinal s) (hs' : #(↑s : Type u) = cof α), cof α ≤ 1
⊢ cof α ≤ 1

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_cof_eq α

Premises used: Order.exists_cof_eq
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
rw : #(↑s : Type u) < ℵ₀
⊢ s.Finite

Tactic:
rw [Set.Finite, ← mk_lt_aleph0_iff]

Premises used: Set.Finite, Cardinal.mk_lt_aleph0_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
⊢ #(↑s : Type u) < ℵ₀

Tactic:
hs'.trans_lt h

Premises used: Eq.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
⊢ #(↑s : Type u) < ℵ₀

Tactic:
exact hs'.trans_lt h

Premises used: Eq.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
⊢ s.Finite

Tactic:
have hf : s.Finite := by
    rw [Set.Finite, ← mk_lt_aleph0_iff]
    exact hs'.trans_lt h
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
hf : s.Finite
obtain : ∀ (t : Set α) (ht : t.Subsingleton) (ht' : IsCofinal t), cof α ≤ 1
⊢ cof α ≤ 1

Tactic:
obtain ⟨t, ht, ht'⟩ := hf.exists_subsingleton_isCofinal hs

Premises used: Set.Finite.exists_subsingleton_isCofinal
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
hf : s.Finite
t : Set α
ht : t.Subsingleton
ht' : IsCofinal t
apply : #(↑t : Type u) ≤ 1
⊢ cof α ≤ 1

Tactic:
apply (cof_le ht').trans

Premises used: Order.cof_le, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
hf : s.Finite
t : Set α
ht : t.Subsingleton
ht' : IsCofinal t
⊢ #(↑t : Type u) ≤ 1

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
⊢ ℵ₀ ≤ cof α ↔ 1 < cof α

Tactic:
simp [← not_lt]

Premises used: not_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : Nonempty α
inst_2 : NoMaxOrder α
⊢ ℵ₀ ≤ cof α

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : NoMaxOrder α
inst_2 : Nonempty α
inst_3 : Countable α
⊢ ℵ₀ ≤ cof α

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
⊢ cof ℕ = ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
rw : ∀ (s : Set α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #(↑s : Type u)
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)

Tactic:
rw [le_lift_cof_iff]

Premises used: Order.le_lift_cof_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
⊢ ∀ (s : Set α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #(↑s : Type u)

Tactic:
fun s hs ↦ (lift_le.2 <| cof_le (h.map_isCofinal hs)).trans mk_image_le_lift

Premises used: Iff.mpr, GaloisConnection.map_isCofinal, Order.cof_le, LE.le.trans, Cardinal.mk_image_le_lift, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
⊢ ∀ (s : Set α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #(↑s : Type u)

Tactic:
exact fun s hs ↦ (lift_le.2 <| cof_le (h.map_isCofinal hs)).trans mk_image_le_lift

Premises used: Iff.mpr, GaloisConnection.map_isCofinal, Order.cof_le, LE.le.trans, Cardinal.mk_image_le_lift, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α γ : Type u
inst : Preorder α
inst_1 : Preorder γ
f : γ → α
g : α → γ
h : GaloisConnection f g
⊢ cof γ ≤ cof α

Tactic:
simpa using h.cof_le_lift

Premises used: GaloisConnection.cof_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
⊢ lift.{v, u} (cof α) = lift.{u, v} (cof β)

Tactic:
f.to_galoisConnection.cof_le_lift.antisymm (f.symm.to_galoisConnection.cof_le_lift)

Premises used: OrderIso.to_galoisConnection, LE.le.antisymm, OrderIso.symm, GaloisConnection.cof_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α γ : Type u
inst : Preorder α
inst_1 : Preorder γ
f : α ≃o γ
⊢ cof α = cof γ

Tactic:
simpa using f.lift_cof_congr

Premises used: OrderIso.lift_cof_congr
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
h₂ : #(↑s : Type u_1) < cof α
contrapose! : ∀ (h₂ : ∀ (x : Set α) (_ : x ∈ s), ¬IsCofinal x), cof α ≤ #(↑s : Type u_1)
⊢ ∃ x ∈ s, IsCofinal x

Tactic:
contrapose! h₂
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
h₂ : ∀ (x : Set α) (_ : x ∈ s), ¬IsCofinal x
⊢ ∀ (x : Set α) (_ : x ∈ s), ∃ (x_1 : α), ∀ y ∈ x, y < x_1

Tactic:
simp_rw [not_isCofinal_iff] at h₂

Premises used: not_isCofinal_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
h₂ : ∀ (x : Set α) (_ : x ∈ s), ∃ (x_1 : α), ∀ y ∈ x, y < x_1
choose :
  ∀ (f : (x : Set α) → (_ : x ∈ s) → α) (hf : ∀ (x : Set α) (_ : x ∈ s), ∀ y ∈ x, y < f x _), cof α ≤ #(↑s : Type u_1)
⊢ cof α ≤ #(↑s : Type u_1)

Tactic:
choose f hf using h₂
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
f : (x : Set α) → (_ : x ∈ s) → α
hf : ∀ (x : Set α) (_ : x ∈ s), ∀ y ∈ x, y < f x _
⊢ cof α ≤ #(↑s : Type u_1)

Tactic:
(cof_le (s := range fun x ↦ f x.1 x.2) fun a ↦ ?_).trans mk_range_le

Premises used: Cardinal.mk_range_le, Order.cof_le, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
f : (x : Set α) → (_ : x ∈ s) → α
hf : ∀ (x : Set α) (_ : x ∈ s), ∀ y ∈ x, y < f x _
refine :
  ∀ (a : α), ∃ (y : α), Membership.mem (γ := Set α) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : Set α) ⋯) y ∧ a ≤ y
⊢ cof α ≤ #(↑s : Type u_1)

Tactic:
refine (cof_le (s := range fun x ↦ f x.1 x.2) fun a ↦ ?_).trans mk_range_le

Premises used: Cardinal.mk_range_le, Order.cof_le, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
f : (x : Set α) → (_ : x ∈ s) → α
hf : ∀ (x : Set α) (_ : x ∈ s), ∀ y ∈ x, y < f x _
a : α
obtain :
  ∀ (b : α) (hab : a ≤ b) (t : Set α) (ht : t ∈ s) (hb : b ∈ t),
    ∃ (y : α), Membership.mem (γ := Set α) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : Set α) ⋯) y ∧ a ≤ y
⊢ ∃ (y : α), Membership.mem (γ := Set α) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : Set α) ⋯) y ∧ a ≤ y

Tactic:
obtain ⟨b, ⟨t, ht, hb⟩, hab⟩ := h₁ a
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
f : (x : Set α) → (_ : x ∈ s) → α
hf : ∀ (x : Set α) (_ : x ∈ s), ∀ y ∈ x, y < f x _
a b : α
hab : a ≤ b
t : Set α
ht : t ∈ s
hb : b ∈ t
⊢ ∃ (y : α), Membership.mem (γ := Set α) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : Set α) ⋯) y ∧ a ≤ y

Tactic:
simpa using ⟨t, ht, hab.trans (hf t ht b hb).le⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α ι : Type u_1
inst : LinearOrder α
s : ι → Set α
h₁ : IsCofinal.{u_1} (α := α) (⋃ (i : ι), s i)
h₂ : #ι < cof α
⊢ IsCofinal (⋃₀ range s)

Tactic:
rw [← sUnion_range] at h₁

Premises used: Set.sUnion_range
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α ι : Type u_1
inst : LinearOrder α
s : ι → Set α
h₁ : IsCofinal.{u_1} (α := α) (⋃ (i : ι), s i)
h₂ : #ι < cof α
h₃ : IsCofinal (⋃₀ range s)
⊢ #ι < cof α

Tactic:
rw [← sUnion_range] at h₁

Premises used: Set.sUnion_range
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α ι : Type u_1
inst : LinearOrder α
s : ι → Set α
h₁ : IsCofinal (⋃₀ range s)
h₂ : #ι < cof α
obtain : ∀ (i : ι) (h : IsCofinal (s i)), ∃ (i : ι), IsCofinal (s i)
⊢ ∃ (i : ι), IsCofinal (s i)

Tactic:
obtain ⟨_, ⟨i, rfl⟩, h⟩ := isCofinal_of_isCofinal_sUnion h₁ (mk_range_le.trans_lt h₂)

Premises used: Cardinal.mk_range_le, isCofinal_of_isCofinal_sUnion, LE.le.trans_lt, rfl
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α ι : Type u_1
inst : LinearOrder α
s : ι → Set α
h₁ : IsCofinal (⋃₀ range s)
h₂ : #ι < cof α
i : ι
h : IsCofinal (s i)
⊢ ∃ (i : ι), IsCofinal (s i)

Tactic:
⟨i, h⟩

Premises used: Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α ι : Type u_1
inst : LinearOrder α
s : ι → Set α
h₁ : IsCofinal (⋃₀ range s)
h₂ : #ι < cof α
i : ι
h : IsCofinal (s i)
⊢ ∃ (i : ι), IsCofinal (s i)

Tactic:
exact ⟨i, h⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : IsEmpty α
s : Set α
⊢ IsClub s

Tactic:
⟨.of_isEmpty, .of_isEmpty⟩

Premises used: IsClub.mk, IsCofinal.of_isEmpty, DirSupClosed.of_isEmpty
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
⊢ IsClub.{v} (α := α) Set.univ

Tactic:
⟨.univ, .univ⟩

Premises used: IsClub.mk, DirSupClosed.univ, IsCofinal.univ
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
s t : Set α
inst : LinearOrder α
hs : IsClub s
ht : IsClub t
⊢ IsClub (s ∪ t)

Tactic:
⟨hs.dirSupClosed.union ht.dirSupClosed, hs.isCofinal.mono Set.subset_union_left⟩

Premises used: DirSupClosed.union, IsClub.dirSupClosed, IsClub.mk, Set.subset_union_left, IsCofinal.mono, IsClub.isCofinal
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
s t : Set α
x : α
inst : LinearOrder α
hs : IsClub s
ht : t ⊆ s
ht₀ : t.Nonempty
hx : IsLUB t x
⊢ x ∈ s

Tactic:
hs.dirSupClosed ht ht₀ (.of_linearOrder _) hx

Premises used: IsClub.dirSupClosed, DirectedOn.of_linearOrder
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : IsClub s
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sSup t ∈ s

Tactic:
hs.isLUB_mem ht ht₀ (isLUB_csSup ht₀ ht₁)

Premises used: IsClub.isLUB_mem, isLUB_csSup
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
inst_1 : OrderTop α
hs : ∀ x ∈ s, IsClub x
⊢ IsClub (⋂₀ s)

Tactic:
⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, ?_⟩

Premises used: IsClub.dirSupClosed, IsClub.mk, DirSupClosed.sInter
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
inst_1 : OrderTop α
hs : ∀ x ∈ s, IsClub x
refine : IsCofinal (⋂₀ s)
⊢ IsClub (⋂₀ s)

Tactic:
refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
inst_1 : OrderTop α
hs : ∀ x ∈ s, IsClub x
rw : ∀ t ∈ s, ⊤ ∈ t
⊢ IsCofinal (⋂₀ s)

Tactic:
rw [isCofinal_iff_top_mem, Set.mem_sInter]

Premises used: Set.mem_sInter, isCofinal_iff_top_mem
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
inst_1 : OrderTop α
hs : ∀ x ∈ s, IsClub x
⊢ ∀ t ∈ s, ⊤ ∈ t

Tactic:
fun x hx ↦ (hs x hx).isCofinal.top_mem

Premises used: IsCofinal.top_mem, IsClub.isCofinal
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
inst_1 : OrderTop α
hs : ∀ x ∈ s, IsClub x
⊢ ∀ t ∈ s, ⊤ ∈ t

Tactic:
exact fun x hx ↦ (hs x hx).isCofinal.top_mem

Premises used: IsCofinal.top_mem, IsClub.isCofinal
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
ι : Type u_1
f : ι → Set α
inst_1 : OrderTop α
hs : ∀ (i : ι), IsClub (f i)
⊢ ∀ x ∈ Set.range f, IsClub x

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
ι : Type u_1
f : ι → Set α
inst_1 : OrderTop α
hs : ∀ (i : ι), IsClub (f i)
⊢ IsClub (⋂₀ Set.range f)

Tactic:
exact .sInter_of_orderTop (by simpa)
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
inl : IsEmpty α → IsClub (⋂₀ s)
inr : Nonempty α → IsClub (⋂₀ s)
⊢ IsClub (⋂₀ s)

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h : IsEmpty α
⊢ IsClub (⋂₀ s)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
inr : ∀ (val : OrderTop α), IsClub (⋂₀ s)
inr₁ : NoTopOrder α → IsClub (⋂₀ s)
⊢ IsClub (⋂₀ s)

Tactic:
cases topOrderOrNoTopOrder α

Premises used: topOrderOrNoTopOrder
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
val : OrderTop α
⊢ IsClub (⋂₀ s)

Tactic:
.sInter_of_orderTop hs

Premises used: IsClub.sInter_of_orderTop
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
val : OrderTop α
⊢ IsClub (⋂₀ s)

Tactic:
exact .sInter_of_orderTop hs
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
val : NoTopOrder α
⊢ IsClub (⋂₀ s)

Tactic:
cases one_lt_cof.not_ge hα

Premises used: Order.one_lt_cof, LT.lt.not_ge
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
ι : Type u_1
f : ι → Set α
hα : cof α ≤ 1
hs : ∀ (i : ι), IsClub (f i)
⊢ ∀ x ∈ Set.range f, IsClub x

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
ι : Type u_1
f : ι → Set α
hα : cof α ≤ 1
hs : ∀ (i : ι), IsClub (f i)
⊢ IsClub (⋂₀ Set.range f)

Tactic:
exact .sInter_of_cof_le_one hα (by simpa)
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
inl : IsEmpty α → IsClub (⋂₀ s)
inr : Nonempty α → IsClub (⋂₀ s)
⊢ IsClub (⋂₀ s)

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : IsEmpty α
⊢ IsClub (⋂₀ s)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
inr : ∀ (hα : cof α < ℵ₀), IsClub (⋂₀ s)
inr₁ : ∀ (hα : ℵ₀ < cof α), IsClub (⋂₀ s)
⊢ IsClub (⋂₀ s)

Tactic:
obtain hα | hα := hα.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : cof α < ℵ₀
⊢ IsClub (⋂₀ s)

Tactic:
.sInter_of_cof_le_one (cof_lt_aleph0_iff.1 hα) hs

Premises used: Iff.mp, Order.cof_lt_aleph0_iff, IsClub.sInter_of_cof_le_one
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : cof α < ℵ₀
⊢ IsClub (⋂₀ s)

Tactic:
exact .sInter_of_cof_le_one (cof_lt_aleph0_iff.1 hα) hs
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
⊢ IsClub (⋂₀ s)

Tactic:
⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, fun a ↦ ?_⟩

Premises used: IsClub.dirSupClosed, IsClub.mk, DirSupClosed.sInter
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
inr : ∀ (a : α), ∃ y ∈ ⋂₀ s, a ≤ y
⊢ IsClub (⋂₀ s)

Tactic:
refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, fun a ↦ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
inr :
  ∀ (f : (x : (↑s : Type v)) → (x : α) → α)
    (hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1), ∃ y ∈ ⋂₀ s, a ≤ y
⊢ ∃ y ∈ ⋂₀ s, a ≤ y

Tactic:
choose f hf using fun x : s ↦ (hs _ x.2).isCofinal

Premises used: Subtype.val, IsClub.isCofinal, Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
⊢ BddAbove (Set.range g)

Tactic:
.of_not_isCofinal fun hg ↦ (cof_le hg).not_gt (hα.trans_le' ?_)

Premises used: BddAbove.of_not_isCofinal, LT.lt.trans_le', LE.le.not_gt, Order.cof_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
refine : ∀ (hg : IsCofinal (Set.range g)), #(↑(Set.range g) : Type v) ≤ ℵ₀
⊢ BddAbove (Set.range g)

Tactic:
refine .of_not_isCofinal fun hg ↦ (cof_le hg).not_gt (hα.trans_le' ?_)
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : IsCofinal (Set.range g)
⊢ #(↑(Set.range g) : Type v) ≤ ℵ₀

Tactic:
simpa using mk_range_le_lift (f := g)

Premises used: Cardinal.mk_range_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
⊢ BddAbove (Set.range g)

Tactic:
have hg : BddAbove (.range g) := by
    refine .of_not_isCofinal fun hg ↦ (cof_le hg).not_gt (hα.trans_le' ?_)
    simpa using mk_range_le_lift (f := g)
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
⊢ ∃ y ∈ ⋂₀ s, a ≤ y

Tactic:
⟨_, fun t ht ↦ ?_, le_csSup hg ⟨0, rfl⟩⟩

Premises used: And.intro, Exists.intro, le_csSup, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
inr : ∀ (t : Set α) (ht : t ∈ s), sSup (Set.range g) ∈ t
⊢ ∃ y ∈ ⋂₀ s, a ≤ y

Tactic:
refine ⟨_, fun t ht ↦ ?_, le_csSup hg ⟨0, rfl⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
t : Set α
ht : t ∈ s
inr : IsLUB (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) (sSup (Set.range g))
apply : (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) ⊆ t
⊢ sSup (Set.range g) ∈ t

Tactic:
apply (hs t ht).isLUB_mem (t := .range fun n ↦ f ⟨t, ht⟩ (g n)) _ (Set.range_nonempty _)

Premises used: Set.range_nonempty, IsClub.isLUB_mem
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
t : Set α
ht : t ∈ s
⊢ IsLUB (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) (sSup (Set.range g))

Tactic:
⟨?_, fun b hb ↦ csSup_le' ?_⟩

Premises used: csSup_le', IsLeast, And.intro, IsLUB