awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
m_1 m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + (↑p : R) * u * (x + v * y)
⊢ HMul.hMul (α := R) (↑p : R) (↑p : R) ∣ HPow.hPow (α := R) (↑p : R) p
have rw : HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ HPow.hPow (α := R) (↑p : R) p
Tactic: rw [← pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
m_1 m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + (↑p : R) * u * (x + v * y)
⊢ ∃ (y_1 : R), (1 + (↑p : R) * u * (x + v * y)) ^ p ^ m = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * y_1)
have obtain : ∀ (z : R)
  (hz :
    (1 + (↑p : R) * u * (x + v * y)) ^ p ^ m =
      1 + HPow.hPow (α := R) (↑p : R) m * ((↑p : R) * u) * (x + v * y + (↑p : R) * v * z)),
  ∃ (y_1 : R), (1 + (↑p : R) * u * (x + v * y)) ^ p ^ m = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * y_1)
Tactic: obtain ⟨z, hz⟩ :=
      exists_one_add_mul_pow_prime_pow_eq (u := p * u) (v := p * v) hp
      (mul_dvd_mul_left _ hvu)
      (by
        rw [mul_pow]
        simp only [← mul_assoc]
        rw [mul_assoc, mul_assoc, ← mul_assoc u, mul_comm u]
        apply mul_dvd_mul _ hpuv
        rw [← pow_two]
        exact pow_dvd_pow _ hp.two_le)
      (x + v * y) m
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
m_1 m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + (↑p : R) * u * (x + v * y)
z : R
hz :
  (1 + (↑p : R) * u * (x + v * y)) ^ p ^ m =
    1 + HPow.hPow (α := R) (↑p : R) m * ((↑p : R) * u) * (x + v * y + (↑p : R) * v * z)
⊢ ∃ (y_1 : R), (1 + (↑p : R) * u * (x + v * y)) ^ p ^ m = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * y_1)
have h : (1 + (↑p : R) * u * (x + v * y)) ^ p ^ m = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * (y + (↑p : R) * z))
Tactic: use y + p * z
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
m_1 m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + (↑p : R) * u * (x + v * y)
z : R
hz :
  (1 + (↑p : R) * u * (x + v * y)) ^ p ^ m =
    1 + HPow.hPow (α := R) (↑p : R) m * ((↑p : R) * u) * (x + v * y + (↑p : R) * v * z)
⊢ (1 + (↑p : R) * u * (x + v * y)) ^ p ^ m = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * (y + (↑p : R) * z))
have h : 1 + HPow.hPow (α := R) (↑p : R) m * ((↑p : R) * u) * (x + v * y + (↑p : R) * v * z) =
  1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * (y + (↑p : R) * z))
Tactic: rw [hz]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n : ℕ
⊢ orderOf (1 + HPow.hPow (α := ZMod (p ^ (0 + m))) (↑p : ZMod (p ^ (0 + m))) m * (↑a : ZMod (p ^ (0 + m)))) =
    HPow.hPow (β := ℕ) p 0
have rw : orderOf (1 + HMul.hMul (α := ZMod (p ^ m)) 0 (↑a : ZMod (p ^ m))) = HPow.hPow (β := ℕ) p 0
Tactic: rw [← Nat.cast_pow, zero_add m, ZMod.natCast_self]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
⊢ orderOf
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) =
    p ^ (n + 1)
have this : Fact (Nat.Prime p)
Tactic: have := Fact.mk hp
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this : Fact (Nat.Prime p)
⊢ orderOf
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) =
    p ^ (n + 1)
have refine_2 : ∀
  (this :
    ∀ (m_1 : ℕ),
      ∃ (y : ZMod (p ^ (n + 1 + m))),
        (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
            p ^ m_1 =
          1 +
            HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
                HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
              ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)),
  orderOf
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) =
    p ^ (n + 1)
Tactic: have := exists_one_add_mul_pow_prime_pow_eq
      (R := ZMod (p ^ (n + 1 + m))) (u := p ^ m) (v := p) hp (dvd_pow_self _ hm0) ?_ a
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this : Fact (Nat.Prime p)
refine_2 :
  ∀
    (this :
      ∀ (m_1 : ℕ),
        ∃ (y : ZMod (p ^ (n + 1 + m))),
          (1 +
                HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
                  (↑a : ZMod (p ^ (n + 1 + m)))) ^
              p ^ m_1 =
            1 +
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
                  HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
                ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)),
    orderOf
        (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) =
      p ^ (n + 1)
⊢ orderOf
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) =
    p ^ (n + 1)
have refine_1 : (↑p : ZMod (p ^ (n + 1 + m))) * HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
    (↑p : ZMod (p ^ (n + 1 + m))) ∣
  HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m ^ p
