awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
h : 3 ≤ #α
x y : α
this : (↑3 : Cardinal.{u_1}) ≤ #α
⊢ (↑2 : Cardinal.{u_1}) < #α

Tactic:
have : ↑(2 : ℕ) < #α := by rwa [← natCast_add_one_le_iff, ← Nat.cast_add_one]
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
h : 3 ≤ #α
x y : α
this_1 : (↑3 : Cardinal.{u_1}) ≤ #α
this : (↑2 : Cardinal.{u_1}) < #α
⊢ ∃ (z : α), z ∉ [x, y]

Tactic:
have := exists_notMem_of_length_lt [x, y] this
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
h : 3 ≤ #α
x y : α
this_1 : (↑3 : Cardinal.{u_1}) ≤ #α
this_2 : (↑2 : Cardinal.{u_1}) < #α
this : ∃ (z : α), z ∉ [x, y]
⊢ ∃ (z : α), z ≠ x ∧ z ≠ y

Tactic:
simpa [not_or] using this

Premises used: not_or
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
b c a : Cardinal.{u}
h : c < b
⊢ a ^ c ≤ a ^< b

Tactic:
le_ciSup (f := fun y : Iio b => a ^ (y : Cardinal)) ?_ ⟨c, h⟩

Premises used: Cardinal.powerlt, Subtype.mk, le_ciSup
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
b c a : Cardinal.{u}
h : c < b
refine : BddAbove.{u + 1} (α := Cardinal.{u}) (range fun (y : (↑(Iio b) : Type (u + 1))) ↦ a ^ (↑y : Cardinal.{u}))
⊢ a ^ c ≤ a ^< b

Tactic:
refine le_ciSup (f := fun y : Iio b => a ^ (y : Cardinal)) ?_ ⟨c, h⟩

Premises used: Subtype.mk, le_ciSup
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
b c a : Cardinal.{u}
h : c < b
rw : BddAbove (HPow.hPow a '' Iio b)
⊢ BddAbove.{u + 1} (α := Cardinal.{u}) (range fun (y : (↑(Iio b) : Type (u + 1))) ↦ a ^ (↑y : Cardinal.{u}))

