awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : { n : ℕ // IsPrimePow n }
⊢ (↑((fun (pk : Primes × ℕ) ↦
            (Subtype.mk (p := fun (n : ℕ) ↦ IsPrimePow n) ((↑pk.1 : ℕ) ^ (pk.2 + 1)) ⋯ : { n : ℕ // IsPrimePow n }))
          ((fun (n : { n : ℕ // IsPrimePow n }) ↦
              (Subtype.mk (p := fun (p : ℕ) ↦ Prime p) (↑n : ℕ).minFac ⋯,
                HSub.hSub (α := ℕ) (β := ℕ) (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) (1 : ℕ)))
            n)) :
      ℕ) =
    (↑n : ℕ)
have a : (↑n : ℕ).minFac ^
    (HSub.hSub (α := ℕ) (β := ℕ) (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) (1 : ℕ) + 1) =
  (↑n : ℕ)
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : { n : ℕ // IsPrimePow n }
⊢ (↑n : ℕ).minFac ^
      (HSub.hSub (α := ℕ) (β := ℕ) (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) (1 : ℕ) + 1) =
    (↑n : ℕ)
have a : HPow.hPow (β := ℕ) (↑n : ℕ).minFac (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) = (↑n : ℕ)
Tactic: rw [sub_one_add_one (Nat.factorization_minFac_ne_zero n.prop.one_lt),
      n.prop.minFac_pow_factorization_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : { n : ℕ // IsPrimePow n }
a : HPow.hPow (β := ℕ) (↑n : ℕ).minFac (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) = (↑n : ℕ)
⊢ (↑n : ℕ).minFac ^
      (HSub.hSub (α := ℕ) (β := ℕ) (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) (1 : ℕ) + 1) =
    (↑n : ℕ)
have a₁ : (↑n : ℕ) = (↑n : ℕ)
Tactic: rw [sub_one_add_one (Nat.factorization_minFac_ne_zero n.prop.one_lt),
      n.prop.minFac_pow_factorization_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (hypothesis)
Goal:
p a m n : ℕ
hp : Prime p
h : p ^ m = a ^ n
⊢ m = HMul.hMul (β := ℕ) n ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
have this : (p ^ m).factorization = (a ^ n).factorization
Tactic: have := congrArg Nat.factorization h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (hypothesis)
Goal:
p a m n : ℕ
hp : Prime p
h : p ^ m = a ^ n
this : (p ^ m).factorization = (a ^ n).factorization
⊢ m = HMul.hMul (β := ℕ) n ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
have this₁ : Finsupp.single p m = n • a.factorization
Tactic: rw [Nat.Prime.factorization_pow hp, Nat.factorization_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
p a m n : ℕ
hp : Prime p
hn : n ≠ 0
h : p ^ m = a ^ n
⊢ ∃ (k : ℕ), a = p ^ k
have rcases : ∀ (k : ℕ) (m_eq : m = n * k), ∃ (k : ℕ), a = p ^ k
Tactic: rcases exponent_dvd_of_prime_pow_eq_pow hp h with ⟨k, m_eq⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (hypothesis)
Goal:
p a m n : ℕ
hp : Prime p
hn : n ≠ 0
h : p ^ m = a ^ n
k : ℕ
m_eq : m = n * k
⊢ ∃ (k : ℕ), a = p ^ k
have h₁ : (p ^ k) ^ n = a ^ n
Tactic: rw [m_eq, pow_mul'] at h
Cleared hypotheses: h, m_eq
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
p a m n : ℕ
hp : Prime p
hn : n ≠ 0
k : ℕ
h : (p ^ k) ^ n = a ^ n
m_eq : m = n * k
⊢ ∃ (k : ℕ), a = p ^ k
have h₁ : a = p ^ k
Tactic: use k
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a n : ℕ
⊢ Eq (α := ℕ) (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun (p k : ℕ) ↦ p ^ (k / n))
    (if n = 0 ∨ a = 0 then 0
    else
      (@FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
            a.factorization n).prod
        fun (x1 x2 : ℕ) ↦ x1 ^ x2)
have pos : ∀ (h : n = 0 ∨ a = 0), Eq (α := ℕ) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a n : ℕ
pos : ∀ (h : n = 0 ∨ a = 0), Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun (p k : ℕ) ↦ p ^ (k / n))
    (if n = 0 ∨ a = 0 then 0
    else
      (@FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
            a.factorization n).prod
        fun (x1 x2 : ℕ) ↦ x1 ^ x2)
have neg : ∀ (h : ¬(n = 0 ∨ a = 0)),
  Eq (α := ℕ) (a.factorization.prod fun (p k : ℕ) ↦ p ^ (k / n))
    ((@FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
          a.factorization n).prod
      fun (x1 x2 : ℕ) ↦ x1 ^ x2)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a : ℕ
⊢ floorRoot 1 a = a
have simp : (if a = 0 then 0 else a.factorization.prod fun (p k : ℕ) ↦ p ^ k) = a
Tactic: simp [floorRoot]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun (p k : ℕ) ↦ p ^ k) = a
have pos : a = 0 → 0 = a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a : ℕ
pos : a = 0 → 0 = a
⊢ (if a = 0 then 0 else a.factorization.prod fun (p k : ℕ) ↦ p ^ k) = a
have neg : ¬a = 0 → (a.factorization.prod fun (p k : ℕ) ↦ p ^ k) = a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.floorRoot (a ^ n) = a
have simp : (if a = 0 then 0 else a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a
Tactic: simp [floorRoot_def, pos_iff_ne_zero.2, hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a
have pos : a = 0 → 0 = a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
pos : a = 0 → 0 = a
⊢ (if a = 0 then 0 else a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a
have neg : ¬a = 0 → (a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n a : ℕ
⊢ (n.floorRoot a).factorization =
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
have rw : factorization
    (if n = 0 ∨ a = 0 then 0
    else
      (@FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
            a.factorization n).prod
        fun (x1 x2 : ℕ) ↦ x1 ^ x2) =
  @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
    a.factorization n
Tactic: rw [floorRoot_def]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n a : ℕ
⊢ factorization
      (if n = 0 ∨ a = 0 then 0
      else
        (@FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass
              _ a.factorization n).prod
          fun (x1 x2 : ℕ) ↦ x1 ^ x2) =
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
have pos : ∀ (h : n = 0 ∨ a = 0),
  factorization 0 =
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n a : ℕ
pos :
  ∀ (h : n = 0 ∨ a = 0),
    factorization 0 =
      @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
        a.factorization n
⊢ factorization
      (if n = 0 ∨ a = 0 then 0
      else
        (@FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass
              _ a.factorization n).prod
          fun (x1 x2 : ℕ) ↦ x1 ^ x2) =
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
have neg : ∀ (h : ¬(n = 0 ∨ a = 0)),
  factorization
      ((@FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
            a.factorization n).prod
        fun (x1 x2 : ℕ) ↦ x1 ^ x2) =
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 =
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
have pos : factorization 0 =
  @FloorDiv.floorDiv ℕ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
    a.factorization 0
Tactic: obtain rfl | rfl := h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n a : ℕ
h : n = 0 ∨ a = 0
pos :
  factorization 0 =
    @FloorDiv.floorDiv ℕ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization 0
⊢ factorization 0 =
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
have pos₁ : factorization 0 =
  @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
    (factorization 0) n
Tactic: obtain rfl | rfl := h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ factorization
      ((@FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
            a.factorization n).prod
        fun (x1 x2 : ℕ) ↦ x1 ^ x2) =
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
have neg : @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
    a.factorization n ≤
  a.factorization
Tactic: apply a.factorization_prod_pow_eq_self_of_le_factorization
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
have inl : HPow.hPow (β := ℕ) a 0 ∣ b ↔ a ∣ floorRoot 0 b
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
inl : HPow.hPow (β := ℕ) a 0 ∣ b ↔ a ∣ floorRoot 0 b
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
have inr : ∀ (hn : n ≠ 0), a ^ n ∣ b ↔ a ∣ n.floorRoot b
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
have inr : a ^ n ∣ 0 ↔ a ∣ n.floorRoot 0
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
inr : a ^ n ∣ 0 ↔ a ∣ n.floorRoot 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
have inr₁ : ∀ (hb : b ≠ 0), a ^ n ∣ b ↔ a ∣ n.floorRoot b
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
have inr : HPow.hPow (α := ℕ) 0 n ∣ b ↔ 0 ∣ n.floorRoot b
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
inr : HPow.hPow (α := ℕ) 0 n ∣ b ↔ 0 ∣ n.floorRoot b
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
have inr₁ : ∀ (ha : a ≠ 0), a ^ n ∣ b ↔ a ∣ n.floorRoot b
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
have inr : (a ^ n).factorization ≤ b.factorization ↔ a ∣ n.floorRoot b
Tactic: rw [← factorization_le_iff_dvd (pow_ne_zero _ ha) hb,
    ← factorization_le_iff_dvd ha (floorRoot_ne_zero.2 ⟨hn, hb⟩), factorization_pow,
    factorization_floorRoot, le_floorDiv_iff_smul_le (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
inr : (a ^ n).factorization ≤ b.factorization ↔ a ∣ n.floorRoot b
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
have inr₁ : (a ^ n).factorization ≤ b.factorization ↔ a.factorization ≤ (n.floorRoot b).factorization
Tactic: rw [← factorization_le_iff_dvd (pow_ne_zero _ ha) hb,
    ← factorization_le_iff_dvd ha (floorRoot_ne_zero.2 ⟨hn, hb⟩), factorization_pow,
    factorization_floorRoot, le_floorDiv_iff_smul_le (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
inr : (a ^ n).factorization ≤ b.factorization ↔ a ∣ n.floorRoot b
inr₁ : (a ^ n).factorization ≤ b.factorization ↔ a.factorization ≤ (n.floorRoot b).factorization
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
have inr₂ : n • a.factorization ≤ b.factorization ↔ a.factorization ≤ (n.floorRoot b).factorization
Tactic: rw [← factorization_le_iff_dvd (pow_ne_zero _ ha) hb,
    ← factorization_le_iff_dvd ha (floorRoot_ne_zero.2 ⟨hn, hb⟩), factorization_pow,
    factorization_floorRoot, le_floorDiv_iff_smul_le (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
inr : (a ^ n).factorization ≤ b.factorization ↔ a ∣ n.floorRoot b
inr₁ : (a ^ n).factorization ≤ b.factorization ↔ a.factorization ≤ (n.floorRoot b).factorization
inr₂ : n • a.factorization ≤ b.factorization ↔ a.factorization ≤ (n.floorRoot b).factorization
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
have inr₃ : n • a.factorization ≤ b.factorization ↔
  a.factorization ≤
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      b.factorization n
Tactic: rw [← factorization_le_iff_dvd (pow_ne_zero _ ha) hb,
    ← factorization_le_iff_dvd ha (floorRoot_ne_zero.2 ⟨hn, hb⟩), factorization_pow,
    factorization_floorRoot, le_floorDiv_iff_smul_le (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
inr : (a ^ n).factorization ≤ b.factorization ↔ a ∣ n.floorRoot b
inr₁ : (a ^ n).factorization ≤ b.factorization ↔ a.factorization ≤ (n.floorRoot b).factorization
inr₂ : n • a.factorization ≤ b.factorization ↔ a.factorization ≤ (n.floorRoot b).factorization
inr₃ :
  n • a.factorization ≤ b.factorization ↔
    a.factorization ≤
      @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
        b.factorization n
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b
have inr₄ : n • a.factorization ≤ b.factorization ↔ n • a.factorization ≤ b.factorization
Tactic: rw [← factorization_le_iff_dvd (pow_ne_zero _ ha) hb,
    ← factorization_le_iff_dvd ha (floorRoot_ne_zero.2 ⟨hn, hb⟩), factorization_pow,
    factorization_floorRoot, le_floorDiv_iff_smul_le (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a n : ℕ
⊢ Eq (α := ℕ) (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun (p k : ℕ) ↦ p ^ ((k + n - 1) / n))
    (if n = 0 ∨ a = 0 then 0
    else
      (@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
            a.factorization n).prod
        fun (x1 x2 : ℕ) ↦ x1 ^ x2)
have pos : ∀ (h : n = 0 ∨ a = 0), Eq (α := ℕ) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a n : ℕ
pos : ∀ (h : n = 0 ∨ a = 0), Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun (p k : ℕ) ↦ p ^ ((k + n - 1) / n))
    (if n = 0 ∨ a = 0 then 0
    else
      (@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
            a.factorization n).prod
        fun (x1 x2 : ℕ) ↦ x1 ^ x2)
have neg : ∀ (h : ¬(n = 0 ∨ a = 0)),
  Eq (α := ℕ) (a.factorization.prod fun (p k : ℕ) ↦ p ^ ((k + n - 1) / n))
    ((@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
          a.factorization n).prod
      fun (x1 x2 : ℕ) ↦ x1 ^ x2)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a : ℕ
⊢ ceilRoot 1 a = a
have simp : (if a = 0 then 0 else a.factorization.prod fun (p k : ℕ) ↦ p ^ k) = a
Tactic: simp [ceilRoot]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.ceilRoot (a ^ n) = a
have simp : (if a = 0 then 0 else a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a
Tactic: simp [ceilRoot_def, pos_iff_ne_zero.2, hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n a : ℕ
⊢ (n.ceilRoot a).factorization =
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
have rw : factorization
    (if n = 0 ∨ a = 0 then 0
    else
      (@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
            a.factorization n).prod
        fun (x1 x2 : ℕ) ↦ x1 ^ x2) =
  @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
    a.factorization n
Tactic: rw [ceilRoot_def]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n a : ℕ
⊢ factorization
      (if n = 0 ∨ a = 0 then 0
      else
        (@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
              a.factorization n).prod
          fun (x1 x2 : ℕ) ↦ x1 ^ x2) =
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
have pos : ∀ (h : n = 0 ∨ a = 0),
  factorization 0 =
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n a : ℕ
pos :
  ∀ (h : n = 0 ∨ a = 0),
    factorization 0 =
      @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
        a.factorization n
⊢ factorization
      (if n = 0 ∨ a = 0 then 0
      else
        (@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
              a.factorization n).prod
          fun (x1 x2 : ℕ) ↦ x1 ^ x2) =
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
have neg : ∀ (h : ¬(n = 0 ∨ a = 0)),
  factorization
      ((@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
            a.factorization n).prod
        fun (x1 x2 : ℕ) ↦ x1 ^ x2) =
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 =
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
have pos : factorization 0 =
  @CeilDiv.ceilDiv ℕ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
    a.factorization 0
Tactic: obtain rfl | rfl := h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n a : ℕ
h : n = 0 ∨ a = 0
pos :
  factorization 0 =
    @CeilDiv.ceilDiv ℕ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization 0
⊢ factorization 0 =
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
have pos₁ : factorization 0 =
  @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
    (factorization 0) n
Tactic: obtain rfl | rfl := h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ factorization
      ((@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
            a.factorization n).prod
        fun (x1 x2 : ℕ) ↦ x1 ^ x2) =
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n
have neg : ∀ (p : ℕ)
  (hp :
    p ∈
      (@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
          a.factorization n).support),
  Prime p
Tactic: refine prod_pow_factorization_eq_self fun p hp ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (hypothesis)
Goal:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp :
  p ∈
    (@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
        a.factorization n).support
⊢ Prime p
have this : Prime p ∧ p ∣ a ∧ ¬a = 0
Tactic: have : p.Prime ∧ p ∣ a ∧ ¬a = 0 := by simpa using support_ceilDiv_subset hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
have inl : 0 ∣ b ^ n ↔ n.ceilRoot 0 ∣ b
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
inl : 0 ∣ b ^ n ↔ n.ceilRoot 0 ∣ b
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
have inr : ∀ (ha : a ≠ 0), a ∣ b ^ n ↔ n.ceilRoot a ∣ b
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
have inr : a ∣ HPow.hPow (α := ℕ) 0 n ↔ n.ceilRoot a ∣ 0
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
inr : a ∣ HPow.hPow (α := ℕ) 0 n ↔ n.ceilRoot a ∣ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
have inr₁ : ∀ (hb : b ≠ 0), a ∣ b ^ n ↔ n.ceilRoot a ∣ b
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
have inr : a.factorization ≤ (b ^ n).factorization ↔ n.ceilRoot a ∣ b
Tactic: rw [← factorization_le_iff_dvd ha (pow_ne_zero _ hb),
    ← factorization_le_iff_dvd (ceilRoot_ne_zero.2 ⟨hn, ha⟩) hb, factorization_pow,
    factorization_ceilRoot, ceilDiv_le_iff_le_smul (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
inr : a.factorization ≤ (b ^ n).factorization ↔ n.ceilRoot a ∣ b
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
have inr₁ : a.factorization ≤ (b ^ n).factorization ↔ (n.ceilRoot a).factorization ≤ b.factorization
Tactic: rw [← factorization_le_iff_dvd ha (pow_ne_zero _ hb),
    ← factorization_le_iff_dvd (ceilRoot_ne_zero.2 ⟨hn, ha⟩) hb, factorization_pow,
    factorization_ceilRoot, ceilDiv_le_iff_le_smul (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
Goal:
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
inr : a.factorization ≤ (b ^ n).factorization ↔ n.ceilRoot a ∣ b
inr₁ : a.factorization ≤ (b ^ n).factorization ↔ (n.ceilRoot a).factorization ≤ b.factorization
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
have inr₂ : a.factorization ≤ n • b.factorization ↔ (n.ceilRoot a).factorization ≤ b.factorization
Tactic: rw [← factorization_le_iff_dvd ha (pow_ne_zero _ hb),
    ← factorization_le_iff_dvd (ceilRoot_ne_zero.2 ⟨hn, ha⟩) hb, factorization_pow,
    factorization_ceilRoot, ceilDiv_le_iff_le_smul (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]