awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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
rw rw₁ : (u * x) ^ i * (↑(p.choose i) : R) = (u * x) ^ i * (↑(p.choose i) : R)
⊢ (u * x) ^ i * (↑(p.choose i) : R) = (u * x) ^ (2 + (i - 2)) * (↑(p.choose i) : R)

Tactic:
rw [Nat.add_sub_of_le hi']

Premises used: Nat.add_sub_of_le
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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) ^ (2 + (i - 2)) * (↑(p.choose i) : R) =
    HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) x 2 * (u * x) ^ (i - 2) * (↑(p.choose i) : R)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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 < p

Tactic:
lia
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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
rw 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)
⊢ 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:
rw [Nat.mul_div_cancel' (hp.dvd_choose_self hi.2.2.1 <| by lia)]

Premises used: Nat.Prime.dvd_choose_self, And.right, And.left, Nat.mul_div_cancel'
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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
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)
⊢ 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:
simp only [Nat.cast_mul]

Premises used: Nat.cast_mul
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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) *
      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:
ring_nf
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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
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))))
⊢ 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:
rw [ha]
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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 (β := ℕ) (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:
ring
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
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))))
⊢ (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:
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

Premises used: Nat.choose, HMul.hMul, HSub.hSub, HDiv.hDiv, Nat.cast, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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) = u ^ p * x ^ p

Tactic:
simp [Nat.choose_self, mul_pow]

Premises used: mul_pow, Nat.choose_self
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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
rw rw₁ : (↑p : R) * u * v * b * x ^ p = (↑p : R) * u * v * b * x ^ p
⊢ u ^ p * x ^ p = (↑p : R) * u * v * b * x ^ p

Tactic:
rw [hb]
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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 : R) * u * v * b * x ^ p = (↑p : R) * u * (v * (b * x ^ p))

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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
p₃ : (↑p : R) * u * v * b * x ^ p = (↑p : R) * u * (v * (b * x ^ p))
⊢ (u * x) ^ p * (↑(p.choose p) : R) = (↑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

Premises used: Nat.choose, HMul.hMul, HPow.hPow
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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 + u * x) ^ HPow.hPow (β := ℕ) p 0 = 1 + HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * u * (x + v * 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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 : ℕ
rw : ∃ (y : R), ((1 + u * x) ^ p) ^ p ^ m = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * y)
⊢ ∃ (y : R), (1 + u * x) ^ p ^ (m + 1) = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * y)

Tactic:
rw [pow_succ', pow_mul]

Premises used: pow_mul, pow_succ'
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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 : ℕ
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)
⊢ ∃ (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

Premises used: ZMod.exists_one_add_mul_pow_prime_eq
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
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)
⊢ ∃ (y : R), ((1 + u * x) ^ p) ^ p ^ m = 1 + HPow.hPow (α := R) (↑p : R) (m + 1) * u * (x + v * y)

Tactic:
rw [hy]
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
rw : (↑p : R) * ((↑p : R) * u) * ((↑p : R) * v) ∣ HPow.hPow (α := R) (↑p : R) p * u ^ p
⊢ (↑p : R) * ((↑p : R) * u) * ((↑p : R) * v) ∣ ((↑p : R) * u) ^ p

Tactic:
rw [mul_pow]

Premises used: mul_pow
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
simp : HMul.hMul (α := R) (↑p : R) (↑p : R) * u * (↑p : R) * v ∣ HPow.hPow (α := R) (↑p : R) p * u ^ p
⊢ (↑p : R) * ((↑p : R) * u) * ((↑p : R) * v) ∣ HPow.hPow (α := R) (↑p : R) p * u ^ p

Tactic:
simp only [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
rw : HMul.hMul (α := R) (↑p : R) (↑p : R) * ((↑p : R) * u * v) ∣ HPow.hPow (α := R) (↑p : R) p * u ^ p
⊢ HMul.hMul (α := R) (↑p : R) (↑p : R) * u * (↑p : R) * v ∣ HPow.hPow (α := R) (↑p : R) p * u ^ p

Tactic:
rw [mul_assoc, mul_assoc, ← mul_assoc u, mul_comm u]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
apply : HMul.hMul (α := R) (↑p : R) (↑p : R) ∣ HPow.hPow (α := R) (↑p : R) p
⊢ HMul.hMul (α := R) (↑p : R) (↑p : R) * ((↑p : R) * u * v) ∣ HPow.hPow (α := R) (↑p : R) p * u ^ p

Tactic:
apply mul_dvd_mul _ hpuv

Premises used: mul_dvd_mul
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
rw : HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ HPow.hPow (α := R) (↑p : R) p
⊢ HMul.hMul (α := R) (↑p : R) (↑p : R) ∣ HPow.hPow (α := R) (↑p : R) p

Tactic:
rw [← pow_two]

Premises used: pow_two
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
⊢ HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ HPow.hPow (α := R) (↑p : R) p

Tactic:
pow_dvd_pow _ hp.two_le

Premises used: pow_dvd_pow, Nat.Prime.two_le
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
⊢ HPow.hPow (α := R) (β := ℕ) (↑p : R) 2 ∣ HPow.hPow (α := R) (↑p : R) p

Tactic:
exact pow_dvd_pow _ hp.two_le

Premises used: pow_dvd_pow, Nat.Prime.two_le
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
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)
⊢ ∃ (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

Premises used: HMul.hMul, mul_dvd_mul_left, HAdd.hAdd
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
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))
⊢ ∃ (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:
use y + p * z
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
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))
⊢ (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:
rw [hz]
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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 + 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:
ring
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n : ℕ
rw : orderOf (1 + HMul.hMul (α := ZMod (p ^ m)) 0 (↑a : ZMod (p ^ m))) = HPow.hPow (β := ℕ) p 0
⊢ orderOf (1 + HPow.hPow (α := ZMod (p ^ (0 + m))) (↑p : ZMod (p ^ (0 + m))) m * (↑a : ZMod (p ^ (0 + m)))) =
    HPow.hPow (β := ℕ) p 0

Tactic:
rw [← Nat.cast_pow, zero_add m, ZMod.natCast_self]

Premises used: ZMod.natCast_self, zero_add, Nat.cast_pow
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n : ℕ
⊢ orderOf (1 + HMul.hMul (α := ZMod (p ^ m)) 0 (↑a : ZMod (p ^ m))) = HPow.hPow (β := ℕ) p 0

Tactic:
simp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬(↑p : ℤ) ∣ a
n_1 n : ℕ
⊢ Fact (Nat.Prime p)

Tactic:
have := Fact.mk hp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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)
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
⊢ 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
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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
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
⊢ 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:
apply orderOf_eq_prime_pow

Premises used: orderOf_eq_prime_pow
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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 :
  ∀ (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
⊢ ¬(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
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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 :
  ¬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
⊢ ¬(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:
rw [hy, ← pow_add, add_eq_left, mul_add, ← mul_assoc, ← pow_succ]

Premises used: pow_succ, mul_assoc, pow_add, add_eq_left, mul_add
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
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
⊢ ¬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:
simp_rw [add_right_comm n _ 1, ← Nat.cast_pow, ZMod.natCast_self, zero_mul, add_zero]

Premises used: ZMod.natCast_self, MulZeroClass.zero_mul, add_right_comm, Nat.cast_pow, add_zero, OfNat.ofNat