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
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
⊢ ∃ (y : R),
    1 +
        (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
          (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
            (u * x) ^ p * (↑(p.choose p) : R))) =
      1 + (↑p : R) * u * (x + v * y)
have h : 1 +
    (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
      (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
        (u * x) ^ p * (↑(p.choose p) : R))) =
  1 +
    (↑p : R) * u *
      (x +
        v *
          (a * HPow.hPow (β := ℕ) x 2 *
              ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * (↑(p.choose i / p) : R) +
            b * x ^ p))
Tactic: use a * x ^ 2 * ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p,
    (u * x) ^ (i - 2) * (p.choose i / p : ℕ) + b * x ^ p
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
⊢ 1 +
      (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
        (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
          (u * x) ^ p * (↑(p.choose p) : R))) =
    1 +
      (↑p : R) * u *
        (x +
          v *
            (a * HPow.hPow (β := ℕ) x 2 *
                ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * (↑(p.choose i / p) : R) +
              b * x ^ p))
have h : 1 +
    (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
      (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
        (u * x) ^ p * (↑(p.choose p) : R))) =
  1 +
    ((↑p : R) * u * x +
      (↑p : R) * u *
        (v *
          (a * HPow.hPow (β := ℕ) x 2 *
              ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * (↑(p.choose i / p) : R) +
            b * x ^ p)))
Tactic: rw [mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
⊢ 1 +
      (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
        (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
          (u * x) ^ p * (↑(p.choose p) : R))) =
    1 +
      ((↑p : R) * u * x +
        (↑p : R) * u *
          (v *
            (a * HPow.hPow (β := ℕ) x 2 *
                ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * (↑(p.choose i / p) : R) +
              b * x ^ p)))
have h : HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) = (↑p : R) * u * x
Tactic: congr 2
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
h : HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) = (↑p : R) * u * x
⊢ 1 +
      (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
        (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
          (u * x) ^ p * (↑(p.choose p) : R))) =
    1 +
      ((↑p : R) * u * x +
        (↑p : R) * u *
          (v *
            (a * HPow.hPow (β := ℕ) x 2 *
                ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * (↑(p.choose i / p) : R) +
              b * x ^ p)))
have h₁ : ∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
    (u * x) ^ p * (↑(p.choose p) : R) =
  (↑p : R) * u *
    (v *
      (a * HPow.hPow (β := ℕ) x 2 *
          ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * (↑(p.choose i / p) : R) +
        b * x ^ p))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
⊢ HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) = (↑p : R) * u * x
have h : HPow.hPow (β := ℕ) (u * x) 1 * (↑p : R) = (↑p : R) * u * x
Tactic: rw [Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
⊢ ∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
      (u * x) ^ p * (↑(p.choose p) : R) =
    (↑p : R) * u *
      (v *
        (a * HPow.hPow (β := ℕ) x 2 *
            ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * (↑(p.choose i / p) : R) +
          b * x ^ p))
have h : ∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
    (u * x) ^ p * (↑(p.choose p) : R) =
  ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p,
      (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R)))) +
    (↑p : R) * u * (v * (b * x ^ p))
Tactic: simp only [mul_add, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
⊢ ∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
      (u * x) ^ p * (↑(p.choose p) : R) =
    ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p,
        (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R)))) +
      (↑p : R) * u * (v * (b * x ^ p))
have h : Eq.{u_1 + 1} (α := R)
  (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R))
  (∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p,
    (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R)))))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
h :
  Eq.{u_1 + 1} (α := R)
    (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R))
    (∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p,
      (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R)))))
⊢ ∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
      (u * x) ^ p * (↑(p.choose p) : R) =
    ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p,
        (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R)))) +
      (↑p : R) * u * (v * (b * x ^ p))
have h₁ : (u * x) ^ p * (↑(p.choose p) : R) = (↑p : R) * u * (v * (b * x ^ p))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R))
    (∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p,
      (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R)))))
have h : ∀ (i : ℕ) (hi : i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p),
  (u * x) ^ i * (↑(p.choose i) : R) =
    (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R))))
