awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
⊢ (a ^ b).card ≤ max a.card b.card
have zero : (HPow.hPow (β := Ordinal.{u_1}) a 0).card ≤ max a.card (card 0)
Tactic: induction b using limitRecOn with
  | zero => simpa using one_lt_omega0.le.trans ha
  | add_one b IH =>
    rw [opow_add_one, card_mul, card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]
    · grw [IH]
      rw [← max_assoc, max_self]
      grw [← le_self_add]
    · rw [ne_eq, card_eq_zero, opow_eq_zero]
      rintro ⟨rfl, -⟩
      cases omega0_pos.not_ge ha
    · rwa [aleph0_le_card]
  | limit b hb IH =>
    rw [(isNormal_opow (one_lt_omega0.trans_le ha)).apply_of_isSuccLimit hb]
    exact card_iSup_Iio_le (le_max_right ..) fun i ↦
      (IH i i.2).trans (max_le_max_left _ (card_le_card i.2.le))
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
zero : (HPow.hPow (β := Ordinal.{u_1}) a 0).card ≤ max a.card (card 0)
⊢ (a ^ b).card ≤ max a.card b.card
have add_one : ∀ (b : Ordinal.{u_1}) (IH : (a ^ b).card ≤ max a.card b.card), (a ^ (b + 1)).card ≤ max a.card (b + 1).card
Tactic: induction b using limitRecOn with
  | zero => simpa using one_lt_omega0.le.trans ha
  | add_one b IH =>
    rw [opow_add_one, card_mul, card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]
    · grw [IH]
      rw [← max_assoc, max_self]
      grw [← le_self_add]
    · rw [ne_eq, card_eq_zero, opow_eq_zero]
      rintro ⟨rfl, -⟩
      cases omega0_pos.not_ge ha
    · rwa [aleph0_le_card]
  | limit b hb IH =>
    rw [(isNormal_opow (one_lt_omega0.trans_le ha)).apply_of_isSuccLimit hb]
    exact card_iSup_Iio_le (le_max_right ..) fun i ↦
      (IH i i.2).trans (max_le_max_left _ (card_le_card i.2.le))
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
zero : (HPow.hPow (β := Ordinal.{u_1}) a 0).card ≤ max a.card (card 0)
add_one : ∀ (b : Ordinal.{u_1}) (IH : (a ^ b).card ≤ max a.card b.card), (a ^ (b + 1)).card ≤ max a.card (b + 1).card
⊢ (a ^ b).card ≤ max a.card b.card
have limit : ∀ (b : Ordinal.{u_1}) (hb : Order.IsSuccLimit b) (IH : ∀ o' < b, (a ^ o').card ≤ max a.card o'.card),
  (a ^ b).card ≤ max a.card b.card
