awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
ind :
  HSub.hSub (α := MvPolynomial ℕ R) (W_ R n)
      (∑ x ∈ range n,
        (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          (HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x))))) =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R)
⊢ HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (W_ R n)
        (∑ x ∈ range n,
          (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
            (HMul.hMul (α := MvPolynomial ℕ R)
              ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
              (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x))))))
      ((algebraMap R (MvPolynomial ℕ R) : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R) =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
ind :
  Eq.{u_1 + 1} (α := MvPolynomial ℕ R)
    (∑ x ∈ range n,
      HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (X x) (p ^ (n - x))))
    (∑ x ∈ range n,
      (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
        (HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x)))))
⊢ HSub.hSub (α := MvPolynomial ℕ R) (W_ R n)
      (∑ x ∈ range n,
        (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          (HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x))))) =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R)

Tactic:
rw [wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ_comm,
    tsub_self, pow_zero, pow_one, mul_comm (X n), add_sub_assoc, add_eq_left, sub_eq_zero]

Premises used: add_sub_assoc, sub_eq_zero, tsub_self, MvPolynomial.X, Finset.sum_range_succ_comm, pow_zero, add_eq_left, pow_one, mul_comm, wittPolynomial_eq_sum_C_mul_X_pow
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
ind :
  ∀ x ∈ range n,
    HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (X x) (p ^ (n - x))) =
      (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
        (HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x))))
⊢ Eq.{u_1 + 1} (α := MvPolynomial ℕ R)
    (∑ x ∈ range n,
      HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (X x) (p ^ (n - x))))
    (∑ x ∈ range n,
      (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
        (HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x)))))

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
i : ℕ
h : i ∈ range n
⊢ i < n

Tactic:
rw [mem_range] at h

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.ZMod.Torsion
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
h :
  ∀ (x : (ZMod p)ˣ),
    Membership.mem (γ := Subgroup (ZMod p)ˣ) (rootsOfUnity (p - 1) (ZMod p)) x ↔
      Membership.mem (γ := Subgroup (ZMod p)ˣ) ⊤ x
⊢ Eq (α := Subgroup (ZMod p)ˣ) (rootsOfUnity (p - 1) (ZMod p)) ⊤

Tactic:
ext
-- Module: Mathlib.RingTheory.ZMod.Torsion
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
⊢ Membership.mem (γ := Subgroup (ZMod p)ˣ) (rootsOfUnity (p - 1) (ZMod p)) x ↔
    Membership.mem (γ := Subgroup (ZMod p)ˣ) ⊤ x

Tactic:
simpa [Units.ext_iff] using pow_card_sub_one_eq_one (Units.ne_zero _)

Premises used: Units.ext_iff, ZMod.pow_card_sub_one_eq_one
-- Module: Mathlib.RingTheory.ZMod.Torsion
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ 2 ≤ p

Tactic:
have : 2 ≤ p := Nat.Prime.two_le Fact.out
-- Module: Mathlib.RingTheory.ZMod.Torsion
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this : 2 ≤ p
⊢ p - 1 ≠ 0

Tactic:
grind
-- Module: Mathlib.RingTheory.ZMod.Torsion
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ NeZero (p - 1)

Tactic:
have : NeZero (p - 1) := ⟨by have : 2 ≤ p := Nat.Prime.two_le Fact.out; grind⟩
-- Module: Mathlib.RingTheory.ZMod.Torsion
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this : NeZero (p - 1)
⊢ HasEnoughRootsOfUnity (ZMod p) (p - 1)

Tactic:
HasEnoughRootsOfUnity.of_card_le ?_

Premises used: HasEnoughRootsOfUnity.of_card_le
-- Module: Mathlib.RingTheory.ZMod.Torsion
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this : NeZero (p - 1)
refine : p - 1 ≤ Fintype.card ↥(rootsOfUnity (p - 1) (ZMod p))
⊢ HasEnoughRootsOfUnity (ZMod p) (p - 1)

Tactic:
refine HasEnoughRootsOfUnity.of_card_le ?_

Premises used: HasEnoughRootsOfUnity.of_card_le
-- Module: Mathlib.RingTheory.ZMod.Torsion
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this : NeZero (p - 1)
⊢ Nat.card ↥(rootsOfUnity (p - 1) (ZMod p)) = Nat.card ↥⊤

Tactic:
have := Nat.card_congr (MulEquiv.subgroupCongr (ZMod.rootsOfUnity_eq_top (p := p))).toEquiv
-- Module: Mathlib.RingTheory.ZMod.Torsion
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this_1 : NeZero (p - 1)
this : Nat.card ↥(rootsOfUnity (p - 1) (ZMod p)) = Nat.card ↥⊤
⊢ Fintype.card ↥(rootsOfUnity (p - 1) (ZMod p)) = Nat.card ↥⊤

