awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : { n : ℕ // IsPrimePow n }
a :
  (↑n : ℕ).minFac ^
      (HSub.hSub (α := ℕ) (β := ℕ) (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) (1 : ℕ) + 1) =
    (↑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 : ℕ)

Tactic:
dsimp only
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : { n : ℕ // IsPrimePow n }
a : HPow.hPow (β := ℕ) (↑n : ℕ).minFac (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) = (↑n : ℕ)
a₁ a₂ : (↑n : ℕ) = (↑n : ℕ)
⊢ (↑n : ℕ).minFac ^
      (HSub.hSub (α := ℕ) (β := ℕ) (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) (1 : ℕ) + 1) =
    (↑n : ℕ)

Tactic:
rw [sub_one_add_one (Nat.factorization_minFac_ne_zero n.prop.one_lt),
      n.prop.minFac_pow_factorization_eq]

Premises used: IsPrimePow.minFac_pow_factorization_eq, Nat.factorization_minFac_ne_zero, Nat.sub_one_add_one, IsPrimePow.one_lt, Subtype.prop
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p : Primes
k : ℕ
⊢ Eq (α := { n : ℕ // IsPrimePow n })
    ((prodNatEquiv : (a : Primes × ℕ) → { n : ℕ // IsPrimePow n }) (p, k) : { n : ℕ // IsPrimePow n })
    (Subtype.mk (p := fun (n : ℕ) ↦ IsPrimePow n) ((↑p : ℕ) ^ (k + 1)) ⋯ : { n : ℕ // IsPrimePow n })

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p : Primes
k : ℕ
⊢ (↑((prodNatEquiv : (a : Primes × ℕ) → { n : ℕ // IsPrimePow n }) (p, k)) : ℕ) = (↑p : ℕ) ^ (k + 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
n : ℕ
hn : IsPrimePow n
⊢ (prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Primes × ℕ)
      (Subtype.mk (p := fun (n : ℕ) ↦ IsPrimePow n) n hn) =
    (Subtype.mk (p := fun (p : ℕ) ↦ Prime p) n.minFac ⋯,
      HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) (1 : ℕ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p a m n : ℕ
hp : Prime p
h : p ^ m = a ^ n
⊢ (p ^ m).factorization = (a ^ n).factorization

Tactic:
have := congrArg Nat.factorization h
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p a m n : ℕ
hp : Prime p
h : p ^ m = a ^ n
this : (p ^ m).factorization = (a ^ n).factorization
⊢ Finsupp.single p m = n • a.factorization

Tactic:
rw [Nat.Prime.factorization_pow hp, Nat.factorization_pow] at this

Premises used: Nat.Prime.factorization_pow, Nat.factorization_pow
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p a m n : ℕ
hp : Prime p
h : p ^ m = a ^ n
this : Finsupp.single p m = n • a.factorization
⊢ m = HMul.hMul (β := ℕ) n ((a.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simpa using congr($this p)
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p a m n : ℕ
hp : Prime p
h : p ^ m = a ^ n
⊢ n ∣ m

Tactic:
Dvd.intro (a.factorization p)
    (exponent_eq_exponent_mul_factorization_of_prime_pow_eq_base_pow hp h).symm

Premises used: Dvd.intro, Nat.exponent_eq_exponent_mul_factorization_of_prime_pow_eq_base_pow, Eq.symm, DFunLike.coe, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p a m n : ℕ
hp : Prime p
hn : n ≠ 0
h : p ^ m = a ^ n
rcases : ∀ (k : ℕ) (m_eq : m = n * k), ∃ (k : ℕ), a = p ^ k
⊢ ∃ (k : ℕ), a = p ^ k

Tactic:
rcases exponent_dvd_of_prime_pow_eq_pow hp h with ⟨k, m_eq⟩

Premises used: Nat.exponent_dvd_of_prime_pow_eq_pow
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p a m n : ℕ
hp : Prime p
hn : n ≠ 0
h : p ^ m = a ^ n
k : ℕ
m_eq : m = n * k
⊢ (p ^ k) ^ n = a ^ n

Tactic:
rw [m_eq, pow_mul'] at h

Premises used: pow_mul'
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p a m n : ℕ
hp : Prime p
hn : n ≠ 0
h : p ^ m = a ^ n
k : ℕ
m_eq : m = n * k
h₁ : (p ^ k) ^ n = a ^ n
⊢ m = n * k

Tactic:
rw [m_eq, pow_mul'] at h

Premises used: pow_mul'
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p a m n : ℕ
hp : Prime p
hn : n ≠ 0
k : ℕ
h : (p ^ k) ^ n = a ^ n
m_eq : m = n * k
h₁ : a = p ^ k
⊢ ∃ (k : ℕ), a = p ^ k

Tactic:
use k
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p a m n : ℕ
hp : Prime p
hn : n ≠ 0
k : ℕ
h : (p ^ k) ^ n = a ^ n
m_eq : m = n * k
⊢ a = p ^ k

Tactic:
Nat.pow_left_injective hn h.symm

Premises used: Nat.pow_left_injective, Eq.symm
-- Module: Mathlib.Data.Nat.Factorization.PrimePow
Goal:
p a m n : ℕ
hp : Prime p
hn : n ≠ 0
k : ℕ
h : (p ^ k) ^ n = a ^ n
m_eq : m = n * k
⊢ a = p ^ k

Tactic:
exact Nat.pow_left_injective hn h.symm

Premises used: Nat.pow_left_injective, Eq.symm
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
pos : ∀ (h : n = 0 ∨ a = 0), Eq (α := ℕ) 0 0
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)
⊢ 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)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
h : n = 0 ∨ a = 0
⊢ Eq (α := ℕ) 0 0

Tactic:
simp [Finsupp.floorDiv_def, prod_mapRange_index pow_zero]

Premises used: Finsupp.floorDiv_def, pow_zero, Finsupp.prod_mapRange_index
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
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:
simp [Finsupp.floorDiv_def, prod_mapRange_index pow_zero]

Premises used: Finsupp.floorDiv_def, pow_zero, Finsupp.prod_mapRange_index
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a : ℕ
⊢ floorRoot 0 a = 0

Tactic:
simp [floorRoot]

Premises used: Nat.floorRoot
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n : ℕ
⊢ n.floorRoot 0 = 0

Tactic:
simp [floorRoot]

Premises used: Nat.floorRoot
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a : ℕ
simp : (if a = 0 then 0 else a.factorization.prod fun (p k : ℕ) ↦ p ^ k) = a
⊢ floorRoot 1 a = a

Tactic:
simp [floorRoot]

Premises used: Nat.floorRoot
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a : ℕ
pos : a = 0 → 0 = a
neg : ¬a = 0 → (a.factorization.prod fun (p k : ℕ) ↦ p ^ k) = a
⊢ (if a = 0 then 0 else a.factorization.prod fun (p k : ℕ) ↦ p ^ k) = a

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a : ℕ
h : a = 0
⊢ 0 = a

Tactic:
simp [*]
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a : ℕ
h : ¬a = 0
⊢ (a.factorization.prod fun (p k : ℕ) ↦ p ^ k) = a

Tactic:
simp [*]
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n : ℕ
hn : n ≠ 0
⊢ n.floorRoot 1 = 1

Tactic:
simp [floorRoot, hn]

Premises used: Nat.floorRoot
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
simp : (if a = 0 then 0 else a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a
⊢ n.floorRoot (a ^ n) = a

Tactic:
simp [floorRoot_def, pos_iff_ne_zero.2, hn]

Premises used: Iff.mpr, Nat.floorRoot_def, pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
pos : a = 0 → 0 = a
neg : ¬a = 0 → (a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a
⊢ (if a = 0 then 0 else a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
h : a = 0
⊢ 0 = a

Tactic:
simp [*]
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
h : ¬a = 0
⊢ (a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a

Tactic:
simp [*]
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
⊢ n.floorRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0

Tactic:
simp +contextual [floorRoot, not_or]

Premises used: not_or, Nat.floorRoot
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
⊢ ¬(n ≠ 0 ∧ a ≠ 0) ↔ n = 0 ∨ a = 0

Tactic:
simp only [not_and_or, ne_eq, not_not]

Premises used: Classical.not_not, ne_eq, not_and_or
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
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
⊢ (n.floorRoot a).factorization =
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n

Tactic:
rw [floorRoot_def]

Premises used: Nat.floorRoot_def
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
pos :
  ∀ (h : n = 0 ∨ a = 0),
    factorization 0 =
      @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
        a.factorization n
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
⊢ 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:
split_ifs with h
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
h : n = 0 ∨ a = 0
pos :
  factorization 0 =
    @FloorDiv.floorDiv ℕ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization 0
pos₁ :
  factorization 0 =
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      (factorization 0) n
⊢ factorization 0 =
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n

Tactic:
obtain rfl | rfl := h

Premises used: rfl
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a : ℕ
⊢ factorization 0 =
    @FloorDiv.floorDiv ℕ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n : ℕ
⊢ factorization 0 =
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      (factorization 0) n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
neg :
  @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n ≤
    a.factorization
⊢ 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:
apply a.factorization_prod_pow_eq_self_of_le_factorization

Premises used: Nat.factorization_prod_pow_eq_self_of_le_factorization
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ 0 ≤
    @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ n ≠ 0

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ 0 < n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ @FloorDiv.floorDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n ≤
    a.factorization

Tactic:
exact le_self_nsmul (by simp) (by lia) |>.trans <| smul_floorDiv_le (by lia)

Premises used: le_self_nsmul, smul_floorDiv_le, LE.le.trans
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a b n : ℕ
inl : HPow.hPow (β := ℕ) a 0 ∣ b ↔ a ∣ floorRoot 0 b
inr : ∀ (hn : n ≠ 0), a ^ n ∣ b ↔ a ∣ n.floorRoot b
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a b : ℕ
⊢ HPow.hPow (β := ℕ) a 0 ∣ b ↔ a ∣ floorRoot 0 b

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a b n : ℕ
hn : n ≠ 0
inr : a ^ n ∣ 0 ↔ a ∣ n.floorRoot 0
inr₁ : ∀ (hb : b ≠ 0), a ^ n ∣ b ↔ a ∣ n.floorRoot b
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ 0 ↔ a ∣ n.floorRoot 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
inr : HPow.hPow (α := ℕ) 0 n ∣ b ↔ 0 ∣ n.floorRoot b
inr₁ : ∀ (ha : a ≠ 0), a ^ n ∣ b ↔ a ∣ n.floorRoot b
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
⊢ HPow.hPow (α := ℕ) 0 n ∣ b ↔ 0 ∣ n.floorRoot b

Tactic:
simp [hn]
-- Module: Mathlib.Data.Nat.Factorization.Root
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
inr₄ inr₅ : n • a.factorization ≤ b.factorization ↔ n • a.factorization ≤ b.factorization
⊢ a ^ n ∣ b ↔ 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)]

Premises used: Iff.mpr, pow_ne_zero, Nat.floorRoot_ne_zero, Nat.factorization_le_iff_dvd, Nat.factorization_floorRoot, And.intro, Nat.factorization_pow, le_floorDiv_iff_smul_le, pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
⊢ n.floorRoot a ^ n ∣ a

Tactic:
pow_dvd_iff_dvd_floorRoot.2 dvd_rfl

Premises used: Iff.mpr, Nat.pow_dvd_iff_dvd_floorRoot, dvd_rfl
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
pos : ∀ (h : n = 0 ∨ a = 0), Eq (α := ℕ) 0 0
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)
⊢ 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)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
h : n = 0 ∨ a = 0
⊢ Eq (α := ℕ) 0 0

Tactic:
simp [Finsupp.ceilDiv_def, prod_mapRange_index pow_zero, Nat.ceilDiv_eq_add_pred_div]

Premises used: Finsupp.ceilDiv_def, pow_zero, Finsupp.prod_mapRange_index, Nat.ceilDiv_eq_add_pred_div
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
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:
simp [Finsupp.ceilDiv_def, prod_mapRange_index pow_zero, Nat.ceilDiv_eq_add_pred_div]

Premises used: Finsupp.ceilDiv_def, pow_zero, Finsupp.prod_mapRange_index, Nat.ceilDiv_eq_add_pred_div
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a : ℕ
⊢ ceilRoot 0 a = 0

Tactic:
simp [ceilRoot]

Premises used: Nat.ceilRoot
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n : ℕ
⊢ n.ceilRoot 0 = 0

Tactic:
simp [ceilRoot]

Premises used: Nat.ceilRoot
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a : ℕ
simp : (if a = 0 then 0 else a.factorization.prod fun (p k : ℕ) ↦ p ^ k) = a
⊢ ceilRoot 1 a = a

Tactic:
simp [ceilRoot]

Premises used: Nat.ceilRoot
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n : ℕ
hn : n ≠ 0
⊢ n.ceilRoot 1 = 1

Tactic:
simp [ceilRoot, hn]

Premises used: Nat.ceilRoot
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
simp : (if a = 0 then 0 else a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = a
⊢ n.ceilRoot (a ^ n) = a

Tactic:
simp [ceilRoot_def, pos_iff_ne_zero.2, hn]

Premises used: Iff.mpr, Nat.ceilRoot_def, pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
⊢ n.ceilRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0

Tactic:
simp +contextual [ceilRoot_def, not_or]

Premises used: Nat.ceilRoot_def, not_or
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
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
⊢ (n.ceilRoot a).factorization =
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n

Tactic:
rw [ceilRoot_def]

Premises used: Nat.ceilRoot_def
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
pos :
  ∀ (h : n = 0 ∨ a = 0),
    factorization 0 =
      @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
        a.factorization n
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
⊢ 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:
split_ifs with h
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
h : n = 0 ∨ a = 0
pos :
  factorization 0 =
    @CeilDiv.ceilDiv ℕ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization 0
pos₁ :
  factorization 0 =
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      (factorization 0) n
⊢ factorization 0 =
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n

Tactic:
obtain rfl | rfl := h

Premises used: rfl
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a : ℕ
⊢ factorization 0 =
    @CeilDiv.ceilDiv ℕ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n : ℕ
⊢ factorization 0 =
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      (factorization 0) n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Root
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

Tactic:
prod_pow_factorization_eq_self fun p hp ↦ ?_

Premises used: Nat.prod_pow_factorization_eq_self
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
neg :
  ∀ (p : ℕ)
    (hp :
      p ∈
        (@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
            a.factorization n).support),
    Prime p
⊢ 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:
refine prod_pow_factorization_eq_self fun p hp ↦ ?_

Premises used: Nat.prod_pow_factorization_eq_self
-- Module: Mathlib.Data.Nat.Factorization.Root
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 ∧ p ∣ a ∧ ¬a = 0

Tactic:
simpa using support_ceilDiv_subset hp

Premises used: Finsupp.support_ceilDiv_subset
-- Module: Mathlib.Data.Nat.Factorization.Root
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 ∧ p ∣ a ∧ ¬a = 0

Tactic:
have : p.Prime ∧ p ∣ a ∧ ¬a = 0 := by simpa using support_ceilDiv_subset hp
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp :
  p ∈
    (@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
        a.factorization n).support
this : Prime p ∧ p ∣ a ∧ ¬a = 0
⊢ Prime p

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp :
  p ∈
    (@CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
        a.factorization n).support
this : Prime p ∧ p ∣ a ∧ ¬a = 0
⊢ Prime p

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a b n : ℕ
hn : n ≠ 0
inl : 0 ∣ b ^ n ↔ n.ceilRoot 0 ∣ b
inr : ∀ (ha : a ≠ 0), a ∣ b ^ n ↔ n.ceilRoot a ∣ b
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
b n : ℕ
hn : n ≠ 0
⊢ 0 ∣ b ^ n ↔ n.ceilRoot 0 ∣ b

Tactic:
aesop