awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  Membership.mem (γ := Set α)
    (upperBounds (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)))
    (sSup (Set.range g))
inr₁ :
  ∀ (b : α)
    (hb :
      Membership.mem (γ := Set α)
        (upperBounds (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n))) b),
    b ∈ upperBounds (Set.range g)
⊢ IsLUB (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) (sSup (Set.range g))

Tactic:
refine ⟨?_, fun b hb ↦ csSup_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 : BddAbove (Set.range g)
t : Set α
ht : t ∈ s
n : ℕ
apply :
  ¬IsCofinal.{v} (α := α)
      (Set.range fun (x : (↑s : Type v)) ↦
        f x
          (Nat.rec (motive := fun (x : ℕ) ↦ α) a
            (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) n))
apply₁ :
  Membership.mem (γ := Set α)
    (Set.range fun (x : (↑s : Type v)) ↦
      f x
        (Nat.rec (motive := fun (x : ℕ) ↦ α) a
          (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) n))
    ((fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) n)
⊢ (fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) n ≤ sSup (Set.range g)

Tactic:
apply (le_csSup (.of_not_isCofinal _) _).trans (le_csSup hg ⟨n + 1, rfl⟩)

Premises used: HAdd.hAdd, Exists.intro, LE.le.trans, 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)
t : Set α
ht : t ∈ s
n : ℕ
⊢ ¬IsCofinal.{v} (α := α)
      (Set.range fun (x : (↑s : Type v)) ↦
        f x
          (Nat.rec (motive := fun (x : ℕ) ↦ α) a
            (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) n))

Tactic:
fun hg' ↦ (cof_le hg').not_gt (mk_range_le.trans_lt hsα)

Premises used: Cardinal.mk_range_le, LE.le.not_gt, Order.cof_le, LE.le.trans_lt, Not
-- 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
n : ℕ
⊢ ¬IsCofinal.{v} (α := α)
      (Set.range fun (x : (↑s : Type v)) ↦
        f x
          (Nat.rec (motive := fun (x : ℕ) ↦ α) a
            (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) n))

Tactic:
exact fun hg' ↦ (cof_le hg').not_gt (mk_range_le.trans_lt hsα)

Premises used: Cardinal.mk_range_le, LE.le.not_gt, Order.cof_le, LE.le.trans_lt
-- 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_1 : 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
n : ℕ
w : (↑s : Type v)
h :
  Eq.{v + 1} (α := α)
    ((fun (x : (↑s : Type v)) ↦
        f x
          (Nat.rec (motive := fun (x : ℕ) ↦ α) a
            (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) n))
      (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht))
    ((fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) n)
⊢ Membership.mem (γ := Set α)
    (Set.range fun (x : (↑s : Type v)) ↦
      f x
        (Nat.rec (motive := fun (x : ℕ) ↦ α) a
          (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) n))
    ((fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) n)

Tactic:
use ⟨t, ht⟩
-- 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
b : α
hb :
  Membership.mem (γ := Set α)
    (upperBounds (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n))) b
n : ℕ
⊢ g n ≤ b

Tactic:
(hf ⟨t, ht⟩ _).2.trans <| hb ⟨_, rfl⟩

Premises used: Subtype.mk, And.right, Exists.intro, LE.le.trans, 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
b : α
hb :
  Membership.mem (γ := Set α)
    (upperBounds (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n))) b
n : ℕ
⊢ g n ≤ b

Tactic:
exact (hf ⟨t, ht⟩ _).2.trans <| hb ⟨_, rfl⟩

Premises used: Subtype.mk, And.right, Exists.intro, LE.le.trans, 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
⊢ (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) ⊆ t

Tactic:
grind
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ ∀ x ∈ Set.range f, IsClub x

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
refine : #(↑(Set.range f) : Type v) < cof α
⊢ IsClub (⋂₀ Set.range f)

Tactic:
refine IsClub.sInter hα ?_ (by simpa)

Premises used: IsClub.sInter
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
rw : lift.{u, v} #(↑(Set.range f) : Type v) < lift.{u, v} (cof α)
⊢ #(↑(Set.range f) : Type v) < cof α