Tactic: have := exists_one_add_mul_pow_prime_pow_eq
      (R := ZMod (p ^ (n + 1 + m))) (u := p ^ m) (v := p) hp (dvd_pow_self _ hm0) ?_ a
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
⊢ orderOf
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) =
    p ^ (n + 1)
have refine_2 : ¬(1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^ p ^ n =
    1
Tactic: apply orderOf_eq_prime_pow
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
refine_2 :
  ¬(1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
        p ^ n =
      1
⊢ orderOf
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) =
    p ^ (n + 1)
have refine_2₁ : (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
    p ^ (n + 1) =
  1
Tactic: apply orderOf_eq_prime_pow
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
⊢ ¬(1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
        p ^ n =
      1
have refine_2 : ∀ (y : ZMod (p ^ (n + 1 + m)))
  (hy :
    (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
        p ^ n =
      1 +
        HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) n *
            HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
          ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)),
  ¬(1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
        p ^ n =
      1
Tactic: obtain ⟨y, hy⟩ := this n
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
y : ZMod (p ^ (n + 1 + m))
hy :
  (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ n =
    1 +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) n *
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
⊢ ¬(1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
        p ^ n =
      1
have refine_2 : ¬HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (n + m) * (↑a : ZMod (p ^ (n + 1 + m))) +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (n + m + 1) * y =
    0
Tactic: rw [hy, ← pow_add, add_eq_left, mul_add, ← mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
y : ZMod (p ^ (n + 1 + m))
hy :
  (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ n =
    1 +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) n *
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
⊢ ¬HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (n + m) * (↑a : ZMod (p ^ (n + 1 + m))) +
        HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) (n + m + 1) * y =
      0
have refine_2 : ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(p ^ (n + m)) : ZMod (p ^ (n + 1 + m))) (↑a : ZMod (p ^ (n + 1 + m))) = 0
Tactic: simp_rw [add_right_comm n _ 1, ← Nat.cast_pow, ZMod.natCast_self, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
y : ZMod (p ^ (n + 1 + m))
hy :
  (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ n =
    1 +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) n *
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
⊢ ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(p ^ (n + m)) : ZMod (p ^ (n + 1 + m))) (↑a : ZMod (p ^ (n + 1 + m))) = 0
have refine_2 : ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(↑(p ^ (n + m)) : ℤ) : ZMod (p ^ (n + 1 + m)))
      (↑a : ZMod (p ^ (n + 1 + m))) =
    0
Tactic: rwa [← Int.cast_natCast, ← Int.cast_mul, ZMod.intCast_zmod_eq_zero_iff_dvd, add_right_comm,
          pow_succ, Nat.cast_mul, Int.mul_dvd_mul_iff_left (by simp [hp.ne_zero])]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
y : ZMod (p ^ (n + 1 + m))
hy :
  (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ n =
    1 +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) n *
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
refine_2 :
  ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(↑(p ^ (n + m)) : ℤ) : ZMod (p ^ (n + 1 + m)))
        (↑a : ZMod (p ^ (n + 1 + m))) =
      0
⊢ ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(p ^ (n + m)) : ZMod (p ^ (n + 1 + m))) (↑a : ZMod (p ^ (n + 1 + m))) = 0
have refine_2₁ : ¬Eq (α := ZMod (p ^ (n + 1 + m))) (↑((↑(p ^ (n + m)) : ℤ) * a) : ZMod (p ^ (n + 1 + m))) 0
Tactic: rwa [← Int.cast_natCast, ← Int.cast_mul, ZMod.intCast_zmod_eq_zero_iff_dvd, add_right_comm,
          pow_succ, Nat.cast_mul, Int.mul_dvd_mul_iff_left (by simp [hp.ne_zero])]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
y : ZMod (p ^ (n + 1 + m))
hy :
  (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ n =
    1 +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) n *
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
refine_2 :
  ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(↑(p ^ (n + m)) : ℤ) : ZMod (p ^ (n + 1 + m)))
        (↑a : ZMod (p ^ (n + 1 + m))) =
      0
refine_2₁ : ¬Eq (α := ZMod (p ^ (n + 1 + m))) (↑((↑(p ^ (n + m)) : ℤ) * a) : ZMod (p ^ (n + 1 + m))) 0
⊢ ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(p ^ (n + m)) : ZMod (p ^ (n + 1 + m))) (↑a : ZMod (p ^ (n + 1 + m))) = 0
have refine_2₂ : ¬(↑(p ^ (n + 1 + m)) : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
Tactic: rwa [← Int.cast_natCast, ← Int.cast_mul, ZMod.intCast_zmod_eq_zero_iff_dvd, add_right_comm,
          pow_succ, Nat.cast_mul, Int.mul_dvd_mul_iff_left (by simp [hp.ne_zero])]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
y : ZMod (p ^ (n + 1 + m))
hy :
  (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ n =
    1 +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) n *
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
refine_2 :
  ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(↑(p ^ (n + m)) : ℤ) : ZMod (p ^ (n + 1 + m)))
        (↑a : ZMod (p ^ (n + 1 + m))) =
      0