Tactic: congr! 1 with i hi
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
i : ℕ
hi : i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p
⊢ (u * x) ^ i * (↑(p.choose i) : R) =
    (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R))))
have hi₁ : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
Tactic: simp only [Finset.mem_erase, ne_eq, Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
⊢ (u * x) ^ i * (↑(p.choose i) : R) =
    (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R))))
have hi' : 2 ≤ i
Tactic: have hi' : 2 ≤ i := by lia
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ (u * x) ^ i * (↑(p.choose i) : R) = (u * x) ^ (2 + (i - 2)) * (↑(p.choose i) : R)
have rw : (u * x) ^ i * (↑(p.choose i) : R) = (u * x) ^ i * (↑(p.choose i) : R)
Tactic: rw [Nat.add_sub_of_le hi']
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p.choose i) : R) =
    HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p * (p.choose i / p)) : R)
have rw : HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p.choose i) : R) =
  HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p.choose i) : R)
Tactic: rw [Nat.mul_div_cancel' (hp.dvd_choose_self hi.2.2.1 <| by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p * (p.choose i / p)) : R) =
    HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑p : R) * (↑(p.choose i / p) : R)
have simp : HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) *
    HMul.hMul (α := R) (↑p : R) (↑(p.choose i / p) : R) =
  HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑p : R) * (↑(p.choose i / p) : R)
Tactic: simp only [Nat.cast_mul]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑p : R) * (↑(p.choose i / p) : R) =
    (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R))))
have rw : HPow.hPow (β := ℕ) (v * a) 2 * HPow.hPow (β := ℕ) x 2 * (v * a * x) ^ (i - 2) * (↑p : R) * (↑(p.choose i / p) : R) =
  (↑p : R) * (v * a) * (v * (a * HPow.hPow (β := ℕ) x 2 * ((v * a * x) ^ (i - 2) * (↑(p.choose i / p) : R))))
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ (u * x) ^ i * (↑(p.choose i) : R) =
    (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R))))
have i₁ : (u * x) ^ i * (↑(p.choose i) : R) = (u * x) ^ (2 + (i - 2)) * (↑(p.choose i) : R)
Tactic: calc
      (u * x) ^ i * p.choose i =
        (u * x) ^ (2 + (i - 2)) * p.choose i := by rw [Nat.add_sub_of_le hi']
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p.choose i := by ring_nf
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * (p * (p.choose i / p) : ℕ) := by
        rw [Nat.mul_div_cancel' (hp.dvd_choose_self hi.2.2.1 <| by lia)]
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p * (p.choose i / p : ℕ) := by
        simp only [Nat.cast_mul]; ring_nf
      _ = p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * (p.choose i / p : ℕ)))) := by
        rw [ha]; ring
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
i₁ : (u * x) ^ i * (↑(p.choose i) : R) = (u * x) ^ (2 + (i - 2)) * (↑(p.choose i) : R)
⊢ (u * x) ^ i * (↑(p.choose i) : R) =
    (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R))))
have i₂ : (u * x) ^ (2 + (i - 2)) * (↑(p.choose i) : R) =
  HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p.choose i) : R)
Tactic: calc
      (u * x) ^ i * p.choose i =
        (u * x) ^ (2 + (i - 2)) * p.choose i := by rw [Nat.add_sub_of_le hi']
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p.choose i := by ring_nf
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * (p * (p.choose i / p) : ℕ) := by
        rw [Nat.mul_div_cancel' (hp.dvd_choose_self hi.2.2.1 <| by lia)]
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p * (p.choose i / p : ℕ) := by
        simp only [Nat.cast_mul]; ring_nf
      _ = p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * (p.choose i / p : ℕ)))) := by
        rw [ha]; ring
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
i₁ : (u * x) ^ i * (↑(p.choose i) : R) = (u * x) ^ (2 + (i - 2)) * (↑(p.choose i) : R)
i₂ :
  (u * x) ^ (2 + (i - 2)) * (↑(p.choose i) : R) =
    HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p.choose i) : R)