Tactic:
rw [← Cardinal.lift_lt]

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ lift.{u, v} #(↑(Set.range f) : Type v) < lift.{u, v} (cof α)

Tactic:
mk_range_le_lift.trans_lt hι

Premises used: LE.le.trans_lt, Cardinal.mk_range_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ lift.{u, v} #(↑(Set.range f) : Type v) < lift.{u, v} (cof α)

Tactic:
exact mk_range_le_lift.trans_lt hι

Premises used: LE.le.trans_lt, Cardinal.mk_range_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
rw : IsClub (α := α) (⋂₀ {s, t})
⊢ IsClub (s ∩ t)

Tactic:
rw [← Set.sInter_pair]

Premises used: Set.sInter_pair
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
⊢ ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → IsClub x

Tactic:
simpa [hs]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
⊢ ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → IsClub x

Tactic:
have H : ∀ x ∈ ({s, t} : Set _), IsClub x := by simpa [hs]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
H : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → IsClub x
inl : ∀ (hα : cof α < ℵ₀), IsClub (α := α) (⋂₀ {s, t})
inr : ∀ (hα' : ℵ₀ < cof α), IsClub (α := α) (⋂₀ {s, t})
⊢ IsClub (α := α) (⋂₀ {s, t})

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 t : Set α
hα_1 : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
H : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → IsClub x
hα : cof α < ℵ₀
⊢ cof α ≤ 1

Tactic:
rw [cof_lt_aleph0_iff] at hα

Premises used: Order.cof_lt_aleph0_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα_1 : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
H : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → IsClub x
hα : cof α ≤ 1
⊢ IsClub (α := α) (⋂₀ {s, t})

Tactic:
.sInter_of_cof_le_one hα H

Premises used: IsClub.sInter_of_cof_le_one
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα_1 : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
H : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → IsClub x
hα : cof α ≤ 1
⊢ IsClub (α := α) (⋂₀ {s, t})

Tactic:
exact .sInter_of_cof_le_one hα H
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
H : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → IsClub x
hα' : ℵ₀ < cof α
⊢ #(↑{s, t} : Type v) ≤ ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
H : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → IsClub x
hα' : ℵ₀ < cof α
⊢ IsClub (α := α) (⋂₀ {s, t})

Tactic:
exact .sInter hα (hα'.trans_le' <| by simp) H
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
⊢ IsClub (Set.range f)

Tactic:
⟨hf.dirSupClosed_range, fun x ↦ ⟨_, ⟨x, rfl⟩, hf.strictMono.le_apply⟩⟩

Premises used: StrictMono.le_apply, IsClub.mk, Order.IsNormal.dirSupClosed_range, And.intro, Exists.intro, Order.IsNormal.strictMono, rfl
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
inl : IsEmpty α → IsClub (Function.fixedPoints f)
inr : Nonempty α → IsClub (Function.fixedPoints f)
⊢ IsClub (Function.fixedPoints f)

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h : IsEmpty α
⊢ IsClub (Function.fixedPoints f)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h : Nonempty α
⊢ IsClub (Function.fixedPoints f)

Tactic:
⟨fun s hs hs₀ _ a ha ↦ (hf.map_isLUB ha hs₀).unique ?_, fun a ↦ ?_⟩

Premises used: IsClub.mk, Order.IsNormal.map_isLUB, IsLUB.unique
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h : Nonempty α
inr :
  ∀ (s : Set α) (hs : s ⊆ Function.fixedPoints f) (hs₀ : s.Nonempty),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → ∀ (a : α) (ha : IsLUB s a), IsLUB (f '' s) a
inr₁ : ∀ (a : α), ∃ y ∈ Function.fixedPoints f, a ≤ y
⊢ IsClub (Function.fixedPoints f)

Tactic:
refine ⟨fun s hs hs₀ _ a ha ↦ (hf.map_isLUB ha hs₀).unique ?_, fun a ↦ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h : Nonempty α
s : Set α
hs : s ⊆ Function.fixedPoints f
hs₀ : s.Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
inr : IsLUB ((fun (a : α) ↦ a) '' s) a
inr₁ inr₂ inr₃ inr₄ : IsLUB s a
⊢ IsLUB (f '' s) a

Tactic:
rwa [Set.image_congr hs, Set.image_id']

Premises used: Set.image_id', Set.image_congr
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h_1 : Nonempty α
a : α
val : OrderTop α
h : ⊤ ∈ Function.fixedPoints f ∧ a ≤ ⊤
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y

Tactic:
use ⊤
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h : Nonempty α
a : α
val : OrderTop α
⊢ ⊤ ∈ Function.fixedPoints f ∧ a ≤ ⊤

Tactic:
simpa using hf.strictMono.id_le ⊤

Premises used: StrictMono.id_le, Top.top, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h_1 : Nonempty α
a : α
h : NoTopOrder α
⊢ NoMaxOrder α

Tactic:
rw [noTopOrder_iff_noMaxOrder] at h

Premises used: noTopOrder_iff_noMaxOrder
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h_1 : Nonempty α
a : α
h : NoMaxOrder α
inr : BddAbove.{v} (α := α) (Set.range fun (n : ℕ) ↦ f^[n] a)
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y

Tactic:
suffices BddAbove (.range fun n ↦ f^[n] a) from
        ⟨_, hf.iSup_iterate_mem_fixedPoints a this, le_csSup this ⟨0, rfl⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h_1 : Nonempty α
a : α
h : NoMaxOrder α
⊢ BddAbove.{v} (α := α) (Set.range fun (n : ℕ) ↦ f^[n] a)

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

Premises used: BddAbove.of_not_isCofinal, LT.lt.trans_le', Order.aleph0_le_cof, LE.le.not_gt, Order.cof_le, LE.le.lt_of_ne'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h_1 : Nonempty α
a : α
h : NoMaxOrder α
inr :
  ∀ (h : IsCofinal.{v} (α := α) (Set.range fun (n : ℕ) ↦ f^[n] a)), #(↑(Set.range fun (n : ℕ) ↦ f^[n] a) : Type v) ≤ ℵ₀
⊢ BddAbove.{v} (α := α) (Set.range fun (n : ℕ) ↦ f^[n] a)

Tactic:
refine .of_not_isCofinal fun h ↦ (cof_le h).not_gt
        ((aleph0_le_cof.lt_of_ne' hα).trans_le' ?_)
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h_1 : Nonempty α
a : α
h_2 : NoMaxOrder α
h : IsCofinal.{v} (α := α) (Set.range fun (n : ℕ) ↦ f^[n] a)
⊢ #(↑(Set.range fun (n : ℕ) ↦ f^[n] a) : Type v) ≤ ℵ₀

Tactic:
simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a)

Premises used: Cardinal.mk_range_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Club
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h : Nonempty α
a : α
inr : ∀ (x : OrderTop α ⊕' NoTopOrder α), ∃ y ∈ Function.fixedPoints f, a ≤ y
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y

Tactic:
cases topOrderOrNoTopOrder α with
    | inl => use ⊤; simpa using hf.strictMono.id_le ⊤
    | inr h =>
      rw [noTopOrder_iff_noMaxOrder] at h
      suffices BddAbove (.range fun n ↦ f^[n] a) from
        ⟨_, hf.iSup_iterate_mem_fixedPoints a this, le_csSup this ⟨0, rfl⟩⟩
      refine .of_not_isCofinal fun h ↦ (cof_le h).not_gt
        ((aleph0_le_cof.lt_of_ne' hα).trans_le' ?_)
      simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a)

Premises used: topOrderOrNoTopOrder, noTopOrder_iff_noMaxOrder, Cardinal.mk_range_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
⊢ (type fun (x1 x2 : ℕ) ↦ x1 < x2) ≤ (cof ℕ).ord

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Subsingleton α
inl : IsEmpty α → (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
inr : Nonempty α → (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
⊢ (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Subsingleton α
h : IsEmpty α
⊢ (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Subsingleton α
h : Nonempty α
inr : ∀ (val : Unique α), (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
⊢ (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord

Tactic:
cases nonempty_unique α

Premises used: nonempty_unique
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Subsingleton α
h : Nonempty α
val : Unique α
inr : ∀ (this : BoundedOrder α), (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
⊢ (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord

Tactic:
have := BoundedOrder.ofUnique α
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Subsingleton α
h : Nonempty α
val : Unique α
this : BoundedOrder α
⊢ (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
rw : ∀ (s : Set Ordinal.{u_2}), IsCofinal s → Cardinal.univ.{u_2, u_2 + 1} ≤ #(↑s : Type (u_2 + 1))
⊢ (type fun (x1 x2 : Ordinal.{u_2}) ↦ x1 < x2) ≤ (cof Ordinal.{u_2}).ord

Tactic:
rw [type_lt_ordinal, ← ord_univ, ord_le_ord, le_cof_iff]

Premises used: Cardinal.ord_univ, Cardinal.ord_le_ord, Ordinal.type_lt_ordinal, Order.le_cof_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
s : Set Ordinal.{u_2}
hs : IsCofinal s
contrapose! : ∀ (hs : #(↑s : Type (u_2 + 1)) < Cardinal.univ.{u_2, u_2 + 1}), ¬IsCofinal s
⊢ Cardinal.univ.{u_2, u_2 + 1} ≤ #(↑s : Type (u_2 + 1))

Tactic:
contrapose! hs
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
s : Set Ordinal.{u_2}
hs : #(↑s : Type (u_2 + 1)) < Cardinal.univ.{u_2, u_2 + 1}
⊢ Small.{u_2, u_2 + 1} (↑s : Type (u_2 + 1))

Tactic:
rw [← Cardinal.lift_id (#s), ← small_iff_lift_mk_lt_univ] at hs

Premises used: Cardinal.mk, Set.Elem, Cardinal.small_iff_lift_mk_lt_univ, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
s : Set Ordinal.{u_2}
hs : Small.{u_2, u_2 + 1} (↑s : Type (u_2 + 1))
rw : BddAbove s
⊢ ¬IsCofinal s

Tactic:
rw [not_isCofinal_iff_bddAbove]

Premises used: not_isCofinal_iff_bddAbove
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
s : Set Ordinal.{u_2}
hs : Small.{u_2, u_2 + 1} (↑s : Type (u_2 + 1))
⊢ BddAbove s

Tactic:
Ordinal.bddAbove_of_small

Premises used: Ordinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
s : Set Ordinal.{u_2}
hs : Small.{u_2, u_2 + 1} (↑s : Type (u_2 + 1))
⊢ BddAbove s

Tactic:
exact Ordinal.bddAbove_of_small

Premises used: Ordinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
apply : (cof α).ord ≤ type fun (x1 x2 : α) ↦ x1 < x2
⊢ (cof α).ord = type fun (x1 x2 : α) ↦ x1 < x2

Tactic:
apply IsRegularCardinalOrder.type_lt_le_ord_cof.antisymm'

Premises used: LE.le.antisymm', IsRegularCardinalOrder.type_lt_le_ord_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
rw : cof α ≤ #α
⊢ (cof α).ord ≤ type fun (x1 x2 : α) ↦ x1 < x2

Tactic:
rw [ord_le, card_type]

Premises used: Cardinal.ord_le, Ordinal.card_type
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
⊢ cof α ≤ #α

Tactic:
cof_le_cardinalMk α

Premises used: Order.cof_le_cardinalMk
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
⊢ cof α ≤ #α

Tactic:
exact cof_le_cardinalMk α

Premises used: Order.cof_le_cardinalMk
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
rw : cof α = (type (α := α) LT.lt).card
rw₁ : cof α = (cof α).ord.card
rw₂ rw₃ : cof α = cof α
⊢ cof α = #α

Tactic:
rw [← card_type LT.lt, ← ord_cof_eq_type_lt, card_ord]

Premises used: Ordinal.card_type, Order.ord_cof_eq_type_lt, LT.lt, Cardinal.card_ord
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : IsRegularCardinalOrder α
rw : (#α).ord = (cof α).ord
rw₁ rw₂ : (#α).ord = (#α).ord
⊢ (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2

Tactic:
rw [← ord_cof_eq_type_lt, cof_eq_cardinalMk]

Premises used: Order.cof_eq_cardinalMk, Order.ord_cof_eq_type_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum
Goal:
⊢ cof Ordinal.{u} = Cardinal.univ.{u, u + 1}

Tactic:
simp