awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : ∀ (i : (↑(Iio ω) : Type (u_1 + 1))), preBeth (↑i : Ordinal.{u_1}) ≤ ℵ₀
⊢ preBeth ω ≤ ℵ₀

Tactic:
rw [preBeth_limit isSuccLimit_omega0.isSuccPrelimit, ciSup_le_iff' bddAbove_of_small]

Premises used: Ordinal.isSuccLimit_omega0, ciSup_le_iff', Cardinal.preBeth_limit, Order.IsSuccLimit.isSuccPrelimit, Cardinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : Ordinal.{u_1}
ha : a ∈ Iio ω
a₁ :
  ∀ (n : ℕ) (ha : (↑n : Ordinal.{u_1}) ∈ Iio ω),
    preBeth (↑(Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio ω) (↑n : Ordinal.{u_1}) ha) : Ordinal.{u_1}) ≤ ℵ₀
⊢ preBeth (↑(Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio ω) a ha) : Ordinal.{u_1}) ≤ ℵ₀

Tactic:
obtain ⟨n, rfl⟩ := lt_omega0.1 ha

Premises used: Iff.mp, Ordinal.lt_omega0, rfl
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
n : ℕ
ha : (↑n : Ordinal.{u_1}) ∈ Iio ω
a : (↑((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x)^[n] 0) : Cardinal.{u_1}) ≤ ℵ₀
⊢ preBeth (↑(Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio ω) (↑n : Ordinal.{u_1}) ha) : Ordinal.{u_1}) ≤ ℵ₀

Tactic:
rw [preBeth_nat]

Premises used: Cardinal.preBeth_nat
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
n : ℕ
ha : (↑n : Ordinal.{u_1}) ∈ Iio ω
⊢ (↑((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x)^[n] 0) : Cardinal.{u_1}) ≤ ℵ₀

Tactic:
natCast_le_aleph0

Premises used: Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
n : ℕ
ha : (↑n : Ordinal.{u_1}) ∈ Iio ω
⊢ (↑((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x)^[n] 0) : Cardinal.{u_1}) ≤ ℵ₀

Tactic:
exact natCast_le_aleph0

Premises used: Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ ℵ₀ ≤ preBeth ω

Tactic:
simpa using preAleph_le_preBeth ω

Premises used: Ordinal.omega0, Cardinal.preAleph_le_preBeth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ 0 < preBeth o ↔ 0 < o

Tactic:
simpa using preBeth_lt_preBeth (o₁ := 0)

Premises used: Cardinal.preBeth_lt_preBeth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ o.card ≤ preBeth o

Tactic:
o.card_le_preAleph.trans (preAleph_le_preBeth o)

Premises used: Ordinal.card_le_preAleph, Cardinal.preAleph_le_preBeth, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u_1}
⊢ c ≤ preBeth c.ord

Tactic:
simpa using c.ord.card_le_preBeth

Premises used: Ordinal.card_le_preBeth, Cardinal.ord
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ preBeth o = 0 ↔ o = 0

Tactic:
simpa using preBeth_inj (o₂ := 0)

Premises used: Cardinal.preBeth_inj
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ IsStrongPrelimit.{u_1} (preBeth o) ↔ IsSuccPrelimit o

Tactic:
⟨?_, fun ho x hx ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
refine_1 : IsStrongPrelimit.{u_1} (preBeth o) → IsSuccPrelimit o
refine_2 :
  ∀ (ho : IsSuccPrelimit o) (x : Cardinal.{u_1}) (hx : x < preBeth o), HPow.hPow (α := Cardinal.{u_1}) 2 x < preBeth o
⊢ IsStrongPrelimit.{u_1} (preBeth o) ↔ IsSuccPrelimit o

Tactic:
refine ⟨?_, fun ho x hx ↦ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
refine_1 : ¬IsSuccPrelimit o → ¬IsStrongPrelimit.{u_1} (preBeth o)
⊢ IsStrongPrelimit.{u_1} (preBeth o) → IsSuccPrelimit o

Tactic:
contrapose!
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
refine_1 :
  Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o →
    ∃ x < preBeth o, preBeth o ≤ HPow.hPow (α := Cardinal.{u_1}) 2 x
⊢ ¬IsSuccPrelimit o → ¬IsStrongPrelimit.{u_1} (preBeth o)

Tactic:
rw [not_isSuccPrelimit_iff_mem_range_succ, not_isStrongPrelimit_iff]

