awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this_1 : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) (p - 1)
have rw : map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) = HPow.hPow (α := R[X]) (cyclotomic n R) (p - 1)
Tactic: rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
      this, Polynomial.map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this_1 : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)
rw :
  map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) =
    HPow.hPow (α := R[X]) (cyclotomic n R) (p - 1)
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) (p - 1)
have rw₁ : map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) =
  HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) (p - 1)
Tactic: rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
      this, Polynomial.map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this_1 : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)
rw :
  map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) =
    HPow.hPow (α := R[X]) (cyclotomic n R) (p - 1)
rw₁ :
  map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) =
    HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) (p - 1)
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) (p - 1)
have rw₂ : map (algebraMap (ZMod p) R) (HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)) =
  HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) (p - 1)
Tactic: rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
      this, Polynomial.map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this_1 : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)
rw :
  map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) =
    HPow.hPow (α := R[X]) (cyclotomic n R) (p - 1)
rw₁ :
  map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) =
    HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) (p - 1)
rw₂ :
  map (algebraMap (ZMod p) R) (HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)) =
    HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) (p - 1)
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) (p - 1)
have rw₃ : HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) (p - 1) =
  HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) (p - 1)
Tactic: rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
      this, Polynomial.map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) (p - 1)
have suffices : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)
Tactic: suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1) by
    rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
      this, Polynomial.map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)
have a : Eq (α := (ZMod p)[X]) ((fun (x : (ZMod p)[X]) ↦ cyclotomic n (ZMod p) * x) (cyclotomic (n * p) (ZMod p)))
  ((fun (x : (ZMod p)[X]) ↦ cyclotomic n (ZMod p) * x) (HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)))
Tactic: apply mul_right_injective₀ (cyclotomic_ne_zero n <| ZMod p)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ HMul.hMul (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (cyclotomic (n * p) (ZMod p)) =
    cyclotomic n (ZMod p) * HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)
have a : HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
  (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (cyclotomic n (ZMod p))
Tactic: rw [← pow_succ', tsub_add_cancel_of_le hp.out.one_lt.le, mul_comm, ← ZMod.expand_card]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
| ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (cyclotomic n (ZMod p)) : (ZMod p)[X])
have rw : ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ)) : (ZMod p)[X])
Tactic: rw [← map_cyclotomic_int]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (cyclotomic n (ZMod p))
have a : HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
  (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
Tactic: conv_rhs => rw [← map_cyclotomic_int]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
have a : HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
  map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
Tactic: rw [← map_expand, cyclotomic_expand_eq_cyclotomic_mul hp.out hn, Polynomial.map_mul,
    map_cyclotomic, map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
a :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
⊢ HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
have a₁ : HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
  map (Int.castRingHom (ZMod p)) (cyclotomic (n * p) ℤ * cyclotomic n ℤ)
Tactic: rw [← map_expand, cyclotomic_expand_eq_cyclotomic_mul hp.out hn, Polynomial.map_mul,
    map_cyclotomic, map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
a :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
a₁ :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    map (Int.castRingHom (ZMod p)) (cyclotomic (n * p) ℤ * cyclotomic n ℤ)
⊢ HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
have a₂ : HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
  HMul.hMul (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic (n * p) ℤ))
    (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
Tactic: rw [← map_expand, cyclotomic_expand_eq_cyclotomic_mul hp.out hn, Polynomial.map_mul,
    map_cyclotomic, map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
a :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
a₁ :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    map (Int.castRingHom (ZMod p)) (cyclotomic (n * p) ℤ * cyclotomic n ℤ)
a₂ :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    HMul.hMul (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic (n * p) ℤ))
      (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
⊢ HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
have a₃ : HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
Tactic: rw [← map_expand, cyclotomic_expand_eq_cyclotomic_mul hp.out hn, Polynomial.map_mul,
    map_cyclotomic, map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
a :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
a₁ :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    map (Int.castRingHom (ZMod p)) (cyclotomic (n * p) ℤ * cyclotomic n ℤ)
a₂ :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    HMul.hMul (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic (n * p) ℤ))
      (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
a₃ :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
⊢ HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
have a₄ : HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p))
Tactic: rw [← map_expand, cyclotomic_expand_eq_cyclotomic_mul hp.out hn, Polynomial.map_mul,
    map_cyclotomic, map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this_1 : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) p
have rw : map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) = HPow.hPow (α := R[X]) (cyclotomic n R) p
Tactic: rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
      this, Polynomial.map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this_1 : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p
rw : map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) = HPow.hPow (α := R[X]) (cyclotomic n R) p
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) p
have rw₁ : map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) =
  HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) p
Tactic: rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
      this, Polynomial.map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this_1 : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p
rw : map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) = HPow.hPow (α := R[X]) (cyclotomic n R) p
rw₁ :
  map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) =
    HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) p
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) p
have rw₂ : map (algebraMap (ZMod p) R) (HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p) =
  HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) p
Tactic: rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
      this, Polynomial.map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this_1 : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p
rw : map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) = HPow.hPow (α := R[X]) (cyclotomic n R) p
rw₁ :
  map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) =
    HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) p
rw₂ :
  map (algebraMap (ZMod p) R) (HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p) =
    HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) p
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) p
have rw₃ : HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) p =
  HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) p
Tactic: rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
      this, Polynomial.map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) p
have suffices : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p
Tactic: suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p by
    rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
      this, Polynomial.map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p