⊢ (u * x) ^ i * (↑(p.choose i) : R) =
    (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R))))
have i₃ : HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p.choose i) : R) =
  HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p * (p.choose i / p)) : R)
Tactic: calc
      (u * x) ^ i * p.choose i =
        (u * x) ^ (2 + (i - 2)) * p.choose i := by rw [Nat.add_sub_of_le hi']
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p.choose i := by ring_nf
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * (p * (p.choose i / p) : ℕ) := by
        rw [Nat.mul_div_cancel' (hp.dvd_choose_self hi.2.2.1 <| by lia)]
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p * (p.choose i / p : ℕ) := by
        simp only [Nat.cast_mul]; ring_nf
      _ = p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * (p.choose i / p : ℕ)))) := by
        rw [ha]; ring
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
i₁ : (u * x) ^ i * (↑(p.choose i) : R) = (u * x) ^ (2 + (i - 2)) * (↑(p.choose i) : R)
i₂ :
  (u * x) ^ (2 + (i - 2)) * (↑(p.choose i) : R) =
    HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p.choose i) : R)
i₃ :
  HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p.choose i) : R) =
    HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p * (p.choose i / p)) : R)
⊢ (u * x) ^ i * (↑(p.choose i) : R) =
    (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R))))
have i₄ : HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p * (p.choose i / p)) : R) =
  HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑p : R) * (↑(p.choose i / p) : R)
Tactic: calc
      (u * x) ^ i * p.choose i =
        (u * x) ^ (2 + (i - 2)) * p.choose i := by rw [Nat.add_sub_of_le hi']
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p.choose i := by ring_nf
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * (p * (p.choose i / p) : ℕ) := by
        rw [Nat.mul_div_cancel' (hp.dvd_choose_self hi.2.2.1 <| by lia)]
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p * (p.choose i / p : ℕ) := by
        simp only [Nat.cast_mul]; ring_nf
      _ = p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * (p.choose i / p : ℕ)))) := by
        rw [ha]; ring
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
i₁ : (u * x) ^ i * (↑(p.choose i) : R) = (u * x) ^ (2 + (i - 2)) * (↑(p.choose i) : R)
i₂ :
  (u * x) ^ (2 + (i - 2)) * (↑(p.choose i) : R) =
    HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p.choose i) : R)
i₃ :
  HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p.choose i) : R) =
    HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p * (p.choose i / p)) : R)
i₄ :
  HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p * (p.choose i / p)) : R) =
    HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑p : R) * (↑(p.choose i / p) : R)
⊢ (u * x) ^ i * (↑(p.choose i) : R) =
    (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R))))
have i₅ : HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑p : R) * (↑(p.choose i / p) : R) =
  (↑p : R) * u * (v * (a * HPow.hPow (β := ℕ) x 2 * ((u * x) ^ (i - 2) * (↑(p.choose i / p) : R))))