Tactic: induction b using limitRecOn with
  | zero => simpa using one_lt_omega0.le.trans ha
  | add_one b IH =>
    rw [opow_add_one, card_mul, card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]
    · grw [IH]
      rw [← max_assoc, max_self]
      grw [← le_self_add]
    · rw [ne_eq, card_eq_zero, opow_eq_zero]
      rintro ⟨rfl, -⟩
      cases omega0_pos.not_ge ha
    · rwa [aleph0_le_card]
  | limit b hb IH =>
    rw [(isNormal_opow (one_lt_omega0.trans_le ha)).apply_of_isSuccLimit hb]
    exact card_iSup_Iio_le (le_max_right ..) fun i ↦
      (IH i i.2).trans (max_le_max_left _ (card_le_card i.2.le))
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
hb : ω ≤ b
⊢ (a ^ b).card ≤ max a.card b.card
have inl : ∀ (n : ℕ), (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max (card (↑n : Ordinal.{u_1})) b.card
Tactic: obtain ⟨n, rfl⟩ | ha := eq_natCast_or_omega0_le a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
hb : ω ≤ b
inl : ∀ (n : ℕ), (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max (card (↑n : Ordinal.{u_1})) b.card
⊢ (a ^ b).card ≤ max a.card b.card
have inr : ∀ (ha : ω ≤ a), (a ^ b).card ≤ max a.card b.card
Tactic: obtain ⟨n, rfl⟩ | ha := eq_natCast_or_omega0_le a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
⊢ (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max (card (↑n : Ordinal.{u_1})) b.card
have inl : (ω ^ b).card ≤ max (card (↑n : Ordinal.{u_1})) b.card
Tactic: apply (card_le_card <| opow_le_opow_left b (natCast_lt_omega0 n).le).trans
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
⊢ (ω ^ b).card ≤ max (card (↑n : Ordinal.{u_1})) b.card
have inl : max ω.card b.card ≤ max (card (↑n : Ordinal.{u_1})) b.card
Tactic: apply (card_opow_le_of_omega0_le_left le_rfl _).trans
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
⊢ (a ^ b).card ≤ max ℵ₀ (max a.card b.card)
have inl : ∀ (n : ℕ),
  (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) b.card)
Tactic: obtain ⟨n, rfl⟩ | ha := eq_natCast_or_omega0_le a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
inl :
  ∀ (n : ℕ),
    (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) b.card)
⊢ (a ^ b).card ≤ max ℵ₀ (max a.card b.card)
have inr : ∀ (ha : ω ≤ a), (a ^ b).card ≤ max ℵ₀ (max a.card b.card)
Tactic: obtain ⟨n, rfl⟩ | ha := eq_natCast_or_omega0_le a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
b : Ordinal.{u_1}
n : ℕ
⊢ (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) b.card)
have inl : ∀ (m : ℕ),
  (HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) (↑m : Ordinal.{u_1})).card ≤
    max ℵ₀ (max (card (↑n : Ordinal.{u_1})) (card (↑m : Ordinal.{u_1})))
Tactic: obtain ⟨m, rfl⟩ | hb := eq_natCast_or_omega0_le b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
b : Ordinal.{u_1}
n : ℕ
inl :
  ∀ (m : ℕ),
    (HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) (↑m : Ordinal.{u_1})).card ≤
      max ℵ₀ (max (card (↑n : Ordinal.{u_1})) (card (↑m : Ordinal.{u_1})))
⊢ (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) b.card)
have inl₁ : ∀ (hb : ω ≤ b),
  (HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) b).card ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) b.card)
Tactic: obtain ⟨m, rfl⟩ | hb := eq_natCast_or_omega0_le b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
n m : ℕ
⊢ (HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) (↑m : Ordinal.{u_1})).card ≤
    max ℵ₀ (max (card (↑n : Ordinal.{u_1})) (card (↑m : Ordinal.{u_1})))
