awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
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
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c

Tactic:
wlog hℵ₀b : ℵ₀ ≤ b
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
apply₁ : ℵ₀ ≤ c * b
⊢ (↑n : Cardinal.{u_1}) ∣ b ∨ (↑n : Cardinal.{u_1}) ∣ c

Tactic:
apply (this h c b _ _ hc hb hℵ₀.symm hn (hℵ₀.resolve_left hℵ₀b)).symm

Premises used: Or.resolve_left, Or.symm
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
rwa rwa₁ rwa₂ 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
⊢ (↑n : Cardinal.{u_1}) ∣ c * b

Tactic:
rwa [mul_comm] at hbc

Premises used: mul_comm
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
rwa rwa₁ rwa₂ 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
⊢ ℵ₀ ≤ c * b

Tactic:
rwa [mul_comm] at h'

Premises used: mul_comm
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n_1 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:
Or.inl (dvd_of_le_of_aleph0_le hn (natCast_lt_aleph0.le.trans hℵ₀b) hℵ₀b)

Premises used: LT.lt.le, Cardinal.natCast_lt_aleph0, Cardinal.dvd_of_le_of_aleph0_le, Or.inl, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
n_1 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:
exact Or.inl (dvd_of_le_of_aleph0_le hn (natCast_lt_aleph0.le.trans hℵ₀b) hℵ₀b)

Premises used: LT.lt.le, Cardinal.natCast_lt_aleph0, Cardinal.dvd_of_le_of_aleph0_le, Or.inl, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u_1}
inl : ∀ (h : ℵ₀ ≤ a), Prime a ↔ ℵ₀ ≤ a ∨ ∃ (p : ℕ), a = (↑p : Cardinal.{u_1}) ∧ Nat.Prime p
inr : ∀ (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

Tactic:
rcases le_or_gt ℵ₀ a with h | h

Premises used: Cardinal.aleph0, le_or_gt
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ (p : ℕ), a = (↑p : Cardinal.{u_1}) ∧ Nat.Prime p

Tactic:
simp [h]
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u_1}
h : a < ℵ₀
⊢ a < ℵ₀

Tactic:
id h

Premises used: id
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u_1}
h : a < ℵ₀
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
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ (p : ℕ), a = (↑p : Cardinal.{u_1}) ∧ Nat.Prime p

Tactic:
lift a to ℕ using id h

Premises used: id
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
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:
simp [not_le.mpr h]

Premises used: not_le, Iff.mpr
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u_1}
pos : ∀ (h : ℵ₀ ≤ a), IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ IsPrimePow n
neg : ∀ (h : ¬ℵ₀ ≤ a), IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ IsPrimePow n
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ IsPrimePow n

Tactic:
by_cases h : ℵ₀ ≤ a
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ IsPrimePow n

Tactic:
simp [h, (prime_of_aleph0_le h).isPrimePow]

Premises used: Cardinal.prime_of_aleph0_le, Prime.isPrimePow
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u_1}
h : ¬ℵ₀ ≤ a
neg : IsPrimePow a ↔ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ IsPrimePow n

Tactic:
simp only [h, false_or, isPrimePow_nat_iff]

Premises used: isPrimePow_nat_iff, false_or
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u_1}
h : ¬ℵ₀ ≤ a
⊢ a < ℵ₀

Tactic:
not_le.mp h

Premises used: not_le, Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u_1}
h : ¬ℵ₀ ≤ a
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
⊢ IsPrimePow a ↔ ∃ (n : ℕ), a = (↑n : Cardinal.{u_1}) ∧ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
lift a to ℕ using not_le.mp h

Premises used: not_le, Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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
rw : HPow.hPow (α := Cardinal.{u_1}) (↑p : Cardinal.{u_1}) k = (↑n : Cardinal.{u_1})
⊢ HPow.hPow (α := Cardinal.{u_1}) (↑p : Cardinal.{u_1}) k = (↑a : Cardinal.{u_1})

Tactic:
rw [han]
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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 = (↑n : Cardinal.{u_1})