Premises used: Order.not_isSuccPrelimit_iff_mem_range_succ, Cardinal.not_isStrongPrelimit_iff
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : Ordinal.{u_1}
⊢ ∃ x < preBeth (succ a), preBeth (succ a) ≤ HPow.hPow (α := Cardinal.{u_1}) 2 x

Tactic:
⟨preBeth a, ?_, ?_⟩

Premises used: Cardinal.preBeth, And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : Ordinal.{u_1}
refine_1 : preBeth a < preBeth (succ a)
refine_1₁ : preBeth (succ a) ≤ HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth a)
⊢ ∃ x < preBeth (succ a), preBeth (succ a) ≤ HPow.hPow (α := Cardinal.{u_1}) 2 x

Tactic:
refine ⟨preBeth a, ?_, ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : Ordinal.{u_1}
refine_1 : a < succ a
refine_1₁ refine_1₂ : a ≤ a
⊢ preBeth a < preBeth (succ a)

Tactic:
rw [preBeth_lt_preBeth, lt_succ_iff]

Premises used: Cardinal.preBeth_lt_preBeth, Order.lt_succ_iff
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : Ordinal.{u_1}
⊢ preBeth (succ a) ≤ HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth a)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < preBeth o
⊢ x < ⨆ (a : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑a : Ordinal.{u_1})

Tactic:
rw [preBeth_limit ho] at hx

Premises used: Cardinal.preBeth_limit
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < ⨆ (a : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑a : Ordinal.{u_1})
refine_2 :
  ∀ (a : (↑(Iio o) : Type (u_1 + 1))) (ha : x < preBeth (↑a : Ordinal.{u_1})),
    HPow.hPow (α := Cardinal.{u_1}) 2 x < preBeth o
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 x < preBeth o

Tactic:
obtain ⟨a, ha⟩ := exists_lt_of_lt_ciSup' hx

Premises used: exists_lt_of_lt_ciSup'
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < ⨆ (a : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑a : Ordinal.{u_1})
a : (↑(Iio o) : Type (u_1 + 1))
ha : x < preBeth (↑a : Ordinal.{u_1})
refine_2 : HPow.hPow (α := Cardinal.{u_1}) 2 x ≤ preBeth ((↑a : Ordinal.{u_1}) + 1)
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 x < preBeth o

Tactic:
apply (preBeth_strictMono (ho.add_one_lt a.2)).trans_le'

Premises used: LT.lt.trans_le', Order.IsSuccPrelimit.add_one_lt, Cardinal.preBeth_strictMono, Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < ⨆ (a : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑a : Ordinal.{u_1})
a : (↑(Iio o) : Type (u_1 + 1))
ha : x < preBeth (↑a : Ordinal.{u_1})
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 x ≤ preBeth ((↑a : Ordinal.{u_1}) + 1)

Tactic:
simpa using power_le_power_left two_ne_zero ha.le

Premises used: LT.lt.le, two_ne_zero, Cardinal.power_le_power_left
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
rw : preBeth o ≠ 0 ∧ IsStrongPrelimit.{u_1} (preBeth o) ↔ IsSuccLimit o
rw₁ : preBeth o ≠ 0 ∧ IsStrongPrelimit.{u_1} (preBeth o) ↔ o ≠ 0 ∧ IsSuccPrelimit o
rw₂ : o ≠ 0 ∧ IsStrongPrelimit.{u_1} (preBeth o) ↔ o ≠ 0 ∧ IsSuccPrelimit o
rw₃ rw₄ : o ≠ 0 ∧ IsSuccPrelimit o ↔ o ≠ 0 ∧ IsSuccPrelimit o
⊢ IsStrongLimit.{u_1} (preBeth o) ↔ IsSuccLimit o

Tactic:
rw [isStrongLimit_iff, isSuccLimit_iff, preBeth_eq_zero.ne, isStrongPrelimit_preBeth]

Premises used: Cardinal.preBeth_eq_zero, Cardinal.isStrongPrelimit_preBeth, Ordinal.isSuccLimit_iff, Iff.ne, Cardinal.isStrongLimit_iff
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
h : ¬IsMax o
IH : lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)
⊢ lift.{v, u_1} (preBeth (succ o)) = preBeth (Ordinal.lift.{v, u_1} (succ o))