Tactic:
rw [← image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (HPow.hPow a '' Iio b)

Tactic:
bddAbove_image.{u, u} _ bddAbove_Iio

Premises used: bddAbove_Iio, Cardinal.bddAbove_image
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (HPow.hPow a '' Iio b)

Tactic:
exact bddAbove_image.{u, u} _ bddAbove_Iio
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b c : Cardinal.{u}
rw : (∀ (i : (↑(Iio b) : Type (u + 1))), a ^ (↑i : Cardinal.{u}) ≤ c) ↔ ∀ x < b, a ^ x ≤ c
h : BddAbove.{u + 1} (α := Cardinal.{u}) (range fun (c : (↑(Iio b) : Type (u + 1))) ↦ a ^ (↑c : Cardinal.{u}))
⊢ a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c

Tactic:
rw [powerlt, ciSup_le_iff']

Premises used: ciSup_le_iff', Cardinal.powerlt
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b c : Cardinal.{u}
⊢ (∀ (i : (↑(Iio b) : Type (u + 1))), a ^ (↑i : Cardinal.{u}) ≤ c) ↔ ∀ x < b, a ^ x ≤ c

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b c : Cardinal.{u}
h : BddAbove (HPow.hPow a '' Iio b)
⊢ BddAbove.{u + 1} (α := Cardinal.{u}) (range fun (c : (↑(Iio b) : Type (u + 1))) ↦ a ^ (↑c : Cardinal.{u}))

Tactic:
rw [← image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b c : Cardinal.{u}
⊢ BddAbove (HPow.hPow a '' Iio b)

Tactic:
bddAbove_image.{u, u} _ bddAbove_Iio

Premises used: bddAbove_Iio, Cardinal.bddAbove_image
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b c : Cardinal.{u}
⊢ BddAbove (HPow.hPow a '' Iio b)

Tactic:
exact bddAbove_image.{u, u} _ bddAbove_Iio
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b c : Cardinal.{u_1}
h : b ≤ c
⊢ a ^< b ≤ a ^< c

Tactic:
powerlt_le.2 fun _ hx => le_powerlt a <| hx.trans_le h

Premises used: Iff.mpr, Cardinal.le_powerlt, Cardinal.powerlt_le, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
⊢ Monotone (β := Cardinal.{u_1}) fun (c : Cardinal.{u_1}) ↦ a ^< c

Tactic:
fun _ _ => powerlt_le_powerlt_left

Premises used: Cardinal.powerlt_le_powerlt_left, Monotone
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a ≠ 0
⊢ a ^< succ b = a ^ b

Tactic:
(powerlt_le.2 fun _ h' => power_le_power_left h <| le_of_lt_succ h').antisymm <|
    le_powerlt a (lt_succ b)

Premises used: Iff.mpr, LE.le.antisymm, Order.lt_succ, Cardinal.le_powerlt, Cardinal.powerlt_le, Cardinal.power_le_power_left, Order.le_of_lt_succ
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b c : Cardinal.{u_1}
⊢ a ^< min b c = min (a ^< b) (a ^< c)

Tactic:
(powerlt_mono_left a).map_min

Premises used: Cardinal.powerlt_mono_left, Monotone.map_min
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b c : Cardinal.{u_1}
⊢ a ^< max b c = max (a ^< b) (a ^< c)

Tactic:
(powerlt_mono_left a).map_max

Premises used: Monotone.map_max, Cardinal.powerlt_mono_left
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
h : a ≠ 0
apply : 1 ≤ 0 ^< a
⊢ 0 ^< a = 1

Tactic:
apply (powerlt_le.2 fun c _ => zero_power_le _).antisymm

Premises used: Iff.mpr, Cardinal.zero_power_le, LE.le.antisymm, Cardinal.powerlt_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
h : a ≠ 0
rw : HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) 0 0 ≤ 0 ^< a
rw₁ : Cardinal.{u_1}
⊢ 1 ≤ 0 ^< a

Tactic:
rw [← power_zero]

Premises used: Cardinal.power_zero
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
h : a ≠ 0
⊢ HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) 0 0 ≤ 0 ^< a

Tactic:
le_powerlt 0 (pos_iff_ne_zero.2 h)

Premises used: Iff.mpr, Cardinal.le_powerlt, OfNat.ofNat, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (⨆ (c : (↑(Iio 0) : Type (u_1 + 1))), a ^ (↑c : Cardinal.{u_1})) 0

Tactic:
Cardinal.iSup_of_empty _

Premises used: Cardinal.iSup_of_empty
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
convert_3 : IsEmpty.{u_1 + 2} (↑(Iio 0) : Type (u_1 + 1))
⊢ a ^< 0 = 0

Tactic:
convert! Cardinal.iSup_of_empty _

Premises used: Cardinal.iSup_of_empty
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
⊢ IsEmpty.{u_1 + 2} (↑(Iio 0) : Type (u_1 + 1))

Tactic:
Subtype.isEmpty_of_false fun x => mem_Iio.not.mpr not_lt_zero

Premises used: Iff.mpr, Set.mem_Iio, Iff.not, Subtype.isEmpty_of_false, not_lt_zero
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
⊢ IsEmpty.{u_1 + 2} (↑(Iio 0) : Type (u_1 + 1))

Tactic:
exact Subtype.isEmpty_of_false fun x => mem_Iio.not.mpr not_lt_zero

Premises used: Iff.mpr, Set.mem_Iio, Iff.not, Subtype.isEmpty_of_false, not_lt_zero
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
r : α → α → Prop
wf : WellFounded r
s : Set α
hs : sᶜ.Nonempty
⊢ #{ x : α // r x (wf.min (r := r) sᶜ hs) } ≤ #(↑s : Type u)

Tactic:
Cardinal.mk_le_mk_of_subset fun _ ↦ wf.mem_of_lt_min_compl

Premises used: Set.Mem, WellFounded.mem_of_lt_min_compl, Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
s : Set α
h : IsCofinal s
⊢ cof α ≤ #(↑s : Type u)

Tactic:
ciInf_le' (ι := {s : Set α // IsCofinal s}) _ ⟨s, h⟩

Premises used: ciInf_le', Subtype.mk, Order.cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
c : Cardinal.{max u v}
rw :
  (∀ (i : { s : Set α // IsCofinal s }), c ≤ lift.{v, u} #(↑(↑i : Set α) : Type u)) ↔
    ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #(↑s : Type u)
⊢ c ≤ lift.{v, u} (cof α) ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #(↑s : Type u)

Tactic:
rw [cof, lift_iInf, le_ciInf_iff']

Premises used: Cardinal.lift_iInf, le_ciInf_iff', Order.cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
c : Cardinal.{max u v}
⊢ (∀ (i : { s : Set α // IsCofinal s }), c ≤ lift.{v, u} #(↑(↑i : Set α) : Type u)) ↔
    ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #(↑s : Type u)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
c : Cardinal.{u}
⊢ c ≤ cof α ↔ ∀ (s : Set α), IsCofinal s → c ≤ #(↑s : Type u)

Tactic:
simpa using @le_lift_cof_iff.{u, u} α _ c
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
obtain :
  ∀ (s : { s : Set α // IsCofinal s })
    (hs :
      Eq.{u + 2} (α := Cardinal.{u}) ((fun (s : { s : Set α // IsCofinal s }) ↦ mk.{u} (↑(↑s : Set α) : Type u)) s)
        (⨅ (s : { s : Set α // IsCofinal s }), #(↑(↑s : Set α) : Type u))),
    ∃ (s : Set α), IsCofinal s ∧ #(↑s : Type u) = cof α
⊢ ∃ (s : Set α), IsCofinal s ∧ #(↑s : Type u) = cof α

Tactic:
obtain ⟨s, hs⟩ := ciInf_mem fun s : {s : Set α // IsCofinal s} ↦ #s

Premises used: Cardinal.mk, ciInf_mem, Set.Elem, Subtype.val
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
s : { s : Set α // IsCofinal s }
hs :
  Eq.{u + 2} (α := Cardinal.{u}) ((fun (s : { s : Set α // IsCofinal s }) ↦ mk.{u} (↑(↑s : Set α) : Type u)) s)
    (⨅ (s : { s : Set α // IsCofinal s }), #(↑(↑s : Set α) : Type u))
⊢ ∃ (s : Set α), IsCofinal s ∧ #(↑s : Type u) = cof α

Tactic:
⟨s.1, s.2, hs⟩

Premises used: And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
s : { s : Set α // IsCofinal s }
hs :
  Eq.{u + 2} (α := Cardinal.{u}) ((fun (s : { s : Set α // IsCofinal s }) ↦ mk.{u} (↑(↑s : Set α) : Type u)) s)
    (⨅ (s : { s : Set α // IsCofinal s }), #(↑(↑s : Set α) : Type u))
⊢ ∃ (s : Set α), IsCofinal s ∧ #(↑s : Type u) = cof α

Tactic:
exact ⟨s.1, s.2, hs⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
⊢ cof α ≤ #α

Tactic:
cof_le .univ |>.trans_eq mk_univ

Premises used: LE.le.trans_eq, Cardinal.mk_univ, Order.cof_le, IsCofinal.univ
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : IsEmpty α
⊢ cof α = 0

Tactic:
simp [cof]

Premises used: Order.cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
refine : cof α = 0 → IsEmpty α
⊢ cof α = 0 ↔ IsEmpty α

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ by simp [cof]⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : cof α = 0
obtain : ∀ (s : Set α) (hs : IsCofinal s) (hs' : #(↑s : Type u) = cof α), IsEmpty α
⊢ IsEmpty α

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

Premises used: Order.exists_cof_eq
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : cof α = 0
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
⊢ IsEmpty α

Tactic:
simp_all [mk_eq_zero_iff, isCofinal_empty_iff]

Premises used: Cardinal.mk_eq_zero_iff, isCofinal_empty_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : IsEmpty α
⊢ cof α = 0

Tactic:
cof_eq_zero_iff.2 h

Premises used: Iff.mpr, Order.cof_eq_zero_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
⊢ cof α ≠ 0 ↔ Nonempty α

Tactic:
simpa using cof_eq_zero_iff.not

Premises used: Order.cof_eq_zero_iff, Iff.not
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : Nonempty α
⊢ cof α ≠ 0

Tactic:
cof_ne_zero_iff.2 h

Premises used: Iff.mpr, Order.cof_ne_zero_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
⊢ cof α = 1 ↔ ∃ (x : α), IsTop x

Tactic:
⟨fun h ↦ ?_, fun ⟨t, ht⟩ ↦ ?_⟩

Premises used: _private.0.Order.cof_eq_one_iff.match_1, Iff.intro, Order.cof, OfNat.ofNat, Eq
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
refine_1 : ∀ (h : cof α = 1), ∃ (x : α), IsTop x
refine_2 : (∃ (x : α), IsTop x) → ∀ (t : α) (ht : IsTop t), cof α = 1
⊢ cof α = 1 ↔ ∃ (x : α), IsTop x

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨t, ht⟩ ↦ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : cof α = 1
refine_1 : ∀ (s : Set α) (hs : IsCofinal s) (hs' : #(↑s : Type u) = cof α), ∃ (x : α), IsTop x
⊢ ∃ (x : α), IsTop x

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

Premises used: Order.exists_cof_eq
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : cof α = 1
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
⊢ ∃ (x : α), s = {x}

Tactic:
rw [h, mk_set_eq_one_iff] at hs'

Premises used: Cardinal.mk_set_eq_one_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : cof α = 1
s : Set α
hs : IsCofinal s
hs' : ∃ (x : α), s = {x}
refine_1 : ∀ (t : α) (hs : IsCofinal (α := α) {t}), ∃ (x : α), IsTop x
⊢ ∃ (x : α), IsTop x

Tactic:
obtain ⟨t, rfl⟩ := hs'

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : cof α = 1
t : α
hs : IsCofinal (α := α) {t}
h₁ : IsTop t
⊢ ∃ (x : α), IsTop x

Tactic:
use t
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : cof α = 1
t : α
hs : IsCofinal (α := α) {t}
h₁ h₂ h₃ h₄ : ∀ (hs : IsTop t), IsTop t
⊢ IsTop t

Tactic:
rwa [isCofinal_singleton_iff] at hs

Premises used: isCofinal_singleton_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : ∃ (x : α), IsTop x
t : α
ht : IsTop t
refine_2 : cof α ≤ 1
refine_2₁ : 1 ≤ cof α
⊢ cof α = 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : ∃ (x : α), IsTop x
t : α
ht : IsTop t
apply : IsCofinal (α := α) {t}
⊢ cof α ≤ 1

Tactic:
apply (cof_le (s := {t}) _).trans_eq (mk_singleton _)

Premises used: LE.le.trans_eq, Order.cof_le, Cardinal.mk_singleton
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : ∃ (x : α), IsTop x
t : α
ht rwa rwa₁ rwa₂ rwa₃ : IsTop t
⊢ IsCofinal (α := α) {t}

Tactic:
rwa [isCofinal_singleton_iff]

Premises used: isCofinal_singleton_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : ∃ (x : α), IsTop x
t : α
ht : IsTop t
refine_2 : Nonempty α
⊢ 1 ≤ cof α

Tactic:
rw [Cardinal.one_le_iff_ne_zero, cof_ne_zero_iff]

Premises used: Cardinal.one_le_iff_ne_zero, Order.cof_ne_zero_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : ∃ (x : α), IsTop x
t : α
ht : IsTop t
val : α
⊢ Nonempty α

Tactic:
use t
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : OrderTop α
⊢ cof α = 1

Tactic:
cof_eq_one_iff.2 ⟨⊤, isTop_top⟩

Premises used: Iff.mpr, Order.cof_eq_one_iff, Exists.intro, Top.top, isTop_top
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
rw : (∃ (x : α), IsTop x) ↔ ¬∀ (x : α), ¬IsTop x
⊢ cof α ≠ 1 ↔ NoTopOrder α

Tactic:
rw [← not_iff_not, not_not, noTopOrder_iff, cof_eq_one_iff]

Premises used: not_iff_not, Classical.not_not, Order.cof_eq_one_iff, noTopOrder_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
⊢ (∃ (x : α), IsTop x) ↔ ¬∀ (x : α), ¬IsTop x

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
h : NoTopOrder α
⊢ cof α ≠ 1

Tactic:
cof_ne_one_iff.2 h

Premises used: Iff.mpr, Order.cof_ne_one_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
rw : (cof α = 0 ∨ ∃ (x : α), IsTop x) ↔ ∃ (x : α), IsTop x
⊢ cof α ≤ 1 ↔ ∃ (x : α), IsTop x

Tactic:
rw [le_iff_lt_or_eq, Cardinal.lt_one_iff, cof_eq_one_iff]

Premises used: Order.cof_eq_one_iff, Cardinal.lt_one_iff, le_iff_lt_or_eq
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
⊢ (cof α = 0 ∨ ∃ (x : α), IsTop x) ↔ ∃ (x : α), IsTop x

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
rw : (∃ (x : α), IsTop x) ↔ ¬∀ (x : α), ¬IsTop x
⊢ 1 < cof α ↔ NoTopOrder α

Tactic:
rw [← not_iff_not, not_lt, noTopOrder_iff, cof_le_one_iff]

Premises used: not_iff_not, Order.cof_le_one_iff, not_lt, noTopOrder_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
⊢ (∃ (x : α), IsTop x) ↔ ¬∀ (x : α), ¬IsTop x

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
h : NoTopOrder α
⊢ 1 < cof α

Tactic:
one_lt_cof_iff.2 h

Premises used: Iff.mpr, Order.one_lt_cof_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
a : lift.{v, u} (cof α) ≤ lift.{u, v} (cof β)
a₁ : lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)
⊢ lift.{v, u} (cof α) = lift.{u, v} (cof β)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
a : ∀ (s : Set β), IsCofinal s → lift.{v, u} (cof α) ≤ lift.{u, v} #(↑s : Type v)
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} (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 : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
a : ∀ (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 : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
x : (↑s : Type v)
⊢ ∃ (y : α), (↑x : β) ≤ f y

Tactic:
simpa using hf' x

Premises used: Subtype.val
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
⊢ ∀ (x : (↑s : Type v)), ∃ (y : α), (↑x : β) ≤ f y

Tactic:
have H (x : s) : ∃ y : α, x ≤ f y := by simpa using hf' x
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
H : ∀ (x : (↑s : Type v)), ∃ (y : α), (↑x : β) ≤ f y
a :
  ∀ (g : (x : (↑s : Type v)) → α) (hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)),
    lift.{v, u} (cof α) ≤ lift.{u, v} #(↑s : Type v)
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #(↑s : Type v)

Tactic:
choose g hg using H
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #(↑s : Type v)

Tactic:
(lift_le.2 <| cof_le (s := range g) fun a ↦ ?_).trans mk_range_le_lift

Premises used: Iff.mpr, Order.cof_le, LE.le.trans, Cardinal.mk_range_le_lift, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
a : ∀ (a : α), ∃ y ∈ range g, a ≤ y
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #(↑s : Type v)

Tactic:
refine (lift_le.2 <| cof_le (s := range g) fun a ↦ ?_).trans mk_range_le_lift

Premises used: Iff.mpr, Order.cof_le, LE.le.trans, Cardinal.mk_range_le_lift, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
a : α
a₁ : ∀ (b : α) (hb : f a ≤ f b), ∃ y ∈ range g, a ≤ y
⊢ ∃ y ∈ range g, a ≤ y

Tactic:
obtain ⟨_, ⟨b, rfl⟩, hb⟩ := hf' (f a)

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
a b : α
hb : f a ≤ f b
a₁ : ∀ (c : β) (hc : c ∈ s) (hc' : f b ≤ c), ∃ y ∈ range g, a ≤ y
⊢ ∃ y ∈ range g, a ≤ y

Tactic:
obtain ⟨c, hc, hc'⟩ := hs (f b)
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
a b : α
hb : f a ≤ f b
c : β
hc : c ∈ s
hc' : f b ≤ c
⊢ ∃ y ∈ range g, a ≤ y

Tactic:
⟨_, Set.mem_range_self ⟨c, hc⟩, ?_⟩

Premises used: Set.mem_range_self, And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
a b : α
hb : f a ≤ f b
c : β
hc : c ∈ s
hc' : f b ≤ c
a₁ : a ≤ g (Subtype.mk (p := fun (x : β) ↦ x ∈ s) c hc)
⊢ ∃ y ∈ range g, a ≤ y

Tactic:
refine ⟨_, Set.mem_range_self ⟨c, hc⟩, ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
a b : α
hb : f a ≤ f b
c : β
hc : c ∈ s
hc' : f b ≤ c
a₁ : f a ≤ f (g (Subtype.mk (p := fun (x : β) ↦ x ∈ s) c hc))
⊢ a ≤ g (Subtype.mk (p := fun (x : β) ↦ x ∈ s) c hc)

Tactic:
rw [← hf.le_iff_le]

Premises used: StrictMono.le_iff_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
a b : α
hb : f a ≤ f b
c : β
hc : c ∈ s
hc' : f b ≤ c
⊢ f a ≤ f (g (Subtype.mk (p := fun (x : β) ↦ x ∈ s) c hc))

Tactic:
hb.trans (hc'.trans (hg ⟨c, hc⟩))

Premises used: Subtype.mk, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
a b : α
hb : f a ≤ f b
c : β
hc : c ∈ s
hc' : f b ≤ c
⊢ f a ≤ f (g (Subtype.mk (p := fun (x : β) ↦ x ∈ s) c hc))

Tactic:
exact hb.trans (hc'.trans (hg ⟨c, hc⟩))

Premises used: Subtype.mk, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set α
hs : IsCofinal s
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} #(↑s : Type u)

Tactic:
(lift_le.2 <| cof_le (hs.image hf.monotone hf')).trans mk_image_le_lift

Premises used: Iff.mpr, StrictMono.monotone, IsCofinal.image, 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 : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set α
hs : IsCofinal s
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} #(↑s : Type u)

Tactic:
exact (lift_le.2 <| cof_le (hs.image hf.monotone hf')).trans mk_image_le_lift

Premises used: Iff.mpr, StrictMono.monotone, IsCofinal.image, Order.cof_le, LE.le.trans, Cardinal.mk_image_le_lift, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α γ : Type u
inst : LinearOrder α
inst_1 : LinearOrder γ
f : α → γ
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ cof α = cof γ

Tactic:
simpa using lift_cof_congr_of_strictMono hf hf'

Premises used: Order.lift_cof_congr_of_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic
Goal:
α : Type u
inst : LinearOrder α
⊢ cof α < ℵ₀ ↔ cof α ≤ 1

Tactic:
⟨fun h ↦ ?_, (lt_of_le_of_lt · one_lt_aleph0)⟩

Premises used: lt_of_le_of_lt, Cardinal.one_lt_aleph0, Iff.intro