awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
a b : α
hab :
  Eq.{u_1 + 1} (α := { s : Set α // #(↑s : Type u_1) < (#α).ord.cof })
    ((fun (x : α) ↦
        (Subtype.mk (p := fun (s : Set α) ↦ #(↑s : Type u_1) < (#α).ord.cof) {x} ⋯ :
          { s : Set α // #(↑s : Type u_1) < (#α).ord.cof }))
      a)
    ((fun (x : α) ↦
        (Subtype.mk (p := fun (s : Set α) ↦ #(↑s : Type u_1) < (#α).ord.cof) {x} ⋯ :
          { s : Set α // #(↑s : Type u_1) < (#α).ord.cof }))
      b)
⊢ a = b

Tactic:
simpa [singleton_eq_singleton_iff] using hab

Premises used: Set.singleton_eq_singleton_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
inr inr₁ inr₂ : #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
inr₃ : #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } ≤ #α
inr₄ inr₅ : #α ≤ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof }
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α

Tactic:
classical
  letI := linearOrderOfSTO r
  apply le_antisymm
  · conv_rhs => rw [← mk_bounded_subset h hr]
    apply mk_subtype_le_of_subset
    intro s hs
    rw [hr] at hs
    contrapose! hs
    rw [not_bounded_iff] at hs
    apply cof_le
    simp_rw [IsCofinal, ← not_lt]
    exact hs
  · refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
    · rw [mk_singleton, one_lt_cof_iff]
      exact isSuccLimit_ord h'.aleph0_le
    · intro a b hab
      simpa [singleton_eq_singleton_iff] using hab

Premises used: Cardinal.isSuccLimit_ord, Cardinal.mk_subtype_le_of_subset, Cardinal.IsStrongLimit.aleph0_le, Cardinal.mk_bounded_subset, Set.not_bounded_iff, Set.singleton_eq_singleton_iff, le_antisymm, not_lt, Order.cof_le, Cardinal.mk_le_of_injective, Cardinal.mk_singleton, IsCofinal
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
mk : ∀ (α : Type u_1) (hc : ℵ₀ ≤ #α), #α < #α ^ (#α).ord.cof
⊢ c < c ^ c.ord.cof

Tactic:
induction c using Cardinal.inductionOn with | mk α

Premises used: Cardinal.mk
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
mk :
  ∀ (w : LinearOrder α) (w_1 : WellFoundedLT α) (hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2), #α < #α ^ (#α).ord.cof
⊢ #α < #α ^ (#α).ord.cof

Tactic:
obtain ⟨_, _, hα⟩ := exists_ord_eq_type_lt α

Premises used: Cardinal.exists_ord_eq_type_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
rw : IsSuccPrelimit (#α).ord
⊢ NoMaxOrder α

Tactic:
rw [← isSuccPrelimit_type_lt_iff, ← hα]

Premises used: Ordinal.isSuccPrelimit_type_lt_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
⊢ IsSuccPrelimit (#α).ord

Tactic:
(isSuccLimit_ord hc).isSuccPrelimit

Premises used: Cardinal.isSuccLimit_ord, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
⊢ IsSuccPrelimit (#α).ord

Tactic:
exact (isSuccLimit_ord hc).isSuccPrelimit

Premises used: Cardinal.isSuccLimit_ord, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
⊢ NoMaxOrder α

Tactic:
have : NoMaxOrder α := by
    rw [← isSuccPrelimit_type_lt_iff, ← hα]
    exact (isSuccLimit_ord hc).isSuccPrelimit
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this : NoMaxOrder α
mk :
  ∀ (s : Set α) (hs : IsCofinal s) (hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord),
    #α < #α ^ (#α).ord.cof
⊢ #α < #α ^ (#α).ord.cof

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

Premises used: Ordinal.exists_ord_cof_eq
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
mk : #α < prod fun (x : (↑s : Type u_1)) ↦ #α
⊢ #α < #α ^ (#α).ord.cof

Tactic:
rw [hα, cof_type, ← card_ord (Order.cof _), ← hs', card_type, ← prod_const']

Premises used: Ordinal.cof_type, Cardinal.prod_const', Ordinal.card_type, Cardinal.card_ord, Order.cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
⊢ #α < prod fun (x : (↑s : Type u_1)) ↦ #α

Tactic:
(mk_iUnion_le_sum_mk.trans' ?_).trans_lt (sum_lt_prod _ _ fun i ↦ mk_Iio_lt i.1 hα)

Premises used: Cardinal.mk_iUnion_le_sum_mk, Cardinal.mk_Iio_lt, Cardinal.sum_lt_prod, Subtype.val, LE.le.trans_lt, LE.le.trans'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
mk : #α ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)
⊢ #α < prod fun (x : (↑s : Type u_1)) ↦ #α

Tactic:
refine (mk_iUnion_le_sum_mk.trans' ?_).trans_lt (sum_lt_prod _ _ fun i ↦ mk_Iio_lt i.1 hα)

Premises used: Cardinal.mk_iUnion_le_sum_mk, Cardinal.sum_lt_prod, LE.le.trans_lt, LE.le.trans'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
hc : ℵ₀ ≤ #α
w : LinearOrder α
w_1 : WellFoundedLT α
hα : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof α).ord
mk : #(↑Set.univ : Type u_1) ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)
mk₁ : #(↑(⋃ i ∈ s, Iio i) : Type u_1) ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)
mk₂ mk₃ : #(↑(⋃ i ∈ s, Iio i) : Type u_1) ≤ #(↑(⋃ i ∈ s, Iio i) : Type u_1)
⊢ #α ≤ #(↑(⋃ (i : (↑s : Type u_1)), Iio (↑i : α)) : Type u_1)

Tactic:
rw [← mk_univ, ← isCofinal_iff_iUnion_Iio_eq_univ.1 hs, iUnion_coe_set]

Premises used: Cardinal.mk_univ, Set.iUnion_coe_set, Iff.mp, isCofinal_iff_iUnion_Iio_eq_univ
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
apply : (b ^ a) ^ a < (b ^ a) ^ (b ^ a).ord.cof
⊢ a < (b ^ a).ord.cof

Tactic:
apply lt_imp_lt_of_le_imp_le (power_le_power_left <| power_ne_zero a hb.ne_bot)

Premises used: Cardinal.power_ne_zero, lt_imp_lt_of_le_imp_le, Cardinal.power_le_power_left, LT.lt.ne_bot
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
rw : b ^ a < (b ^ a) ^ (b ^ a).ord.cof
⊢ (b ^ a) ^ a < (b ^ a) ^ (b ^ a).ord.cof

Tactic:
rw [← power_mul, mul_eq_self ha]

Premises used: Cardinal.power_mul, Cardinal.mul_eq_self
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
⊢ b ^ a < (b ^ a) ^ (b ^ a).ord.cof

Tactic:
lt_power_cof_ord (ha.trans <| (cantor' _ hb).le)

Premises used: LT.lt.le, LE.le.trans, Cardinal.cantor', Cardinal.lt_power_cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
⊢ b ^ a < (b ^ a) ^ (b ^ a).ord.cof

Tactic:
exact lt_power_cof_ord (ha.trans <| (cantor' _ hb).le)

Premises used: LT.lt.le, LE.le.trans, Cardinal.cantor', Cardinal.lt_power_cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀ = 𝔠

Tactic:
rfl

Premises used: Cardinal.continuum, rfl
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
rw : lift.{v, u_1} (HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀) = 𝔠
rw₁ : HPow.hPow (α := Cardinal.{max u_1 v}) 2 (lift.{v, u_1} ℵ₀) = 𝔠
rw₂ : HPow.hPow (α := Cardinal.{max u_1 v}) 2 ℵ₀ = 𝔠
rw₃ rw₄ : 𝔠 = 𝔠
⊢ lift.{v, u_1} 𝔠 = 𝔠

Tactic:
rw [← two_power_aleph0, lift_two_power, lift_aleph0, two_power_aleph0]

Premises used: Cardinal.lift_two_power, Cardinal.lift_aleph0, Cardinal.two_power_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
c : Cardinal.{u}
rw : lift.{v, u} 𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c
rw₁ rw₂ : 𝔠 ≤ c ↔ 𝔠 ≤ c
⊢ 𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c

Tactic:
rw [← lift_continuum.{v, u}, lift_le]

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
c : Cardinal.{u}
rw : lift.{v, u} c ≤ lift.{v, u} 𝔠 ↔ c ≤ 𝔠
rw₁ rw₂ : c ≤ 𝔠 ↔ c ≤ 𝔠
⊢ lift.{v, u} c ≤ 𝔠 ↔ c ≤ 𝔠

Tactic:
rw [← lift_continuum.{v, u}, lift_le]

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
c : Cardinal.{u}
rw : lift.{v, u} 𝔠 < lift.{v, u} c ↔ 𝔠 < c
rw₁ rw₂ : 𝔠 < c ↔ 𝔠 < c
⊢ 𝔠 < lift.{v, u} c ↔ 𝔠 < c

Tactic:
rw [← lift_continuum.{v, u}, lift_lt]

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
c : Cardinal.{u}
rw : lift.{v, u} c < lift.{v, u} 𝔠 ↔ c < 𝔠
rw₁ rw₂ : c < 𝔠 ↔ c < 𝔠
⊢ lift.{v, u} c < 𝔠 ↔ c < 𝔠

Tactic:
rw [← lift_continuum.{v, u}, lift_lt]

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ ℵ₀ < 𝔠

Tactic:
cantor ℵ₀

Premises used: Cardinal.aleph0, Cardinal.cantor
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ ℵ₀ ≤ 𝔠

Tactic:
aleph0_lt_continuum.le

Premises used: LT.lt.le, Cardinal.aleph0_lt_continuum
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ ℶ_ 1 = 𝔠

Tactic:
simpa using beth_succ 0

Premises used: Cardinal.beth_succ, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
n : ℕ
⊢ (↑n : Cardinal.{u_1}) < 𝔠

Tactic:
natCast_lt_aleph0.trans aleph0_lt_continuum

Premises used: Cardinal.natCast_lt_aleph0, LT.lt.trans, Cardinal.aleph0_lt_continuum
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ #(Set ℕ) = 𝔠

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ 0 < 𝔠

Tactic:
nat_lt_continuum 0

Premises used: Cardinal.nat_lt_continuum, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ 𝔠 ≠ 0

Tactic:
continuum_pos.ne'

Premises used: Cardinal.continuum_pos, LT.lt.ne'
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
rw : Order.succ ℵ₀ ≤ 𝔠
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ≤ 𝔠

Tactic:
rw [← succ_aleph0]

Premises used: Cardinal.succ_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ Order.succ ℵ₀ ≤ 𝔠

Tactic:
Order.succ_le_of_lt aleph0_lt_continuum

Premises used: Order.succ_le_of_lt, Cardinal.aleph0_lt_continuum
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ Order.succ ℵ₀ ≤ 𝔠

Tactic:
exact Order.succ_le_of_lt aleph0_lt_continuum

Premises used: Order.succ_le_of_lt, Cardinal.aleph0_lt_continuum
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u_1}) → ℕ) 𝔠 : ℕ) (0 : ℕ)

Tactic:
toNat_apply_of_aleph0_le aleph0_le_continuum

Premises used: Cardinal.aleph0_le_continuum, Cardinal.toNat_apply_of_aleph0_le
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u_1}) → ℕ∞) 𝔠 : ℕ∞) (⊤ : ℕ∞)

Tactic:
(toENat_eq_top.2 aleph0_le_continuum)

Premises used: Iff.mpr, Cardinal.aleph0_le_continuum, Cardinal.toENat_eq_top
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ ℵ₀ + 𝔠 = 𝔠

Tactic:
add_eq_right aleph0_le_continuum aleph0_le_continuum

Premises used: Cardinal.aleph0_le_continuum, Cardinal.add_eq_right
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ 𝔠 + ℵ₀ = 𝔠

Tactic:
(add_comm _ _).trans aleph0_add_continuum

Premises used: Cardinal.aleph0_add_continuum, add_comm, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ 𝔠 + 𝔠 = 𝔠

Tactic:
add_eq_self aleph0_le_continuum

Premises used: Cardinal.aleph0_le_continuum, Cardinal.add_eq_self
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
n : ℕ
⊢ (↑n : Cardinal.{u_1}) + 𝔠 = 𝔠

Tactic:
nat_add_eq n aleph0_le_continuum

Premises used: Cardinal.aleph0_le_continuum, Cardinal.nat_add_eq
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
n : ℕ
⊢ 𝔠 + (↑n : Cardinal.{u_1}) = 𝔠

Tactic:
(add_comm _ _).trans (nat_add_continuum n)

Premises used: Cardinal.nat_add_continuum, add_comm, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n + 𝔠 = 𝔠

Tactic:
nat_add_continuum n

Premises used: Cardinal.nat_add_continuum
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ 𝔠 + OfNat.ofNat n = 𝔠

Tactic:
continuum_add_nat n

Premises used: Cardinal.continuum_add_nat
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ 𝔠 * 𝔠 = 𝔠

Tactic:
mul_eq_left aleph0_le_continuum le_rfl continuum_ne_zero

Premises used: Cardinal.aleph0_le_continuum, le_rfl, Cardinal.mul_eq_left, Cardinal.continuum_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ 𝔠 * ℵ₀ = 𝔠

Tactic:
mul_eq_left aleph0_le_continuum aleph0_le_continuum aleph0_ne_zero

Premises used: Cardinal.aleph0_le_continuum, Cardinal.mul_eq_left, Cardinal.aleph0_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ ℵ₀ * 𝔠 = 𝔠

Tactic:
(mul_comm _ _).trans continuum_mul_aleph0

Premises used: Cardinal.continuum_mul_aleph0, mul_comm, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
n : ℕ
hn : n ≠ 0
⊢ (↑n : Cardinal.{u_1}) * 𝔠 = 𝔠

Tactic:
mul_eq_right aleph0_le_continuum (nat_lt_continuum n).le (Nat.cast_ne_zero.2 hn)

Premises used: Iff.mpr, Cardinal.aleph0_le_continuum, Cardinal.nat_lt_continuum, LT.lt.le, Cardinal.mul_eq_right, Nat.cast_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
n : ℕ
hn : n ≠ 0
⊢ 𝔠 * (↑n : Cardinal.{u_1}) = 𝔠

Tactic:
(mul_comm _ _).trans (nat_mul_continuum hn)

Premises used: Cardinal.nat_mul_continuum, mul_comm, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n * 𝔠 = 𝔠

Tactic:
nat_mul_continuum (OfNat.ofNat_ne_zero n)

Premises used: OfNat.ofNat_ne_zero, Cardinal.nat_mul_continuum
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ 𝔠 * OfNat.ofNat n = 𝔠

Tactic:
continuum_mul_nat (OfNat.ofNat_ne_zero n)

Premises used: OfNat.ofNat_ne_zero, Cardinal.continuum_mul_nat
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
⊢ ℵ₀ ^ ℵ₀ = 𝔠

Tactic:
power_self_eq le_rfl

Premises used: le_rfl, Cardinal.power_self_eq, Cardinal.continuum
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
n : ℕ
hn : 2 ≤ n
⊢ HPow.hPow (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ℵ₀ = 𝔠

Tactic:
nat_power_eq le_rfl hn

Premises used: le_rfl, Cardinal.nat_power_eq, Cardinal.continuum
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
rw : HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀ ^ ℵ₀ = HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀
rw₁ : HPow.hPow (α := Cardinal.{u_1}) 2 (ℵ₀ * ℵ₀) = HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀
rw₂ rw₃ : HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀ = HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀
⊢ 𝔠 ^ ℵ₀ = 𝔠

Tactic:
rw [← two_power_aleph0, ← power_mul, mul_eq_left le_rfl le_rfl aleph0_ne_zero]

Premises used: Cardinal.power_mul, le_rfl, Cardinal.mul_eq_left, Cardinal.two_power_aleph0, Cardinal.aleph0_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
a : x ^ ℵ₀ ≤ 𝔠
a₁ : 𝔠 ≤ x ^ ℵ₀
⊢ x ^ ℵ₀ = 𝔠

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
a : x ^ ℵ₀ ≤ 𝔠 ^ ℵ₀
⊢ x ^ ℵ₀ ≤ 𝔠

Tactic:
rw [← continuum_power_aleph0]

Premises used: Cardinal.continuum_power_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ ≤ 𝔠 ^ ℵ₀

Tactic:
power_le_power_right h₂

Premises used: Cardinal.power_le_power_right
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ ≤ 𝔠 ^ ℵ₀

Tactic:
exact power_le_power_right h₂

Premises used: Cardinal.power_le_power_right
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀ ≤ x ^ ℵ₀

Tactic:
power_le_power_right h₁

Premises used: Cardinal.power_le_power_right
-- Module: Mathlib.SetTheory.Cardinal.Continuum
Goal:
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 ℵ₀ ≤ x ^ ℵ₀

Tactic:
exact power_le_power_right h₁

Premises used: Cardinal.power_le_power_right
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
inl : ∀ (ha : a < ℵ₀), #(↑t : Type u) ≤ a
inr : ∀ (ha : ℵ₀ ≤ a), #(↑t : Type u) ≤ a
⊢ #(↑t : Type u) ≤ a

Tactic:
rcases lt_or_ge a ℵ₀ with ha | ha

Premises used: Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : a < ℵ₀
⊢ ∃ (n : ℕ), a = (↑n : Cardinal.{u})

Tactic:
lt_aleph0.1 ha

Premises used: Iff.mp, Cardinal.lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
a : Cardinal.{u}
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ a
ha : a < ℵ₀
inl :
  ∀ (n : ℕ) (h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})) (ha : (↑n : Cardinal.{u}) < ℵ₀),
    #(↑t : Type u) ≤ (↑n : Cardinal.{u})
⊢ #(↑t : Type u) ≤ a

Tactic:
obtain ⟨n, rfl⟩ : ∃ (n : ℕ), a = n := lt_aleph0.1 ha

Premises used: Iff.mp, Cardinal.lt_aleph0, rfl
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
apply : ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ t), s.card ≤ n
⊢ #(↑t : Type u) ≤ (↑n : Cardinal.{u})

Tactic:
apply mk_le_iff_forall_finset_subset_card_le.2 (fun s hs ↦ ?_)

Premises used: Iff.mpr, Cardinal.mk_le_iff_forall_finset_subset_card_le
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
⊢ ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i

Tactic:
have A : ∀ x ∈ s, ∀ᶠ i in l, x ∈ f i := fun x hx ↦ ht x (hs hx)
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
⊢ ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i

Tactic:
have B : ∀ᶠ i in l, ∀ x ∈ s, x ∈ f i := (s.eventually_all).2 A
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
rcases : ∀ (i : ι) (hi : ∀ x ∈ s, x ∈ f i), s.card ≤ n
⊢ s.card ≤ n

Tactic:
rcases B.exists with ⟨i, hi⟩

Premises used: Filter.Eventually.exists
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
have : ∀ (this : (i : ι) → Fintype (↑(f i) : Type u)), s.card ≤ n
⊢ s.card ≤ n

Tactic:
have : ∀ i, Fintype (f i) := fun i ↦ (lt_aleph0_iff_fintype.1 ((h'f i).trans_lt ha)).some
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
x : α
hx : x ∈ s
⊢ x ∈ u

Tactic:
simpa only [u, Set.mem_toFinset] using hi x hx

Premises used: Set.mem_toFinset
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
⊢ s ⊆ u

Tactic:
have : s ⊆ u := fun x hx ↦ by simpa only [u, Set.mem_toFinset] using hi x hx
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this_1 : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
this : s ⊆ u
⊢ s.card ≤ u.card

Tactic:
Finset.card_le_card this

Premises used: Finset.card_le_card
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this_1 : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
this : s ⊆ u
⊢ s.card ≤ u.card

Tactic:
exact Finset.card_le_card this

Premises used: Finset.card_le_card
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
⊢ s.card ≤ u.card

Tactic:
have I1 : s.card ≤ u.card := by
      have : s ⊆ u := fun x hx ↦ by simpa only [u, Set.mem_toFinset] using hi x hx
      exact Finset.card_le_card this
-- Module: Mathlib.SetTheory.Cardinal.CountableCover
Goal:
α ι : Type u
inst : Countable ι
f : ι → Set α
l : Filter ι
inst_1 : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})
ha : (↑n : Cardinal.{u}) < ℵ₀
s : Finset α
hs : (↑s : Set α) ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype (↑(f i) : Type u)
u : Finset α := (f i).toFinset
I1 : s.card ≤ u.card
⊢ #(↑(f i) : Type u) ≤ (↑n : Cardinal.{u})

Tactic:
h'f i