Tactic: calc
      (u * x) ^ i * p.choose i =
        (u * x) ^ (2 + (i - 2)) * p.choose i := by rw [Nat.add_sub_of_le hi']
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p.choose i := by ring_nf
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * (p * (p.choose i / p) : ℕ) := by
        rw [Nat.mul_div_cancel' (hp.dvd_choose_self hi.2.2.1 <| by lia)]
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p * (p.choose i / p : ℕ) := by
        simp only [Nat.cast_mul]; ring_nf
      _ = p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * (p.choose i / p : ℕ)))) := by
        rw [ha]; ring
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
⊢ u ^ p * x ^ p = (↑p : R) * u * v * b * x ^ p
have rw : (↑p : R) * u * v * b * x ^ p = (↑p : R) * u * v * b * x ^ p
Tactic: rw [hb]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
⊢ (u * x) ^ p * (↑(p.choose p) : R) = (↑p : R) * u * (v * (b * x ^ p))
have p₁ : (u * x) ^ p * (↑(p.choose p) : R) = u ^ p * x ^ p
Tactic: calc
      (u * x) ^ p * (p.choose p) = u ^ p * x ^ p := by simp [Nat.choose_self, mul_pow]
    _ = p * u * v * b * x ^ p := by rw [hb]
    _ = p * u * (v * (b * x ^ p)) := by ring_nf
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
p₁ : (u * x) ^ p * (↑(p.choose p) : R) = u ^ p * x ^ p
⊢ (u * x) ^ p * (↑(p.choose p) : R) = (↑p : R) * u * (v * (b * x ^ p))
have p₂ : u ^ p * x ^ p = (↑p : R) * u * v * b * x ^ p
Tactic: calc
      (u * x) ^ p * (p.choose p) = u ^ p * x ^ p := by simp [Nat.choose_self, mul_pow]
    _ = p * u * v * b * x ^ p := by rw [hb]
    _ = p * u * (v * (b * x ^ p)) := by ring_nf
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = (↑p : R) * u * v * b
p₁ : (u * x) ^ p * (↑(p.choose p) : R) = u ^ p * x ^ p
p₂ : u ^ p * x ^ p = (↑p : R) * u * v * b * x ^ p
⊢ (u * x) ^ p * (↑(p.choose p) : R) = (↑p : R) * u * (v * (b * x ^ p))
have p₃ : (↑p : R) * u * v * b * x ^ p = (↑p : R) * u * (v * (b * x ^ p))
Tactic: calc
      (u * x) ^ p * (p.choose p) = u ^ p * x ^ p := by simp [Nat.choose_self, mul_pow]
    _ = p * u * v * b * x ^ p := by rw [hb]
    _ = p * u * (v * (b * x ^ p)) := by ring_nf
-- 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), (1 + u * x) ^ p ^ (m + 1) = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * y)
have rw : ∃ (y : R), ((1 + u * x) ^ p) ^ p ^ m = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * y)
Tactic: rw [pow_succ', pow_mul]
-- 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), ((1 + u * x) ^ p) ^ p ^ m = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * y)
have obtain : ∀ (y : R) (hy : (1 + u * x) ^ p = 1 + (↑p : R) * u * (x + v * y)),
  ∃ (y : R), ((1 + u * x) ^ p) ^ p ^ m = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * y)
Tactic: obtain ⟨y, hy⟩ := exists_one_add_mul_pow_prime_eq hp hvu hpuv x
-- 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 : R), ((1 + u * x) ^ p) ^ p ^ m = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * y)
have rw : ∃ (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: rw [hy]
-- 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)
⊢ (↑p : R) * ((↑p : R) * u) * ((↑p : R) * v) ∣ ((↑p : R) * u) ^ p
have rw : (↑p : R) * ((↑p : R) * u) * ((↑p : R) * v) ∣ HPow.hPow (α := R) (↑p : R) p * u ^ p
Tactic: rw [mul_pow]
-- 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)
⊢ (↑p : R) * ((↑p : R) * u) * ((↑p : R) * v) ∣ HPow.hPow (α := R) (↑p : R) p * u ^ p
have simp : HMul.hMul (α := R) (↑p : R) (↑p : R) * u * (↑p : R) * v ∣ HPow.hPow (α := R) (↑p : R) p * u ^ p
Tactic: simp only [← mul_assoc]
-- 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) * u * (↑p : R) * v ∣ HPow.hPow (α := R) (↑p : R) p * u ^ p
have rw : HMul.hMul (α := R) (↑p : R) (↑p : R) * ((↑p : R) * u * v) ∣ HPow.hPow (α := R) (↑p : R) p * u ^ p
Tactic: rw [mul_assoc, mul_assoc, ← mul_assoc u, mul_comm u]
-- 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) * ((↑p : R) * u * v) ∣ HPow.hPow (α := R) (↑p : R) p * u ^ p
have apply : HMul.hMul (α := R) (↑p : R) (↑p : R) ∣ HPow.hPow (α := R) (↑p : R) p
Tactic: apply mul_dvd_mul _ hpuv