Tactic:
mod_cast h

Premises used: congrArg, cast, Nat.cast, Nat.cast_inj._simp_1, congrFun', Eq.symm, Eq, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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 = (↑n : Cardinal.{u_1})

Tactic:
exact mod_cast h
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : ℕ
h : ¬ℵ₀ ≤ (↑a : Cardinal.{u_1})
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
⊢ (∃ (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⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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})
rw : HPow.hPow (β := Cardinal.{u_1}) p 1 ≤ p ^ k
⊢ HPow.hPow (β := Cardinal.{u_1}) p 1 ≤ (↑a : Cardinal.{u_1})

Tactic:
rw [← hpk]
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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})
apply : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑k : Cardinal.{u_1})
⊢ HPow.hPow (β := Cardinal.{u_1}) p 1 ≤ p ^ k

Tactic:
apply power_le_power_left hp.ne_zero

Premises used: Prime.ne_zero, Cardinal.power_le_power_left
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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})
⊢ LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑k : Cardinal.{u_1})

Tactic:
mod_cast hk

Premises used: congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, congrFun', Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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})
⊢ LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑k : Cardinal.{u_1})

Tactic:
exact mod_cast hk
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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})

Tactic:
have key : p ^ (1 : Cardinal) ≤ ↑a := by
    rw [← hpk]; apply power_le_power_left hp.ne_zero; exact mod_cast hk
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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})
⊢ p ≤ (↑a : Cardinal.{u_1})

Tactic:
rw [power_one] at key

Premises used: Cardinal.power_one
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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})
⊢ p < ℵ₀

