awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
refine_3 :
  ∀
    (this :
      ∀ {n : ℕ} (h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) (b c : Cardinal.{u_1})
        (hbc : (↑n : Cardinal.{u_1}) ∣ b * c) (h' : ℵ₀ ≤ b * c) (hb : b ≠ 0) (hc : c ≠ 0) (hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c)
        (hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (hℵ₀b : ℵ₀ ≤ b),
        (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c)
    (hℵ₀b : ¬ℵ₀ ≤ b), (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have wlog : ∀ {n : ℕ} (h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) (b c : Cardinal.{u_1}) (hbc : (↑n : Cardinal.{u_1}) ∣ b * c)
  (h' : ℵ₀ ≤ b * c) (hb : b ≠ 0) (hc : c ≠ 0) (hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c)
  (hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (hℵ₀b : ℵ₀ ≤ b),
  (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
Tactic: wlog hℵ₀b : ℵ₀ ≤ b
Cleared hypotheses: h, b, c, hbc, h', hb, hc, hℵ₀, hn
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
this :
  ∀ {n : ℕ} (h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) (b c : Cardinal.{u_1}) (hbc : (↑n : Cardinal.{u_1}) ∣ b * c)
    (h' : ℵ₀ ≤ b * c) (hb : b ≠ 0) (hc : c ≠ 0) (hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c)
    (hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (hℵ₀b : ℵ₀ ≤ b),
    (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have apply : (↑n : Cardinal.{u_1}) ∣ c * b
Tactic: apply (this h c b _ _ hc hb hℵ₀.symm hn (hℵ₀.resolve_left hℵ₀b)).symm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
this :
  ∀ {n : ℕ} (h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) (b c : Cardinal.{u_1}) (hbc : (↑n : Cardinal.{u_1}) ∣ b * c)
    (h' : ℵ₀ ≤ b * c) (hb : b ≠ 0) (hc : c ≠ 0) (hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c)
    (hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (hℵ₀b : ℵ₀ ≤ b),
    (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
apply : (↑n : Cardinal.{u_1}) ∣ c * b
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
have apply₁ : ℵ₀ ≤ c * b
Tactic: apply (this h c b _ _ hc hb hℵ₀.symm hn (hℵ₀.resolve_left hℵ₀b)).symm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
this :
  ∀ {n : ℕ} (h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) (b c : Cardinal.{u_1}) (hbc : (↑n : Cardinal.{u_1}) ∣ b * c)
    (h' : ℵ₀ ≤ b * c) (hb : b ≠ 0) (hc : c ≠ 0) (hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c)
    (hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (hℵ₀b : ℵ₀ ≤ b),
    (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ (↑n : Cardinal.{u_1}) ∣ c * b
have rwa : ∀ (hbc : (↑n : Cardinal.{u_1}) ∣ c * b) (h' : ℵ₀ ≤ b * c) (hb : b ≠ 0) (hc : c ≠ 0) (hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c)
  (hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0)
  (this :
    ∀ {n : ℕ} (h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) (b c : Cardinal.{u_1}) (hbc : (↑n : Cardinal.{u_1}) ∣ b * c)
      (h' : ℵ₀ ≤ b * c) (hb : b ≠ 0) (hc : c ≠ 0) (hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c)
      (hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (hℵ₀b : ℵ₀ ≤ b),
      (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c)
  (hℵ₀b : ¬ℵ₀ ≤ b), (↑n : Cardinal.{u_1}) ∣ c * b
Tactic: rwa [mul_comm] at hbc
Cleared hypotheses: hbc, h', hb, hc, hℵ₀, hn, this, hℵ₀b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : (↑n : Cardinal.{u_1}) ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0
this :
  ∀ {n : ℕ} (h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) (b c : Cardinal.{u_1}) (hbc : (↑n : Cardinal.{u_1}) ∣ b * c)
    (h' : ℵ₀ ≤ b * c) (hb : b ≠ 0) (hc : c ≠ 0) (hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c)
    (hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (hℵ₀b : ℵ₀ ≤ b),
    (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b
have rwa : ∀ (h' : ℵ₀ ≤ c * b) (hb : b ≠ 0) (hc : c ≠ 0) (hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c)
  (hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0)
  (this :
    ∀ {n : ℕ} (h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) (b c : Cardinal.{u_1}) (hbc : (↑n : Cardinal.{u_1}) ∣ b * c)
      (h' : ℵ₀ ≤ b * c) (hb : b ≠ 0) (hc : c ≠ 0) (hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c)
      (hn : Ne.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 0) (hℵ₀b : ℵ₀ ≤ b),
      (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c)
  (hℵ₀b : ¬ℵ₀ ≤ b), ℵ₀ ≤ c * b
Tactic: rwa [mul_comm] at h'
Cleared hypotheses: h', hb, hc, hℵ₀, hn, this, hℵ₀b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u_1}
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ (p : ℕ), a = (↑p : Cardinal.{u_1}) ∧ Nat.Prime p
have inl : ∀ (h : ℵ₀ ≤ a), Prime a ↔ ℵ₀ ≤ a ∨ ∃ (p : ℕ), a = (↑p : Cardinal.{u_1}) ∧ Nat.Prime p
Tactic: rcases le_or_gt ℵ₀ a with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u_1}
inl : ∀ (h : ℵ₀ ≤ a), Prime a ↔ ℵ₀ ≤ a ∨ ∃ (p : ℕ), a = (↑p : Cardinal.{u_1}) ∧ Nat.Prime p
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ (p : ℕ), a = (↑p : Cardinal.{u_1}) ∧ Nat.Prime p
have inr : ∀ (h : a < ℵ₀), Prime a ↔ ℵ₀ ≤ a ∨ ∃ (p : ℕ), a = (↑p : Cardinal.{u_1}) ∧ Nat.Prime p
Tactic: rcases le_or_gt ℵ₀ a with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u_1}
h : a < ℵ₀
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ (p : ℕ), a = (↑p : Cardinal.{u_1}) ∧ Nat.Prime p
have inr : ∀ (a : ℕ) (h : (↑a : Cardinal.{u_1}) < ℵ₀),
  Prime.{u_1 + 1} (M := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) ↔
    ℵ₀ ≤ (↑a : Cardinal.{u_1}) ∨
      ∃ (p : ℕ), Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑p : Cardinal.{u_1}) ∧ Nat.Prime p
Tactic: lift a to ℕ using id h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u_1}
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ IsPrimePow n
have pos : ∀ (h : ℵ₀ ≤ a), IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ IsPrimePow n
Tactic: by_cases h : ℵ₀ ≤ a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u_1}
pos : ∀ (h : ℵ₀ ≤ a), IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ IsPrimePow n
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ IsPrimePow n
have neg : ∀ (h : ¬ℵ₀ ≤ a), IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ IsPrimePow n
Tactic: by_cases h : ℵ₀ ≤ a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u_1}
h : ¬ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ IsPrimePow n
have neg : IsPrimePow a ↔ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Tactic: simp only [h, false_or, isPrimePow_nat_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : Cardinal.{u_1}
h : ¬ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have neg : ∀ (a : ℕ) (h : ¬ℵ₀ ≤ (↑a : Cardinal.{u_1})),
  IsPrimePow.{u_1 + 1} (R := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) ↔
    ∃ (n : ℕ),
      Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ∧
        ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Tactic: lift a to ℕ using not_le.mp h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : ℕ
h_1 : ¬ℵ₀ ≤ (↑a : Cardinal.{u_1})
h_2 :
  ∃ (n : ℕ),
    Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ∧
      ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
n : ℕ
han : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑n : Cardinal.{u_1})
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
h : p ^ k = n
⊢ HPow.hPow (α := Cardinal.{u_1}) (↑p : Cardinal.{u_1}) k = (↑a : Cardinal.{u_1})
have rw : HPow.hPow (α := Cardinal.{u_1}) (↑p : Cardinal.{u_1}) k = (↑n : Cardinal.{u_1})
Tactic: rw [han]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : ℕ
h : ¬ℵ₀ ≤ (↑a : Cardinal.{u_1})
⊢ (∃ (p : Cardinal.{u_1}) (k : ℕ), Prime p ∧ 0 < k ∧ p ^ k = (↑a : Cardinal.{u_1})) ↔
    ∃ (n : ℕ),
      Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ∧
        ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have neg : (∃ (p : Cardinal.{u_1}) (k : ℕ), Prime p ∧ 0 < k ∧ p ^ k = (↑a : Cardinal.{u_1})) →
  ∃ (n : ℕ),
    Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ∧
      ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Tactic: refine
    ⟨?_, fun ⟨n, han, p, k, hp, hk, h⟩ =>
          ⟨p, k, nat_is_prime_iff.2 hp, hk, by rw [han]; exact mod_cast h⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : ℕ
h : ¬ℵ₀ ≤ (↑a : Cardinal.{u_1})
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = (↑a : Cardinal.{u_1})
⊢ HPow.hPow (β := Cardinal.{u_1}) p 1 ≤ (↑a : Cardinal.{u_1})
have rw : HPow.hPow (β := Cardinal.{u_1}) p 1 ≤ p ^ k
Tactic: rw [← hpk]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : ℕ
h : ¬ℵ₀ ≤ (↑a : Cardinal.{u_1})
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = (↑a : Cardinal.{u_1})
⊢ HPow.hPow (β := Cardinal.{u_1}) p 1 ≤ p ^ k
have apply : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑k : Cardinal.{u_1})
Tactic: apply power_le_power_left hp.ne_zero
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
a : ℕ
h : ¬ℵ₀ ≤ (↑a : Cardinal.{u_1})
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = (↑a : Cardinal.{u_1})
⊢ ∃ (n : ℕ),
    Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ∧
      ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have key : HPow.hPow (β := Cardinal.{u_1}) p 1 ≤ (↑a : Cardinal.{u_1})
Tactic: have key : p ^ (1 : Cardinal) ≤ ↑a := by
    rw [← hpk]; apply power_le_power_left hp.ne_zero; exact mod_cast hk
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (hypothesis)
Goal:
a : ℕ
h : ¬ℵ₀ ≤ (↑a : Cardinal.{u_1})
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = (↑a : Cardinal.{u_1})
key : HPow.hPow (β := Cardinal.{u_1}) p 1 ≤ (↑a : Cardinal.{u_1})
⊢ ∃ (n : ℕ),
    Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ∧
      ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have key₁ : p ≤ (↑a : Cardinal.{u_1})
Tactic: rw [power_one] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Divisibility (goal)
Goal:
a : ℕ
h : ¬ℵ₀ ≤ (↑a : Cardinal.{u_1})
p : Cardinal.{u_1}
k : ℕ
hp : Prime p
hk : 0 < k
hpk : p ^ k = (↑a : Cardinal.{u_1})
key : p ≤ (↑a : Cardinal.{u_1})
⊢ ∃ (n : ℕ),
    Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ∧
      ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have neg : ∀ (p : ℕ) (hp : Prime.{u_1 + 1} (M := Cardinal.{u_1}) (↑p : Cardinal.{u_1}))
  (hpk : HPow.hPow (α := Cardinal.{u_1}) (↑p : Cardinal.{u_1}) k = (↑a : Cardinal.{u_1}))
  (key : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑p : Cardinal.{u_1}) (↑a : Cardinal.{u_1})),
  ∃ (n : ℕ),
    Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) ∧
      ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Tactic: lift p to ℕ using key.trans_lt natCast_lt_aleph0
Cleared hypotheses: p, hp, hpk, key
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
n : ℕ
⊢ (↑m : Cardinal.{u_1}) < (↑n : Cardinal.{u_1}) ↔ m < (↑n : ℕ∞)
have norm_cast : m < (↑n : ℕ∞) ↔ m < (↑n : ℕ∞)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ
n : ℕ∞
⊢ (↑m : Cardinal.{u_1}) < (↑n : Cardinal.{u_1}) ↔ (↑m : ℕ∞) < n
have norm_cast : (↑m : ℕ∞) < n ↔ (↑m : ℕ∞) < n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
⊢ 0 < (↑m : Cardinal.{u_1}) ↔ 0 < m
have norm_cast : 0 < m ↔ 0 < m
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
⊢ 1 < (↑m : Cardinal.{u_1}) ↔ 1 < m
have norm_cast : 1 < m ↔ 1 < m
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
n : ℕ
⊢ (↑m : Cardinal.{u_1}) ≤ (↑n : Cardinal.{u_1}) ↔ m ≤ (↑n : ℕ∞)
have norm_cast : m ≤ (↑n : ℕ∞) ↔ m ≤ (↑n : ℕ∞)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
⊢ (↑m : Cardinal.{u_1}) ≤ 1 ↔ m ≤ 1
have norm_cast : m ≤ 1 ↔ m ≤ 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ
n : ℕ∞
⊢ (↑m : Cardinal.{u_1}) ≤ (↑n : Cardinal.{u_1}) ↔ (↑m : ℕ∞) ≤ n
have norm_cast : (↑m : ℕ∞) ≤ n ↔ (↑m : ℕ∞) ≤ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
n : ℕ∞
⊢ 1 ≤ (↑n : Cardinal.{u_1}) ↔ 1 ≤ n
have norm_cast : 1 ≤ n ↔ 1 ≤ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
n : ℕ
⊢ (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) ↔ m = (↑n : ℕ∞)
have norm_cast : m = (↑n : ℕ∞) ↔ m = (↑n : ℕ∞)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ
n : ℕ∞
⊢ (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) ↔ (↑m : ℕ∞) = n
have norm_cast : (↑m : ℕ∞) = n ↔ (↑m : ℕ∞) = n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
⊢ (↑m : Cardinal.{u_1}) = 0 ↔ m = 0
have norm_cast : m = 0 ↔ m = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
⊢ 0 = (↑m : Cardinal.{u_1}) ↔ m = 0
have norm_cast : 0 = m ↔ m = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
⊢ (↑m : Cardinal.{u_1}) = 1 ↔ m = 1
have norm_cast : m = 1 ↔ m = 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
m : ℕ∞
⊢ 1 = (↑m : Cardinal.{u_1}) ↔ m = 1
have norm_cast : 1 = m ↔ m = 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} x < (↑m : Cardinal.{max u v}) ↔ x < (↑m : Cardinal.{v})
have rw : lift.{u, v} x < lift.{u, v} (↑m : Cardinal.{v}) ↔ x < (↑m : Cardinal.{v})
Tactic: rw [← lift_ofENat.{u, v}, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{v}
m : ℕ∞
rw : lift.{u, v} x < lift.{u, v} (↑m : Cardinal.{v}) ↔ x < (↑m : Cardinal.{v})
⊢ lift.{u, v} x < (↑m : Cardinal.{max u v}) ↔ x < (↑m : Cardinal.{v})
have rw₁ : x < (↑m : Cardinal.{v}) ↔ x < (↑m : Cardinal.{v})
Tactic: rw [← lift_ofENat.{u, v}, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} x ≤ (↑m : Cardinal.{max u v}) ↔ x ≤ (↑m : Cardinal.{v})
have rw : lift.{u, v} x ≤ lift.{u, v} (↑m : Cardinal.{v}) ↔ x ≤ (↑m : Cardinal.{v})
Tactic: rw [← lift_ofENat.{u, v}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{v}
m : ℕ∞
rw : lift.{u, v} x ≤ lift.{u, v} (↑m : Cardinal.{v}) ↔ x ≤ (↑m : Cardinal.{v})
⊢ lift.{u, v} x ≤ (↑m : Cardinal.{max u v}) ↔ x ≤ (↑m : Cardinal.{v})
have rw₁ : x ≤ (↑m : Cardinal.{v}) ↔ x ≤ (↑m : Cardinal.{v})
Tactic: rw [← lift_ofENat.{u, v}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} x = (↑m : Cardinal.{max u v}) ↔ x = (↑m : Cardinal.{v})
have rw : lift.{u, v} x = lift.{u, v} (↑m : Cardinal.{v}) ↔ x = (↑m : Cardinal.{v})
Tactic: rw [← lift_ofENat.{u, v}, lift_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{v}
m : ℕ∞
rw : lift.{u, v} x = lift.{u, v} (↑m : Cardinal.{v}) ↔ x = (↑m : Cardinal.{v})
⊢ lift.{u, v} x = (↑m : Cardinal.{max u v}) ↔ x = (↑m : Cardinal.{v})
have rw₁ : x = (↑m : Cardinal.{v}) ↔ x = (↑m : Cardinal.{v})
Tactic: rw [← lift_ofENat.{u, v}, lift_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{v}
m : ℕ∞
⊢ (↑m : Cardinal.{max u v}) < lift.{u, v} x ↔ (↑m : Cardinal.{v}) < x
have rw : lift.{u, v} (↑m : Cardinal.{v}) < lift.{u, v} x ↔ (↑m : Cardinal.{v}) < x
Tactic: rw [← lift_ofENat.{u, v}, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{v}
m : ℕ∞
rw : lift.{u, v} (↑m : Cardinal.{v}) < lift.{u, v} x ↔ (↑m : Cardinal.{v}) < x
⊢ (↑m : Cardinal.{max u v}) < lift.{u, v} x ↔ (↑m : Cardinal.{v}) < x
have rw₁ : (↑m : Cardinal.{v}) < x ↔ (↑m : Cardinal.{v}) < x
Tactic: rw [← lift_ofENat.{u, v}, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{v}
m : ℕ∞
⊢ (↑m : Cardinal.{max u v}) ≤ lift.{u, v} x ↔ (↑m : Cardinal.{v}) ≤ x
have rw : lift.{u, v} (↑m : Cardinal.{v}) ≤ lift.{u, v} x ↔ (↑m : Cardinal.{v}) ≤ x
Tactic: rw [← lift_ofENat.{u, v}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{v}
m : ℕ∞
rw : lift.{u, v} (↑m : Cardinal.{v}) ≤ lift.{u, v} x ↔ (↑m : Cardinal.{v}) ≤ x
⊢ (↑m : Cardinal.{max u v}) ≤ lift.{u, v} x ↔ (↑m : Cardinal.{v}) ≤ x
have rw₁ : (↑m : Cardinal.{v}) ≤ x ↔ (↑m : Cardinal.{v}) ≤ x
Tactic: rw [← lift_ofENat.{u, v}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{v}
m : ℕ∞
⊢ (↑m : Cardinal.{max u v}) = lift.{u, v} x ↔ (↑m : Cardinal.{v}) = x
have rw : lift.{u, v} (↑m : Cardinal.{v}) = lift.{u, v} x ↔ (↑m : Cardinal.{v}) = x
Tactic: rw [← lift_ofENat.{u, v}, lift_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{v}
m : ℕ∞
rw : lift.{u, v} (↑m : Cardinal.{v}) = lift.{u, v} x ↔ (↑m : Cardinal.{v}) = x
⊢ (↑m : Cardinal.{max u v}) = lift.{u, v} x ↔ (↑m : Cardinal.{v}) = x
have rw₁ : (↑m : Cardinal.{v}) = x ↔ (↑m : Cardinal.{v}) = x
Tactic: rw [← lift_ofENat.{u, v}, lift_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
⊢ range ofENat = Iic ℵ₀
have refine : ∀ (x : Cardinal.{u_1}) (hx : x ≤ ℵ₀), x ∈ range ofENat
Tactic: refine (range_subset_iff.2 ofENat_le_aleph0).antisymm fun x (hx : x ≤ ℵ₀) ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
⊢ x ∈ range ofENat
have inl : ∀ (hlt : x < ℵ₀), x ∈ range ofENat
Tactic: rcases hx.lt_or_eq with hlt | rfl
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
inl : ∀ (hlt : x < ℵ₀), x ∈ range ofENat
⊢ x ∈ range ofENat
have inr : ∀ (hx : ℵ₀ ≤ ℵ₀), ℵ₀ ∈ range ofENat
Tactic: rcases hx.lt_or_eq with hlt | rfl
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
hlt : x < ℵ₀
⊢ x ∈ range ofENat
have inl : ∀ (x : ℕ) (hx : (↑x : Cardinal.{u_1}) ≤ ℵ₀), (↑x : Cardinal.{u_1}) ∈ range ofENat
Tactic: lift x to ℕ using hlt
Cleared hypotheses: x, hx, hlt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
n : ℕ∞
x : Cardinal.{u_1}
hx : x < ℵ₀
⊢ (↑n : Cardinal.{u_1}) ≤ x ↔ n ≤ x.toENatAux
have inl : ∀ (x : ℕ), (↑n : Cardinal.{u_1}) ≤ (↑x : Cardinal.{u_1}) ↔ n ≤ toENatAux.{u_1} (↑x : Cardinal.{u_1})
Tactic: lift x to ℕ using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (hypothesis)
Goal:
n : ℕ∞
x : Cardinal.{u_1}
⊢ (↑n : Cardinal.{u_1}) ≤ x ↔ n ≤ x.toENatAux
have x₁ : x < ℵ₀ ∨ ℵ₀ ≤ x
Tactic: cases lt_or_ge x ℵ₀ with
  | inl hx => lift x to ℕ using hx; simp
  | inr hx => simp [toENatAux_eq_top hx, (ofENat_le_aleph0 n).trans hx]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x : Cardinal.{u_1}
n : ℕ
hx : x < ℵ₀
⊢ x.toENatAux ≤ (↑n : ℕ∞) ↔ x ≤ (↑n : Cardinal.{u_1})
have inl : ∀ (x : ℕ),
  toENatAux.{u_1} (↑x : Cardinal.{u_1}) ≤ (↑n : ℕ∞) ↔
    LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑x : Cardinal.{u_1}) (↑n : Cardinal.{u_1})
Tactic: lift x to ℕ using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (hypothesis)
Goal:
x : Cardinal.{u_1}
n : ℕ
⊢ x.toENatAux ≤ (↑n : ℕ∞) ↔ x ≤ (↑n : Cardinal.{u_1})
have x₁ : x < ℵ₀ ∨ ℵ₀ ≤ x
Tactic: cases lt_or_ge x ℵ₀ with
  | inl hx => lift x to ℕ using hx; simp
  | inr hx => simp [toENatAux_eq_top hx, natCast_lt_aleph0.trans_le hx]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
have inr : ∀ (this : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux) (hle : ¬x ≤ y),
  toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
Tactic: wlog hle : x ≤ y
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
inr :
  ∀ (this : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux) (hle : ¬x ≤ y),
    toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
have wlog : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
Tactic: wlog hle : x ≤ y
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
hle : ¬x ≤ y
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
have inr : toENatAux.{u} (y * x) = x.toENatAux * y.toENatAux
Tactic: rw [mul_comm, this y x (le_of_not_ge hle), mul_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
hle : ¬x ≤ y
inr : toENatAux.{u} (y * x) = x.toENatAux * y.toENatAux
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
have inr₁ : y.toENatAux * x.toENatAux = x.toENatAux * y.toENatAux
Tactic: rw [mul_comm, this y x (le_of_not_ge hle), mul_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}) (hle : x ≤ y), toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
hle : ¬x ≤ y
inr : toENatAux.{u} (y * x) = x.toENatAux * y.toENatAux
inr₁ : y.toENatAux * x.toENatAux = x.toENatAux * y.toENatAux
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
have inr₂ : x.toENatAux * y.toENatAux = x.toENatAux * y.toENatAux
Tactic: rw [mul_comm, this y x (le_of_not_ge hle), mul_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
x y : Cardinal.{u}
hle : x ≤ y
hy : y < ℵ₀
⊢ toENatAux.{u} (x * y) = x.toENatAux * y.toENatAux
have inl : ∀ (x : ℕ) (hle : (↑x : Cardinal.{u}) ≤ y),
  toENatAux.{u} ((↑x : Cardinal.{u}) * y) = toENatAux.{u} (↑x : Cardinal.{u}) * y.toENatAux
Tactic: lift x to ℕ using hle.trans_lt hy
Cleared hypotheses: x, hle
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ENat (goal)
Goal:
y : Cardinal.{u}
hy : y < ℵ₀
x : ℕ
hle : (↑x : Cardinal.{u}) ≤ y
⊢ toENatAux.{u} ((↑x : Cardinal.{u}) * y) = toENatAux.{u} (↑x : Cardinal.{u}) * y.toENatAux
have inl : ∀ (y : ℕ) (hle : LE.le.{u + 1} (α := Cardinal.{u}) (↑x : Cardinal.{u}) (↑y : Cardinal.{u})),
  toENatAux.{u} (HMul.hMul (α := Cardinal.{u}) (↑x : Cardinal.{u}) (↑y : Cardinal.{u})) =
    toENatAux.{u} (↑x : Cardinal.{u}) * toENatAux.{u} (↑y : Cardinal.{u})
Tactic: lift y to ℕ using hy
Cleared hypotheses: y, hy, hle