Tactic:
simp [IH]
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
isSuccPrelimit :
  Eq (α := Cardinal.{max u_1 v}) (⨆ (i : (↑(Iio o) : Type (u_1 + 1))), lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
    (⨆ (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))), preBeth (↑a : Ordinal.{max u_1 v}))
⊢ lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)

Tactic:
rw [preBeth_limit ho, preBeth_limit (isSuccPrelimit_lift.2 ho), lift_iSup bddAbove_of_small]

Premises used: Iff.mpr, Cardinal.lift_iSup, Ordinal.isSuccPrelimit_lift, Cardinal.preBeth_limit, Cardinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
isSuccPrelimit :
  Eq (α := Set Cardinal.{max u_1 v})
    (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
    (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
⊢ Eq (α := Cardinal.{max u_1 v}) (⨆ (i : (↑(Iio o) : Type (u_1 + 1))), lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
    (⨆ (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))), preBeth (↑a : Ordinal.{max u_1 v}))

Tactic:
apply congrArg sSup

Premises used: congrArg, SupSet.sSup
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
isSuccPrelimit :
  ∀ (x : Cardinal.{max u_1 v}),
    Membership.mem (γ := Set Cardinal.{max u_1 v})
        (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1}))) x ↔
      Membership.mem (γ := Set Cardinal.{max u_1 v})
        (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦
          preBeth (↑a : Ordinal.{max u_1 v}))
        x
⊢ Eq (α := Set Cardinal.{max u_1 v})
    (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
    (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))

Tactic:
ext x
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
x : Cardinal.{max u_1 v}
isSuccPrelimit :
  Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1}))) x →
    Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      x
isSuccPrelimit₁ :
  Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      x →
    Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1}))) x
⊢ Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1}))) x ↔
    Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      x

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi : i ∈ Iio o
⊢ Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
    ((fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) i hi))

Tactic:
⟨⟨i.lift, ?_⟩, (IH _ hi).symm⟩

Premises used: Set.Mem, setOf, Ordinal.lift, Subtype.mk, Exists.intro, Set.range, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi : i ∈ Iio o
isSuccPrelimit : Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)
⊢ Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
    ((fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) i hi))

Tactic:
refine ⟨⟨i.lift, ?_⟩, (IH _ hi).symm⟩
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi : i ∈ Iio o
⊢ Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{max u_1 v}
hi : i ∈ Iio (Ordinal.lift.{v, u_1} o)
isSuccPrelimit :
  ∀ (i : Ordinal.{u_1}) (hi : Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)),
    Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
      ((fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
        (Subtype.mk (p := fun (x : Ordinal.{max u_1 v}) ↦ x ∈ Iio (Ordinal.lift.{v, u_1} o)) (Ordinal.lift.{v, u_1} i)
          hi))
⊢ Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
    ((fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      (Subtype.mk (p := fun (x : Ordinal.{max u_1 v}) ↦ x ∈ Iio (Ordinal.lift.{v, u_1} o)) i hi))

Tactic:
obtain ⟨i, rfl⟩ := Ordinal.mem_range_lift_of_le hi.le

Premises used: Ordinal.mem_range_lift_of_le, LT.lt.le, rfl
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi : Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)
⊢ i < o

Tactic:
rw [mem_Iio, Ordinal.lift_lt] at hi

Premises used: Set.mem_Iio, Ordinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi_1 : Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)
hi : i < o
⊢ Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
    ((fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      (Subtype.mk (p := fun (x : Ordinal.{max u_1 v}) ↦ x ∈ Iio (Ordinal.lift.{v, u_1} o)) (Ordinal.lift.{v, u_1} i)
        hi_1))

Tactic:
⟨⟨i, hi⟩, IH _ hi⟩

Premises used: Set.Mem, setOf, Subtype.mk, Exists.intro, Set.range
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi_1 : Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)
hi : i < o
⊢ Membership.mem (γ := Set Cardinal.{max u_1 v})
    (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
    ((fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      (Subtype.mk (p := fun (x : Ordinal.{max u_1 v}) ↦ x ∈ Iio (Ordinal.lift.{v, u_1} o)) (Ordinal.lift.{v, u_1} i)
        hi_1))

Tactic:
exact ⟨⟨i, hi⟩, IH _ hi⟩
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
succ :
  ∀ (o : Ordinal.{u_1}),
    ¬IsMax o →
      ∀ (IH : lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)),
        lift.{v, u_1} (preBeth (Order.succ o)) = preBeth (Ordinal.lift.{v, u_1} (Order.succ o))
isSuccPrelimit :
  ∀ (o : Ordinal.{u_1}) (ho : IsSuccPrelimit o)
    (IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)),
    lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)