Tactic:
key.trans_lt natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
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})
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
⊢ ∃ (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

Premises used: Cardinal.natCast_lt_aleph0, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : ℕ
h : ¬ℵ₀ ≤ (↑a : Cardinal.{u_1})
k : ℕ
hk : 0 < k
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:
⟨a, rfl, p, k, nat_is_prime_iff.mp hp, hk, mod_cast hpk⟩

Premises used: congrArg, cast, Nat.cast, And.intro, Cardinal.nat_is_prime_iff, Exists.intro, Iff.mp, Nat.cast_inj._simp_1, congrFun', Eq, rfl, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : ℕ
h : ¬ℵ₀ ≤ (↑a : Cardinal.{u_1})
k : ℕ
hk : 0 < k
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:
exact ⟨a, rfl, p, k, nat_is_prime_iff.mp hp, hk, mod_cast hpk⟩
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ (↑⊤ : Cardinal.{u_1}) = ℵ₀

Tactic:
rfl

Premises used: Cardinal.ofENat, rfl
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ
⊢ (↑(↑n : ℕ∞) : Cardinal.{u_1}) = (↑n : Cardinal.{u_1})

Tactic:
rfl

Premises used: Cardinal.ofENat, rfl
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ (↑0 : Cardinal.{u_1}) = 0

Tactic:
rfl

Premises used: Cardinal.ofENat, rfl
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ (↑1 : Cardinal.{u_1}) = 1

Tactic:
rfl

Premises used: Cardinal.ofENat, rfl
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ (↑(OfNat.ofNat n) : Cardinal.{u_1}) = OfNat.ofNat n

Tactic:
rfl

Premises used: Cardinal.ofENat, rfl
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ StrictMono ofENat

Tactic:
WithTop.strictMono_iff.2 ⟨Nat.strictMono_cast, fun _ ↦ natCast_lt_aleph0⟩

Premises used: Iff.mpr, Cardinal.natCast_lt_aleph0, ENat, And.intro, Nat.strictMono_cast, WithTop.strictMono_iff
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m n : ℕ∞
⊢ (↑m : Cardinal.{u_1}) < (↑n : Cardinal.{u_1}) ↔ m < n

Tactic:
ofENat_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Cardinal.ofENat_strictMono
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
⊢ (↑m : Cardinal.{u_1}) < ℵ₀ ↔ m < ⊤

Tactic:
ofENat_lt_ofENat (n := ⊤)

Premises used: Cardinal.ofENat_lt_ofENat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
n : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : m < (↑n : ℕ∞) ↔ m < (↑n : ℕ∞)
⊢ (↑m : Cardinal.{u_1}) < (↑n : Cardinal.{u_1}) ↔ m < (↑n : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
n : ℕ
inst : n.AtLeastTwo
⊢ (↑m : Cardinal.{u_1}) < OfNat.ofNat n ↔ m < OfNat.ofNat n

Tactic:
ofENat_lt_nat

Premises used: Cardinal.ofENat_lt_nat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ
n : ℕ∞
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑m : ℕ∞) < n ↔ (↑m : ℕ∞) < n
⊢ (↑m : Cardinal.{u_1}) < (↑n : Cardinal.{u_1}) ↔ (↑m : ℕ∞) < n

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 < m ↔ 0 < m
⊢ 0 < (↑m : Cardinal.{u_1}) ↔ 0 < m

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 < m ↔ 1 < m
⊢ 1 < (↑m : Cardinal.{u_1}) ↔ 1 < m

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ
inst : m.AtLeastTwo
n : ℕ∞
⊢ OfNat.ofNat m < (↑n : Cardinal.{u_1}) ↔ OfNat.ofNat m < n

Tactic:
nat_lt_ofENat

Premises used: Cardinal.nat_lt_ofENat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ Monotone ofENat

Tactic:
ofENat_strictMono.monotone

Premises used: StrictMono.monotone, Cardinal.ofENat_strictMono
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m n : ℕ∞
⊢ (↑m : Cardinal.{u_1}) ≤ (↑n : Cardinal.{u_1}) ↔ m ≤ n

Tactic:
ofENat_strictMono.le_iff_le

Premises used: Cardinal.ofENat_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ∞
⊢ (↑n : Cardinal.{u_1}) ≤ ℵ₀

Tactic:
ofENat_le_ofENat.2 le_top

Premises used: Iff.mpr, Cardinal.ofENat_le_ofENat, le_top
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
n : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : m ≤ (↑n : ℕ∞) ↔ m ≤ (↑n : ℕ∞)
⊢ (↑m : Cardinal.{u_1}) ≤ (↑n : Cardinal.{u_1}) ↔ m ≤ (↑n : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : m ≤ 1 ↔ m ≤ 1
⊢ (↑m : Cardinal.{u_1}) ≤ 1 ↔ m ≤ 1

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
n : ℕ
inst : n.AtLeastTwo
⊢ (↑m : Cardinal.{u_1}) ≤ OfNat.ofNat n ↔ m ≤ OfNat.ofNat n

Tactic:
ofENat_le_nat

Premises used: Cardinal.ofENat_le_nat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ
n : ℕ∞
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑m : ℕ∞) ≤ n ↔ (↑m : ℕ∞) ≤ n
⊢ (↑m : Cardinal.{u_1}) ≤ (↑n : Cardinal.{u_1}) ↔ (↑m : ℕ∞) ≤ n

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
n : ℕ∞
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 ≤ n ↔ 1 ≤ n
⊢ 1 ≤ (↑n : Cardinal.{u_1}) ↔ 1 ≤ n

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ
inst : m.AtLeastTwo
n : ℕ∞
⊢ OfNat.ofNat m ≤ (↑n : Cardinal.{u_1}) ↔ OfNat.ofNat m ≤ n

Tactic:
nat_le_ofENat

Premises used: Cardinal.nat_le_ofENat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
⊢ Injective ofENat

Tactic:
ofENat_strictMono.injective

Premises used: StrictMono.injective, Cardinal.ofENat_strictMono
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m n : ℕ∞
⊢ (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) ↔ m = n

Tactic:
ofENat_injective.eq_iff

Premises used: Function.Injective.eq_iff, Cardinal.ofENat_injective
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
n : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : m = (↑n : ℕ∞) ↔ m = (↑n : ℕ∞)
⊢ (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) ↔ m = (↑n : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ
n : ℕ∞
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑m : ℕ∞) = n ↔ (↑m : ℕ∞) = n
⊢ (↑m : Cardinal.{u_1}) = (↑n : Cardinal.{u_1}) ↔ (↑m : ℕ∞) = n

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : m = 0 ↔ m = 0
⊢ (↑m : Cardinal.{u_1}) = 0 ↔ m = 0

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
norm_cast : 0 = m ↔ m = 0
⊢ 0 = (↑m : Cardinal.{u_1}) ↔ m = 0

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
⊢ 0 = m ↔ m = 0

Tactic:
apply eq_comm

Premises used: eq_comm
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : m = 1 ↔ m = 1
⊢ (↑m : Cardinal.{u_1}) = 1 ↔ m = 1

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
norm_cast : 1 = m ↔ m = 1
⊢ 1 = (↑m : Cardinal.{u_1}) ↔ m = 1

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
⊢ 1 = m ↔ m = 1

Tactic:
apply eq_comm

Premises used: eq_comm
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ∞
n : ℕ
inst : n.AtLeastTwo
⊢ (↑m : Cardinal.{u_1}) = OfNat.ofNat n ↔ m = OfNat.ofNat n

Tactic:
ofENat_eq_nat

Premises used: Cardinal.ofENat_eq_nat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
m : ℕ
n : ℕ∞
inst : m.AtLeastTwo
⊢ OfNat.ofNat m = (↑n : Cardinal.{u_1}) ↔ OfNat.ofNat m = n

Tactic:
nat_eq_ofENat

Premises used: Cardinal.nat_eq_ofENat
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{v}
m : ℕ∞
rw : lift.{u, v} x < lift.{u, v} (↑m : Cardinal.{v}) ↔ x < (↑m : Cardinal.{v})
rw₁ rw₂ : x < (↑m : Cardinal.{v}) ↔ x < (↑m : Cardinal.{v})
⊢ lift.{u, v} x < (↑m : Cardinal.{max u v}) ↔ x < (↑m : Cardinal.{v})

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

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{v}
m : ℕ∞
rw : lift.{u, v} x ≤ lift.{u, v} (↑m : Cardinal.{v}) ↔ x ≤ (↑m : Cardinal.{v})
rw₁ rw₂ : x ≤ (↑m : Cardinal.{v}) ↔ x ≤ (↑m : Cardinal.{v})
⊢ lift.{u, v} x ≤ (↑m : Cardinal.{max u v}) ↔ x ≤ (↑m : Cardinal.{v})

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

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{v}
m : ℕ∞
rw : lift.{u, v} x = lift.{u, v} (↑m : Cardinal.{v}) ↔ x = (↑m : Cardinal.{v})
rw₁ rw₂ : x = (↑m : Cardinal.{v}) ↔ x = (↑m : Cardinal.{v})
⊢ lift.{u, v} x = (↑m : Cardinal.{max u v}) ↔ x = (↑m : Cardinal.{v})

Tactic:
rw [← lift_ofENat.{u, v}, lift_inj]

Premises used: Cardinal.lift_inj
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{v}
m : ℕ∞
rw : lift.{u, v} (↑m : Cardinal.{v}) < lift.{u, v} x ↔ (↑m : Cardinal.{v}) < x
rw₁ rw₂ : (↑m : Cardinal.{v}) < x ↔ (↑m : Cardinal.{v}) < x
⊢ (↑m : Cardinal.{max u v}) < lift.{u, v} x ↔ (↑m : Cardinal.{v}) < x

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

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.ENat
Goal:
x : Cardinal.{v}
m : ℕ∞
rw : lift.{u, v} (↑m : Cardinal.{v}) ≤ lift.{u, v} x ↔ (↑m : Cardinal.{v}) ≤ x
rw₁ rw₂ : (↑m : Cardinal.{v}) ≤ x ↔ (↑m : Cardinal.{v}) ≤ x
⊢ (↑m : Cardinal.{max u v}) ≤ lift.{u, v} x ↔ (↑m : Cardinal.{v}) ≤ x

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

Premises used: Cardinal.lift_le