have inl : (↑(n ^ m) : Cardinal.{u_1}) ≤ max ℵ₀ (max (card (↑n : Ordinal.{u_1})) (card (↑m : Ordinal.{u_1})))
Tactic: rw [opow_natCast, ← natCast_pow, card_nat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ (a ^ b).card = max a.card b.card
have apply : a.card ≤ (a ^ b).card
Tactic: apply (card_opow_le_of_omega0_le_left ha b).antisymm (max_le _ _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
apply : a.card ≤ (a ^ b).card
⊢ (a ^ b).card = max a.card b.card
have apply₁ : b.card ≤ (a ^ b).card
Tactic: apply (card_opow_le_of_omega0_le_left ha b).antisymm (max_le _ _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ a.card ≤ (a ^ b).card
have a₁ : a ≤ a ^ b
Tactic: apply card_le_card
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b.card ≤ (a ^ b).card
have a₁ : b ≤ a ^ b
Tactic: apply card_le_card
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ (a ^ b).card = max a.card b.card
have apply : a.card ≤ (a ^ b).card
Tactic: apply (card_opow_le_of_omega0_le_right a hb).antisymm (max_le _ _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
apply : a.card ≤ (a ^ b).card
⊢ (a ^ b).card = max a.card b.card
have apply₁ : b.card ≤ (a ^ b).card
Tactic: apply (card_opow_le_of_omega0_le_right a hb).antisymm (max_le _ _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ a.card ≤ (a ^ b).card
have a₁ : a ≤ a ^ b
Tactic: apply card_le_card
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ b.card ≤ (a ^ b).card
have a₁ : b ≤ a ^ b
Tactic: apply card_le_card
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
h : a ≠ 0
⊢ (ω ^ a).card = max ℵ₀ a.card
have rw : max ω.card a.card = max ℵ₀ a.card
Tactic: rw [card_opow_eq_of_omega0_le_left le_rfl h.bot_lt, card_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
h : a ≠ 0
rw : max ω.card a.card = max ℵ₀ a.card
⊢ (ω ^ a).card = max ℵ₀ a.card
have rw₁ : max ℵ₀ a.card = max ℵ₀ a.card
Tactic: rw [card_opow_eq_of_omega0_le_left le_rfl h.bot_lt, card_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
h : 1 < a
⊢ (a ^ ω).card = max ℵ₀ a.card
have rw : max a.card ω.card = max ℵ₀ a.card
Tactic: rw [card_opow_eq_of_omega0_le_right h le_rfl, card_omega0, max_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
h : 1 < a
rw : max a.card ω.card = max ℵ₀ a.card
⊢ (a ^ ω).card = max ℵ₀ a.card
have rw₁ : max a.card ℵ₀ = max ℵ₀ a.card
Tactic: rw [card_opow_eq_of_omega0_le_right h le_rfl, card_omega0, max_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
a : Ordinal.{u_1}
h : 1 < a
rw : max a.card ω.card = max ℵ₀ a.card
rw₁ : max a.card ℵ₀ = max ℵ₀ a.card
⊢ (a ^ ω).card = max ℵ₀ a.card
have rw₂ : max ℵ₀ a.card = max ℵ₀ a.card
Tactic: rw [card_opow_eq_of_omega0_le_right h le_rfl, card_omega0, max_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o)
have inl : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)
Tactic: obtain rfl | ho := eq_zero_or_pos o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
inl : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o)
have inr : ∀ (ho : 0 < o), IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o)
Tactic: obtain rfl | ho := eq_zero_or_pos o
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0)
have inl : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ω
Tactic: rw [omega_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o
hb : b < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o
⊢ LT.lt (α := Ordinal.{u_1}) ((fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) a b : Ordinal.{u_1})
    ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o : Ordinal.{u_1})
have inr : ∀ (ha : a.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)
  (hb : b.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o),
  card ((fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) a b) < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
Tactic: rw [lt_omega_iff_card_lt] at ha hb ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
hb : b.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
⊢ card ((fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) a b) < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
have apply : ℵ₀ < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
Tactic: apply (card_opow_le a b).trans_lt (max_lt _ (max_lt ha hb))
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
hb : b.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
⊢ ℵ₀ < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
have rwa : LT.lt (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0 : Cardinal.{u_1})
  ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
Tactic: rwa [← aleph_zero, aleph_lt_aleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) o
have obtain : ∀ (a : Ordinal.{u_1}) (h : IsInitial.{u_1} ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a))
  (ho : ω ≤ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a),
  IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)
Tactic: obtain ⟨a, rfl⟩ := mem_range_omega_iff.2 ⟨ho, h⟩
Cleared hypotheses: o, h, ho
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) c.ord
have apply : ω ≤ c.ord
Tactic: apply (isInitial_ord c).isPrincipal_opow
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
hb : b < c.ord
⊢ (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) a b < c.ord
have rw : ∀ (ha : a.card < c) (hb : b.card < c), a.card + b.card < c
Tactic: rw [lt_ord, card_add] at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) o
have rw : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) o.card.ord
Tactic: rw [← h.ord_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) o.card.ord
have hc : ℵ₀ ≤ o.card
Tactic: apply isPrincipal_add_ord
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
hb : b < c.ord
⊢ (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) a b < c.ord
have rw : ∀ (ha : a.card < c) (hb : b.card < c), a.card * b.card < c
Tactic: rw [lt_ord, card_mul] at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) o
have rw : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) o.card.ord
Tactic: rw [← h.ord_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) o.card.ord
have hc : ℵ₀ ≤ o.card
Tactic: apply isPrincipal_mul_ord
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
⊢ ∃ (a : α), #β ≤ #(↑(f ⁻¹' {a}) : Type u)
have by_contra! : ∀ (h : ∀ (a : α), #(↑(f ⁻¹' {a}) : Type u) < #β), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #(↑(f ⁻¹' {a}) : Type u) < #β
⊢ False
have apply : #(↑Set.univ : Type u) < #β
Tactic: apply mk_univ.not_lt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (hypothesis)
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
⊢ ∃ (a : α), #(↑(f ⁻¹' {a}) : Type u) = #β
have this : ∃ (a : α), #β ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: have : ∃ a, #β ≤ #(f ⁻¹' {a}) := by
    by_contra! h
    apply mk_univ.not_lt
    rw [← preimage_univ, ← iUnion_of_singleton, preimage_iUnion]
    exact
      mk_iUnion_le_sum_mk.trans_lt <| (sum_le_mk_mul_iSup _).trans_lt <|
        mul_lt_of_lt h₁ (h₂.trans_le <| cof_ord_le _) (iSup_lt_of_lt_cof_ord h₂ h)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
this : ∃ (a : α), #β ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), #(↑(f ⁻¹' {a}) : Type u) = #β
have obtain : ∀ (x : α) (h : #β ≤ #(↑(f ⁻¹' {x}) : Type u)), ∃ (a : α), #(↑(f ⁻¹' {a}) : Type u) = #β
Tactic: obtain ⟨x, h⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #(↑(f ⁻¹' {x}) : Type u)
⊢ ∃ (a : α), #(↑(f ⁻¹' {a}) : Type u) = #β
have refine : #(↑(f ⁻¹' {x}) : Type u) ≤ #β
Tactic: refine ⟨x, h.antisymm' ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #(↑(f ⁻¹' {x}) : Type u)
⊢ #(↑(f ⁻¹' {x}) : Type u) ≤ #β
have rw : ∃ (p : Set β), #(↑p : Type u) = #(↑(f ⁻¹' {x}) : Type u)
Tactic: rw [le_mk_iff_exists_set]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
θ : Cardinal.{u}
hθ : θ ≤ #β
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
⊢ ∃ (a : α), θ ≤ #(↑(f ⁻¹' {a}) : Type u)
have rcases : ∀ (s : Set β) (hθ : #(↑s : Type u) ≤ #β) (h₁ : ℵ₀ ≤ #(↑s : Type u)) (h₂ : #α < (#(↑s : Type u)).ord.cof),
  ∃ (a : α), #(↑s : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: rcases le_mk_iff_exists_set.1 hθ with ⟨s, rfl⟩
Cleared hypotheses: θ, hθ, h₁, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
s : Set β
hθ : #(↑s : Type u) ≤ #β
h₁ : ℵ₀ ≤ #(↑s : Type u)
h₂ : #α < (#(↑s : Type u)).ord.cof
⊢ ∃ (a : α), #(↑s : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)
have obtain : ∀ (a : α) (ha : #(↑(f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' {a}) : Type u) = #(↑s : Type u)),
  ∃ (a : α), #(↑s : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: obtain ⟨a, ha⟩ := infinite_pigeonhole (f ∘ Subtype.val : s → α) h₁ h₂
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
s : Set β
hθ : #(↑s : Type u) ≤ #β
h₁ : ℵ₀ ≤ #(↑s : Type u)
h₂ : #α < (#(↑s : Type u)).ord.cof
a : α
ha : #(↑(f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' {a}) : Type u) = #(↑s : Type u)
⊢ ∃ (a : α), #(↑s : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)
have h : #(↑s : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: use a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
s : Set β
hθ : #(↑s : Type u) ≤ #β
h₁ : ℵ₀ ≤ #(↑s : Type u)
h₂ : #α < (#(↑s : Type u)).ord.cof
a : α
ha : #(↑(f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' {a}) : Type u) = #(↑s : Type u)
⊢ #(↑s : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)
have h : #(↑(Subtype.val (p := fun (x : β) ↦ x ∈ s) ⁻¹' f ⁻¹' {a}) : Type u) ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: rw [← ha, @preimage_comp _ _ _ Subtype.val f]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
⊢ ∃ (a : α) (t : Set β) (h : t ⊆ s),
    θ ≤ #(↑t : Type u) ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x ⋯) = a
have obtain : ∀ (a : α) (ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)),
  ∃ (a : α) (t : Set β) (h : t ⊆ s),
    θ ≤ #(↑t : Type u) ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x sorry) = a
Tactic: obtain ⟨a, ha⟩ := infinite_pigeonhole_card f θ hθ h₁ h₂
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α) (t : Set β) (h : t ⊆ s),
    θ ≤ #(↑t : Type u) ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x ⋯) = a