refine_2₁ : ¬Eq (α := ZMod (p ^ (n + 1 + m))) (↑((↑(p ^ (n + m)) : ℤ) * a) : ZMod (p ^ (n + 1 + m))) 0
refine_2₂ : ¬(↑(p ^ (n + 1 + m)) : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
⊢ ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(p ^ (n + m)) : ZMod (p ^ (n + 1 + m))) (↑a : ZMod (p ^ (n + 1 + m))) = 0
have refine_2₃ : ¬(↑(p ^ (n + m + 1)) : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
Tactic: rwa [← Int.cast_natCast, ← Int.cast_mul, ZMod.intCast_zmod_eq_zero_iff_dvd, add_right_comm,
          pow_succ, Nat.cast_mul, Int.mul_dvd_mul_iff_left (by simp [hp.ne_zero])]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
y : ZMod (p ^ (n + 1 + m))
hy :
  (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ n =
    1 +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) n *
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
refine_2 :
  ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(↑(p ^ (n + m)) : ℤ) : ZMod (p ^ (n + 1 + m)))
        (↑a : ZMod (p ^ (n + 1 + m))) =
      0
refine_2₁ : ¬Eq (α := ZMod (p ^ (n + 1 + m))) (↑((↑(p ^ (n + m)) : ℤ) * a) : ZMod (p ^ (n + 1 + m))) 0
refine_2₂ : ¬(↑(p ^ (n + 1 + m)) : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
refine_2₃ : ¬(↑(p ^ (n + m + 1)) : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
⊢ ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(p ^ (n + m)) : ZMod (p ^ (n + 1 + m))) (↑a : ZMod (p ^ (n + 1 + m))) = 0
have refine_2₄ : ¬(↑(p ^ (n + m) * p) : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
Tactic: rwa [← Int.cast_natCast, ← Int.cast_mul, ZMod.intCast_zmod_eq_zero_iff_dvd, add_right_comm,
          pow_succ, Nat.cast_mul, Int.mul_dvd_mul_iff_left (by simp [hp.ne_zero])]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
this_1 : Fact (Nat.Prime p)
this :
  ∀ (m_1 : ℕ),
    ∃ (y : ZMod (p ^ (n + 1 + m))),
      (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
          p ^ m_1 =
        1 +
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m_1 *
              HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
            ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
y : ZMod (p ^ (n + 1 + m))
hy :
  (1 + HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m * (↑a : ZMod (p ^ (n + 1 + m)))) ^
      p ^ n =
    1 +
      HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) n *
          HPow.hPow (α := ZMod (p ^ (n + 1 + m))) (↑p : ZMod (p ^ (n + 1 + m))) m *
        ((↑a : ZMod (p ^ (n + 1 + m))) + (↑p : ZMod (p ^ (n + 1 + m))) * y)
refine_2 :
  ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(↑(p ^ (n + m)) : ℤ) : ZMod (p ^ (n + 1 + m)))
        (↑a : ZMod (p ^ (n + 1 + m))) =
      0
refine_2₁ : ¬Eq (α := ZMod (p ^ (n + 1 + m))) (↑((↑(p ^ (n + m)) : ℤ) * a) : ZMod (p ^ (n + 1 + m))) 0
refine_2₂ : ¬(↑(p ^ (n + 1 + m)) : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
refine_2₃ : ¬(↑(p ^ (n + m + 1)) : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
refine_2₄ : ¬(↑(p ^ (n + m) * p) : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
⊢ ¬HMul.hMul (α := ZMod (p ^ (n + 1 + m))) (↑(p ^ (n + m)) : ZMod (p ^ (n + 1 + m))) (↑a : ZMod (p ^ (n + 1 + m))) = 0
have refine_2₅ : ¬HMul.hMul (α := ℤ) (↑(p ^ (n + m)) : ℤ) (↑p : ℤ) ∣ (↑(p ^ (n + m)) : ℤ) * a
Tactic: rwa [← Int.cast_natCast, ← Int.cast_mul, ZMod.intCast_zmod_eq_zero_iff_dvd, add_right_comm,
          pow_succ, Nat.cast_mul, Int.mul_dvd_mul_iff_left (by simp [hp.ne_zero])]