Tactic:
rw [Nat.card_eq_fintype_card] at this

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.ZMod.Torsion
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this_1 : NeZero (p - 1)
this : Fintype.card ↥(rootsOfUnity (p - 1) (ZMod p)) = Nat.card ↥⊤
rw : p - 1 ≤ Nat.card ↥⊤
⊢ p - 1 ≤ Fintype.card ↥(rootsOfUnity (p - 1) (ZMod p))

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.ZMod.Torsion
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this_1 : NeZero (p - 1)
this : Fintype.card ↥(rootsOfUnity (p - 1) (ZMod p)) = Nat.card ↥⊤
⊢ p - 1 ≤ Nat.card ↥⊤

Tactic:
simp [Fintype.card_units]

Premises used: Fintype.card_units
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
⊢ IsCyclic (ZMod 0)ˣ

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
⊢ IsCyclic (ZMod 1)ˣ

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
⊢ IsCyclic (ZMod 2)ˣ

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
apply : Nat.card (ZMod 4)ˣ = 2
⊢ IsCyclic (ZMod 4)ˣ

Tactic:
apply isCyclic_of_prime_card (p := 2)

Premises used: isCyclic_of_prime_card
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
simp : φ 4 = 2
⊢ Nat.card (ZMod 4)ˣ = 2

Tactic:
simp only [Nat.card_eq_fintype_card, card_units_eq_totient]

Premises used: ZMod.card_units_eq_totient, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
⊢ φ 4 = 2

Tactic:
decide
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
p : ℕ
hp : Nat.Prime p
⊢ IsCyclic (ZMod p)ˣ

Tactic:
have : Fact (p.Prime) := ⟨hp⟩
  inferInstance

Premises used: inferInstance, Fact.mk
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
rw : ¬Monoid.exponent (ZMod 8)ˣ = φ 8
⊢ ¬IsCyclic (ZMod 8)ˣ

Tactic:
rw [IsCyclic.iff_exponent_eq_card, Nat.card_eq_fintype_card, card_units_eq_totient]

Premises used: ZMod.card_units_eq_totient, IsCyclic.iff_exponent_eq_card, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
⊢ ∀ (g : (ZMod 8)ˣ), HPow.hPow (β := ℕ) g 2 = 1

Tactic:
decide
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
⊢ Monoid.exponent (ZMod 8)ˣ ∣ 2

Tactic:
have h : Monoid.exponent (ZMod 8)ˣ ∣ 2 := Monoid.exponent_dvd_of_forall_pow_eq_one (by decide)
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
h : Monoid.exponent (ZMod 8)ˣ ∣ 2
h' : Monoid.exponent (ZMod 8)ˣ = 4
⊢ False