have refine_1 : {x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} ⊆ s
Tactic: refine ⟨a, { x | ∃ h, f ⟨x, h⟩ = a }, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
refine_1 : {x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} ⊆ s
⊢ ∃ (a : α) (t : Set β) (h : t ⊆ s),
    θ ≤ #(↑t : Type u) ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x ⋯) = a
have refine_2 : θ ≤ #(↑{x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} : Type u)
Tactic: refine ⟨a, { x | ∃ h, f ⟨x, h⟩ = a }, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
refine_1 : {x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} ⊆ s
refine_2 : θ ≤ #(↑{x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} : Type u)
⊢ ∃ (a : α) (t : Set β) (h : t ⊆ s),
    θ ≤ #(↑t : Type u) ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x ⋯) = a
have refine_3 : ∀ ⦃x : β⦄
  (hx : Membership.mem (γ := Set β) {x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} x),
  f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x sorry) = a
Tactic: refine ⟨a, { x | ∃ h, f ⟨x, h⟩ = a }, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
s : Set β
f : (↑s : Type u) → α
θ : Cardinal.{u}
hθ : θ ≤ #(↑s : Type u)
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ θ ≤ #(↑{x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} : Type u)
have refine_2 : (↑{x : β | ∃ (h : x ∈ s), f (Subtype.mk (p := fun (x : β) ↦ x ∈ s) x h) = a} : Type u) ≃
  { a_1 : β // ∃ (h : a_1 ∈ s), Subtype.mk (p := fun (x : β) ↦ x ∈ s) a_1 h ∈ f ⁻¹' {a} }
Tactic: refine
      ha.trans
        (ge_of_eq <|
          Quotient.sound ⟨Equiv.trans ?_ (Equiv.subtypeSubtypeEquivSubtypeExists _ _).symm⟩)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
⊢ ∃ (a : α), #α < #(↑(f ⁻¹' {a}) : Type u)
have simp_rw : ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: simp_rw [← succ_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
⊢ ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)
have inl : ∀ (hα : #α < ℵ₀), ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: rcases lt_or_ge #α ℵ₀ with hα | hα
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
inl : ∀ (hα : #α < ℵ₀), ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)
have inr : ∀ (hα : ℵ₀ ≤ #α), ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: rcases lt_or_ge #α ℵ₀ with hα | hα
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : #α < ℵ₀
⊢ ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)
have inl : ∀ (a : α) (ha : ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)), ∃ (a : α), succ #α ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: obtain ⟨a, ha⟩ := infinite_pigeonhole_card f ℵ₀ hβ le_rfl
      (by rwa [isRegular_aleph0.cof_ord])
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite β
⊢ ∃ (a : α), Infinite.{u + 1} (↑(f ⁻¹' {a}) : Type u)
have simp_rw : ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: simp_rw [Cardinal.infinite_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite β
⊢ ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
have inl : ∀ (hα : #α < ℵ₀), ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: rcases lt_or_ge #α ℵ₀ with hα | hα