⊢ lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)

Tactic:
induction o using SuccOrder.prelimitRecOn with
  | succ o _ IH => simp [IH]
  | isSuccPrelimit o ho IH =>
    rw [preBeth_limit ho, preBeth_limit (isSuccPrelimit_lift.2 ho), lift_iSup bddAbove_of_small]
    apply congrArg sSup
    ext x
    constructor <;> rintro ⟨⟨i, hi⟩, rfl⟩
    · refine ⟨⟨i.lift, ?_⟩, (IH _ hi).symm⟩
      simpa
    · obtain ⟨i, rfl⟩ := Ordinal.mem_range_lift_of_le hi.le
      rw [mem_Iio, Ordinal.lift_lt] at hi
      exact ⟨⟨i, hi⟩, IH _ hi⟩

Premises used: Set.mem_Iio, Ordinal.lift_lt, Order.succ, congrArg, Cardinal.lift_iSup, Cardinal.bddAbove_of_small, SupSet.sSup, rfl
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ ℶ_ o = preBeth (ω + o)

Tactic:
rfl

Premises used: Cardinal.beth, rfl
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ preBeth o ≤ ℶ_ o

Tactic:
preBeth_le_preBeth.2 le_add_self

Premises used: Iff.mpr, Cardinal.preBeth_le_preBeth, Cardinal.beth, le_add_self
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
x x_1 : Ordinal.{u_1}
h : x < x_1
⊢ ω + x < ω + x_1

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ Monotone ℶ_

Tactic:
beth_strictMono.monotone

Premises used: StrictMono.monotone, Cardinal.beth_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ ℶ_ o₁ < ℶ_ o₂ ↔ o₁ < o₂

Tactic:
beth_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Cardinal.beth_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ ℶ_ o₁ ≤ ℶ_ o₂ ↔ o₁ ≤ o₂

Tactic:
beth_strictMono.le_iff_le

Premises used: Cardinal.beth_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ ℶ_ 0 = ℵ₀

Tactic:
simp [beth]

Premises used: Cardinal.beth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ ℶ_ (o + 1) = HPow.hPow (α := Cardinal.{u_1}) 2 (ℶ_ o)

Tactic:
simp [beth, ← add_assoc]

Premises used: add_assoc, Cardinal.beth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ ℶ_ (succ o) = HPow.hPow (α := Cardinal.{u_1}) 2 (ℶ_ o)

Tactic:
beth_add_one o

Premises used: Order.succ, Cardinal.beth_add_one
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ IsNormal ℶ_

Tactic:
isNormal_preBeth.comp (isNormal_add_right _)

Premises used: Order.IsNormal.comp, Ordinal.isNormal_add_right, WellFounded.fixF, Cardinal.isNormal_preBeth, Cardinal.beth, WellFounded.fix
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ ℶ_ o = ⨆ (a : (↑(Iio o) : Type (u_1 + 1))), ℶ_ (↑a : Ordinal.{u_1})

Tactic:
isNormal_beth.apply_of_isSuccLimit ho

Premises used: Order.IsNormal.apply_of_isSuccLimit, Cardinal.isNormal_beth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ≤ ℶ_ o

Tactic:
preAleph_le_preBeth _

Premises used: Cardinal.preAleph_le_preBeth, Cardinal.beth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ ℶ_ o

Tactic:
(aleph0_le_aleph o).trans <| aleph_le_beth o

Premises used: Cardinal.aleph_le_beth, Cardinal.aleph0_le_aleph, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ 0 < ℶ_ o

Tactic:
aleph0_pos.trans_le <| aleph0_le_beth o

Premises used: Cardinal.aleph0_le_beth, LT.lt.trans_le, Cardinal.aleph0_pos
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ ℶ_ o ≠ 0

Tactic:
(beth_pos o).ne'

Premises used: Cardinal.beth_pos, LT.lt.ne'
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ o.card ≤ ℶ_ o

Tactic:
o.card_le_aleph.trans (aleph_le_beth o)

Premises used: Cardinal.aleph_le_beth, Ordinal.card_le_aleph, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u_1}
⊢ c ≤ ℶ_ c.ord