Tactic:
simp [h'] at h
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
rw :
  ∃ (y : R),
    ∑ m ∈ Finset.range (p + 1), (u * x) ^ m * HPow.hPow (α := R) 1 (p - m) * (↑(p.choose m) : R) =
      1 + (↑p : R) * u * (x + v * y)
⊢ ∃ (y : R), (1 + u * x) ^ p = 1 + (↑p : R) * u * (x + v * y)

Tactic:
rw [add_comm, add_pow]

Premises used: add_comm, add_pow
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
⊢ 0 ∈ Finset.range (p + 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
rw :
  ∃ (y : R),
    HPow.hPow (β := ℕ) (u * x) 0 * HPow.hPow (α := R) 1 (p - 0) * (↑(p.choose 0) : R) +
        ∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * HPow.hPow (α := R) 1 (p - x_1) * (↑(p.choose x_1) : R) =
      1 + (↑p : R) * u * (x + v * y)
⊢ ∃ (y : R),
    ∑ m ∈ Finset.range (p + 1), (u * x) ^ m * HPow.hPow (α := R) 1 (p - m) * (↑(p.choose m) : R) =
      1 + (↑p : R) * u * (x + v * y)

Tactic:
rw [← Finset.add_sum_erase (a := 0) _ _ (by simp)]

Premises used: Finset.add_sum_erase
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
simp_rw :
  ∃ (y : R),
    HAdd.hAdd (α := R) 1 (∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * (↑(p.choose x_1) : R)) =
      1 + (↑p : R) * u * (x + v * y)
⊢ ∃ (y : R),
    HPow.hPow (β := ℕ) (u * x) 0 * HPow.hPow (α := R) 1 (p - 0) * (↑(p.choose 0) : R) +
        ∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * HPow.hPow (α := R) 1 (p - x_1) * (↑(p.choose x_1) : R) =
      1 + (↑p : R) * u * (x + v * y)

Tactic:
simp_rw [one_pow, pow_zero, Nat.choose_zero_right, Nat.cast_one, mul_one]

Premises used: one_pow, pow_zero, mul_one, Nat.cast_one, Nat.choose_zero_right
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
⊢ 1 ∈ (Finset.range (p + 1)).erase 0

Tactic:
simp [hp.pos]

Premises used: Nat.Prime.pos
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
rw :
  ∃ (y : R),
    1 +
        (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
          ∑ x_1 ∈ ((Finset.range (p + 1)).erase 0).erase 1, (u * x) ^ x_1 * (↑(p.choose x_1) : R)) =
      1 + (↑p : R) * u * (x + v * y)
⊢ ∃ (y : R),
    HAdd.hAdd (α := R) 1 (∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * (↑(p.choose x_1) : R)) =
      1 + (↑p : R) * u * (x + v * y)

Tactic:
rw [← Finset.add_sum_erase (a := 1) _ _ (by simp [hp.pos])]

Premises used: Finset.add_sum_erase
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
simp : p ≠ 1 ∧ p ≠ 0 ∧ p ∈ Finset.range (p + 1)
⊢ p ∈ ((Finset.range (p + 1)).erase 0).erase 1

Tactic:
simp only [Finset.mem_erase]

Premises used: Finset.mem_erase
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
rw : 2 ≤ p ∧ p ∈ Finset.range (p + 1)
⊢ p ≠ 1 ∧ p ≠ 0 ∧ p ∈ Finset.range (p + 1)

Tactic:
rw [← and_assoc, and_comm (a := ¬ _), ← Nat.two_le_iff]

Premises used: Nat.two_le_iff, and_comm, and_assoc
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
⊢ 2 ≤ p ∧ p ∈ Finset.range (p + 1)

Tactic:
simp [hp.two_le]

Premises used: Nat.Prime.two_le
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
rw :
  ∃ (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)
⊢ ∃ (y : R),
    1 +
        (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
          ∑ x_1 ∈ ((Finset.range (p + 1)).erase 0).erase 1, (u * x) ^ x_1 * (↑(p.choose x_1) : R)) =
      1 + (↑p : R) * u * (x + v * y)

Tactic:
rw [← Finset.sum_erase_add (a := p) _ _ (by -- aesop works but is slow
      simp only [Finset.mem_erase]
      rw [← and_assoc, and_comm (a := ¬ _), ← Nat.two_le_iff]
      simp [hp.two_le])]

Premises used: Finset.sum_erase_add
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
obtain :
  ∀ (a : R) (ha : u = v * a),
    ∃ (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)
⊢ ∃ (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)

Tactic:
obtain ⟨a, ha⟩ := hvu
-- Module: Mathlib.RingTheory.ZMod.UnitsCyclic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hpuv : (↑p : R) * u * v ∣ u ^ p
x a : R
ha : u = v * a
obtain :
  ∀ (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)
⊢ ∃ (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)

Tactic:
obtain ⟨b, hb⟩ := hpuv
-- 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
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))
⊢ ∃ (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)

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

Premises used: HMul.hMul, Finset.range, HAdd.hAdd, OfNat.ofNat, Finset.erase
-- 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
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)))
⊢ 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:
rw [mul_add]

Premises used: mul_add
-- 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
h : HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) = (↑p : R) * u * x
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))
⊢ 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:
congr 2
-- 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
h : HPow.hPow (β := ℕ) (u * x) 1 * (↑p : R) = (↑p : R) * u * x
⊢ HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) = (↑p : R) * u * x

Tactic:
rw [Nat.choose_one_right]

Premises used: Nat.choose_one_right
-- 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
⊢ HPow.hPow (β := ℕ) (u * x) 1 * (↑p : R) = (↑p : R) * u * x

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
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))
⊢ ∑ 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:
simp only [mul_add, Finset.mul_sum]

Premises used: Finset.mul_sum, mul_add
-- 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
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)))))
h₁ : (u * x) ^ p * (↑(p.choose p) : R) = (↑p : R) * u * (v * (b * x ^ p))
⊢ ∑ 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:
congr 1
-- 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
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))))
⊢ 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 with i hi
-- 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 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p
⊢ ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1

Tactic:
simp only [Finset.mem_erase, ne_eq, Finset.mem_range] at hi

Premises used: Finset.mem_range, ne_eq, Finset.mem_erase
-- 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
⊢ 2 ≤ i

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
⊢ 2 ≤ i

Tactic:
have hi' : 2 ≤ i := by lia