have rw : Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
  ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (cyclotomic n (ZMod p)))
Tactic: rw [← ZMod.expand_card, ← map_cyclotomic_int n, ← map_expand,
    cyclotomic_expand_eq_cyclotomic hp.out hn, map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
rw :
  Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
    ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (cyclotomic n (ZMod p)))
⊢ cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p
have rw₁ : Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
  ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ)))
Tactic: rw [← ZMod.expand_card, ← map_cyclotomic_int n, ← map_expand,
    cyclotomic_expand_eq_cyclotomic hp.out hn, map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
rw :
  Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
    ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (cyclotomic n (ZMod p)))
rw₁ :
  Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
    ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ)))
⊢ cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p
have rw₂ : Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
  (map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)))
Tactic: rw [← ZMod.expand_card, ← map_cyclotomic_int n, ← map_expand,
    cyclotomic_expand_eq_cyclotomic hp.out hn, map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
rw :
  Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
    ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (cyclotomic n (ZMod p)))
rw₁ :
  Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
    ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ)))
rw₂ :
  Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
    (map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)))
⊢ cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p
have rw₃ : Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (map (Int.castRingHom (ZMod p)) (cyclotomic (n * p) ℤ))
Tactic: rw [← ZMod.expand_card, ← map_cyclotomic_int n, ← map_expand,
    cyclotomic_expand_eq_cyclotomic hp.out hn, map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
rw :
  Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
    ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (cyclotomic n (ZMod p)))
rw₁ :
  Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
    ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ)))
rw₂ :
  Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
    (map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)))
rw₃ : Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (map (Int.castRingHom (ZMod p)) (cyclotomic (n * p) ℤ))
⊢ cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p
have rw₄ : Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic (n * p) (ZMod p))
Tactic: rw [← ZMod.expand_card, ← map_cyclotomic_int n, ← map_expand,
    cyclotomic_expand_eq_cyclotomic hp.out hn, map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p m : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Ring R
inst_2 : CharP R p
hm : ¬p ∣ m
h : LT.lt (α := ℕ) 0 1
⊢ cyclotomic (HPow.hPow (β := ℕ) p 1 * m) R =
    HPow.hPow (α := R[X]) (cyclotomic m R) (HPow.hPow (β := ℕ) p 1 - p ^ HSub.hSub (α := ℕ) 1 1)
have rw : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - p ^ HSub.hSub (α := ℕ) 1 1)
Tactic: rw [pow_one, Nat.sub_self, pow_zero, mul_comm, cyclotomic_mul_prime_eq_pow_of_not_dvd R hm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p m : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Ring R
inst_2 : CharP R p
hm : ¬p ∣ m
h : LT.lt (α := ℕ) 0 1
rw : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - p ^ HSub.hSub (α := ℕ) 1 1)
rw₁ : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - HPow.hPow (β := ℕ) p 0)
⊢ cyclotomic (HPow.hPow (β := ℕ) p 1 * m) R =
    HPow.hPow (α := R[X]) (cyclotomic m R) (HPow.hPow (β := ℕ) p 1 - p ^ HSub.hSub (α := ℕ) 1 1)
have rw₂ : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - 1)
Tactic: rw [pow_one, Nat.sub_self, pow_zero, mul_comm, cyclotomic_mul_prime_eq_pow_of_not_dvd R hm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p m : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Ring R
inst_2 : CharP R p
hm : ¬p ∣ m
h : LT.lt (α := ℕ) 0 1
rw : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - p ^ HSub.hSub (α := ℕ) 1 1)
rw₁ : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - HPow.hPow (β := ℕ) p 0)
rw₂ : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - 1)
⊢ cyclotomic (HPow.hPow (β := ℕ) p 1 * m) R =
    HPow.hPow (α := R[X]) (cyclotomic m R) (HPow.hPow (β := ℕ) p 1 - p ^ HSub.hSub (α := ℕ) 1 1)
have rw₃ : cyclotomic (m * p) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - 1)
Tactic: rw [pow_one, Nat.sub_self, pow_zero, mul_comm, cyclotomic_mul_prime_eq_pow_of_not_dvd R hm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p m : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Ring R
inst_2 : CharP R p
hm : ¬p ∣ m
h : LT.lt (α := ℕ) 0 1
rw : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - p ^ HSub.hSub (α := ℕ) 1 1)
rw₁ : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - HPow.hPow (β := ℕ) p 0)
rw₂ : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - 1)
rw₃ : cyclotomic (m * p) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - 1)
⊢ cyclotomic (HPow.hPow (β := ℕ) p 1 * m) R =
    HPow.hPow (α := R[X]) (cyclotomic m R) (HPow.hPow (β := ℕ) p 1 - p ^ HSub.hSub (α := ℕ) 1 1)
have rw₄ : HPow.hPow (α := R[X]) (cyclotomic m R) (p - 1) = HPow.hPow (α := R[X]) (cyclotomic m R) (p - 1)
Tactic: rw [pow_one, Nat.sub_self, pow_zero, mul_comm, cyclotomic_mul_prime_eq_pow_of_not_dvd R hm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
p m : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Ring R
inst_2 : CharP R p
hm : ¬p ∣ m
a : ℕ
h : 0 < a + 2
⊢ p ^ a.succ * m = p * (p ^ a * m)
have rw : p ^ a.succ * m = p * p ^ a * m
Tactic: rw [← mul_assoc, pow_succ']