Tactic:
simpa using c.ord.card_le_beth

Premises used: Cardinal.ord, Ordinal.card_le_beth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
rw : IsStrongLimit.{u_1} (preBeth (ω + o)) ↔ IsSuccPrelimit o
rw₁ : IsSuccLimit (ω + o) ↔ IsSuccPrelimit o
rw₂ rw₃ : IsSuccPrelimit o ↔ IsSuccPrelimit o
⊢ IsStrongLimit.{u_1} (ℶ_ o) ↔ IsSuccPrelimit o

Tactic:
rw [beth_eq_preBeth, isStrongLimit_preBeth, isSuccLimit_add_iff_of_isSuccLimit isSuccLimit_omega0]

Premises used: Cardinal.isStrongLimit_preBeth, Ordinal.isSuccLimit_omega0, Ordinal.isSuccLimit_add_iff_of_isSuccLimit, Cardinal.beth_eq_preBeth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
rw : lift.{v, u_1} (preBeth (ω + o)) = ℶ_ (Ordinal.lift.{v, u_1} o)
rw₁ : lift.{v, u_1} (preBeth (ω + o)) = preBeth (ω + Ordinal.lift.{v, u_1} o)
rw₂ : preBeth (Ordinal.lift.{v, u_1} (ω + o)) = preBeth (ω + Ordinal.lift.{v, u_1} o)
rw₃ : preBeth (Ordinal.lift.{v, u_1} ω + Ordinal.lift.{v, u_1} o) = preBeth (ω + Ordinal.lift.{v, u_1} o)
rw₄ rw₅ : preBeth (ω + Ordinal.lift.{v, u_1} o) = preBeth (ω + Ordinal.lift.{v, u_1} o)
⊢ lift.{v, u_1} (ℶ_ o) = ℶ_ (Ordinal.lift.{v, u_1} o)

Tactic:
rw [beth_eq_preBeth, beth_eq_preBeth, lift_preBeth, Ordinal.lift_add, lift_omega0]

Premises used: Cardinal.lift_preBeth, Ordinal.lift_add, Cardinal.beth_eq_preBeth, Ordinal.lift_omega0
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1}) ≤ o
rw : ω < HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1})
⊢ preBeth o = ℶ_ o

Tactic:
rw [beth, add_of_omega0_opow_le _ ho]

Premises used: Ordinal.add_of_omega0_opow_le, Cardinal.beth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
⊢ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1 ≤ lift.{v, u} c ↔ (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ c

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
⊢ lift.{v, u} c ≤ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1 ↔ c ≤ (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1

Tactic:
simpa using lift_le (b := ℵ₁)

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
⊢ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1 < lift.{v, u} c ↔ (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 < c

Tactic:
simpa using lift_lt (a := ℵ₁)

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
⊢ lift.{v, u} c < (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1 ↔ c < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
⊢ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1 = lift.{v, u} c ↔ (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 = c

Tactic:
simpa using lift_inj (a := ℵ₁)

Premises used: Cardinal.lift_inj
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
⊢ lift.{v, u} c = (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) 1 ↔ c = (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1

Tactic:
simp [eqComm]

Premises used: eqComm
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
⊢ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) (↑n : Ordinal.{max u v}) ≤ lift.{v, u} c ↔
    (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) (↑n : Ordinal.{u}) ≤ c

Tactic:
simpa using lift_le (a := ℵ_ n)

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c ≤ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) (↑n : Ordinal.{max u v}) ↔
    c ≤ (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) (↑n : Ordinal.{u})

Tactic:
simpa using lift_le (b := ℵ_ n)

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
⊢ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) (↑n : Ordinal.{max u v}) < lift.{v, u} c ↔
    (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) (↑n : Ordinal.{u}) < c

Tactic:
simpa using lift_lt (a := ℵ_ n)

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c < (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) (↑n : Ordinal.{max u v}) ↔
    c < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) (↑n : Ordinal.{u})

Tactic:
simpa using lift_lt (b := ℵ_ n)

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u}
n : ℕ
⊢ (ℵ_ : (a : Ordinal.{max u v}) → Cardinal.{max u v}) (↑n : Ordinal.{max u v}) = lift.{v, u} c ↔
    (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) (↑n : Ordinal.{u}) = c

Tactic:
simpa using lift_inj (a := ℵ_ n)

Premises used: Cardinal.lift_inj