awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
rw : gaussSum (χ ^ p) (ψ ^ p) = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
rw₁ : gaussSum (χ ^ p) (ψ.mulShift (↑p : R)) = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
rw₂ : gaussSum χ (ψ.mulShift (↑p : R)) = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
rw₃ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R')
      (HMul.hMul (α := R') ((χ : (a : R) → R') (↑hp.unit : R) : R') (gaussSum χ (ψ.mulShift (↑hp.unit : R))))
rw₄ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (↑p : R) : R') ((χ : (a : R) → R') (↑hp.unit : R) : R') *
      gaussSum χ (ψ.mulShift (↑hp.unit : R))
rw₅ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (↑p : R) : R') ((χ : (a : R) → R') (↑p : R) : R') *
      gaussSum χ (ψ.mulShift (↑p : R))
rw₆ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑p : R) : R') 2 * gaussSum χ (ψ.mulShift (↑p : R))
rw₇ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') ((HPow.hPow (β := ℕ) χ 2 : (a : R) → R') (↑p : R) : R') (gaussSum χ (ψ.mulShift (↑p : R)))
rw₈ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') ((1 : (a : R) → R') (↑p : R) : R') (gaussSum χ (ψ.mulShift (↑p : R)))
rw₉ :
  gaussSum χ (ψ.mulShift (↑hp.unit : R)) =
    HMul.hMul (α := R') ((1 : (a : R) → R') (↑hp.unit : R) : R') (gaussSum χ (ψ.mulShift (↑hp.unit : R)))
⊢ gaussSum χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
have rw₁₀ : gaussSum χ (ψ.mulShift (↑hp.unit : R)) = 1 * gaussSum χ (ψ.mulShift (↑hp.unit : R))
Tactic: rw [_root_.gaussSum_frob, pow_mulShift, hχ.pow_char p, ← gaussSum_mulShift χ ψ hp.unit,
    ← mul_assoc, hp.unit_spec, ← pow_two, ← pow_apply' _ two_ne_zero, hχ.sq_eq_one, ← hp.unit_spec,
    one_apply_coe, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
rw : gaussSum (χ ^ p) (ψ ^ p) = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
rw₁ : gaussSum (χ ^ p) (ψ.mulShift (↑p : R)) = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
rw₂ : gaussSum χ (ψ.mulShift (↑p : R)) = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
rw₃ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R')
      (HMul.hMul (α := R') ((χ : (a : R) → R') (↑hp.unit : R) : R') (gaussSum χ (ψ.mulShift (↑hp.unit : R))))
rw₄ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (↑p : R) : R') ((χ : (a : R) → R') (↑hp.unit : R) : R') *
      gaussSum χ (ψ.mulShift (↑hp.unit : R))
rw₅ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (↑p : R) : R') ((χ : (a : R) → R') (↑p : R) : R') *
      gaussSum χ (ψ.mulShift (↑p : R))
rw₆ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑p : R) : R') 2 * gaussSum χ (ψ.mulShift (↑p : R))
rw₇ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') ((HPow.hPow (β := ℕ) χ 2 : (a : R) → R') (↑p : R) : R') (gaussSum χ (ψ.mulShift (↑p : R)))
rw₈ :
  gaussSum χ (ψ.mulShift (↑p : R)) =
    HMul.hMul (α := R') ((1 : (a : R) → R') (↑p : R) : R') (gaussSum χ (ψ.mulShift (↑p : R)))
rw₉ :
  gaussSum χ (ψ.mulShift (↑hp.unit : R)) =
    HMul.hMul (α := R') ((1 : (a : R) → R') (↑hp.unit : R) : R') (gaussSum χ (ψ.mulShift (↑hp.unit : R)))
rw₁₀ : gaussSum χ (ψ.mulShift (↑hp.unit : R)) = 1 * gaussSum χ (ψ.mulShift (↑hp.unit : R))
⊢ gaussSum χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
have rw₁₁ : gaussSum χ (ψ.mulShift (↑hp.unit : R)) = gaussSum χ (ψ.mulShift (↑hp.unit : R))
Tactic: rw [_root_.gaussSum_frob, pow_mulShift, hχ.pow_char p, ← gaussSum_mulShift χ ψ hp.unit,
    ← mul_assoc, hp.unit_spec, ← pow_two, ← pow_apply' _ two_ne_zero, hχ.sq_eq_one, ← hp.unit_spec,
    one_apply_coe, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ HPow.hPow (β := ℕ) p 0 =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
have zero : HPow.hPow (β := ℕ) (gaussSum χ ψ) 1 =
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
Tactic: rw [pow_zero, pow_one, pow_zero, MulChar.map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
zero :
  HPow.hPow (β := ℕ) (gaussSum χ ψ) 1 =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
⊢ gaussSum χ ψ ^ HPow.hPow (β := ℕ) p 0 =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
have zero₁ : gaussSum χ ψ = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
Tactic: rw [pow_zero, pow_one, pow_zero, MulChar.map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
zero :
  HPow.hPow (β := ℕ) (gaussSum χ ψ) 1 =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
zero₁ :
  gaussSum χ ψ = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
⊢ gaussSum χ ψ ^ HPow.hPow (β := ℕ) p 0 =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
have zero₂ : gaussSum χ ψ = HMul.hMul (α := R') ((χ : (a : R) → R') 1 : R') (gaussSum χ ψ)
Tactic: rw [pow_zero, pow_one, pow_zero, MulChar.map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
zero :
  HPow.hPow (β := ℕ) (gaussSum χ ψ) 1 =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
zero₁ :
  gaussSum χ ψ = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
zero₂ : gaussSum χ ψ = HMul.hMul (α := R') ((χ : (a : R) → R') 1 : R') (gaussSum χ ψ)
⊢ gaussSum χ ψ ^ HPow.hPow (β := ℕ) p 0 =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
have zero₃ : gaussSum χ ψ = 1 * gaussSum χ ψ
Tactic: rw [pow_zero, pow_one, pow_zero, MulChar.map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
zero :
  HPow.hPow (β := ℕ) (gaussSum χ ψ) 1 =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
zero₁ :
  gaussSum χ ψ = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
zero₂ : gaussSum χ ψ = HMul.hMul (α := R') ((χ : (a : R) → R') 1 : R') (gaussSum χ ψ)
zero₃ : gaussSum χ ψ = 1 * gaussSum χ ψ
⊢ gaussSum χ ψ ^ HPow.hPow (β := ℕ) p 0 =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (β := ℕ) (↑p : R) 0) : R') (gaussSum χ ψ)
have zero₄ : gaussSum χ ψ = gaussSum χ ψ
Tactic: rw [pow_zero, pow_one, pow_zero, MulChar.map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
⊢ gaussSum χ ψ ^ p ^ (n + 1) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
have succ : gaussSum χ ψ ^ (p ^ n * p) =
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
Tactic: rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul,
      ← pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
succ :
  gaussSum χ ψ ^ (p ^ n * p) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
⊢ gaussSum χ ψ ^ p ^ (n + 1) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
have succ₁ : (gaussSum χ ψ ^ p ^ n) ^ p =
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
Tactic: rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul,
      ← pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
succ :
  gaussSum χ ψ ^ (p ^ n * p) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₁ :
  (gaussSum χ ψ ^ p ^ n) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
⊢ gaussSum χ ψ ^ p ^ (n + 1) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
have succ₂ : HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ) ^ p =
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
Tactic: rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul,
      ← pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
succ :
  gaussSum χ ψ ^ (p ^ n * p) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₁ :
  (gaussSum χ ψ ^ p ^ n) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₂ :
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
⊢ gaussSum χ ψ ^ p ^ (n + 1) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
have succ₃ : HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p * gaussSum χ ψ ^ p =
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
Tactic: rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul,
      ← pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
succ :
  gaussSum χ ψ ^ (p ^ n * p) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₁ :
  (gaussSum χ ψ ^ p ^ n) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₂ :
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₃ :
  HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p * gaussSum χ ψ ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
⊢ gaussSum χ ψ ^ p ^ (n + 1) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
have succ₄ : HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p *
    HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ) =
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
Tactic: rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul,
      ← pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
succ :
  gaussSum χ ψ ^ (p ^ n * p) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₁ :
  (gaussSum χ ψ ^ p ^ n) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₂ :
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₃ :
  HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p * gaussSum χ ψ ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₄ :
  HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p *
      HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
⊢ gaussSum χ ψ ^ p ^ (n + 1) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
have succ₅ : HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p)
      ((χ : (a : R) → R') (↑p : R) : R') *
    gaussSum χ ψ =
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
Tactic: rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul,
      ← pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
succ :
  gaussSum χ ψ ^ (p ^ n * p) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₁ :
  (gaussSum χ ψ ^ p ^ n) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₂ :
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₃ :
  HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p * gaussSum χ ψ ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₄ :
  HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p *
      HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₅ :
  HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p)
        ((χ : (a : R) → R') (↑p : R) : R') *
      gaussSum χ ψ =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
⊢ gaussSum χ ψ ^ p ^ (n + 1) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
have succ₆ : HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p)
      ((χ : (a : R) → R') (↑p : R) : R') *
    gaussSum χ ψ =
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n * (↑p : R)) : R') (gaussSum χ ψ)
Tactic: rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul,
      ← pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit.{u} (M := R) (↑p : R)
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ)
succ :
  gaussSum χ ψ ^ (p ^ n * p) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₁ :
  (gaussSum χ ψ ^ p ^ n) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₂ :
  HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') (gaussSum χ ψ) ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₃ :
  HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p * gaussSum χ ψ ^ p =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₄ :
  HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p *
      HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₅ :
  HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p)
        ((χ : (a : R) → R') (↑p : R) : R') *
      gaussSum χ ψ =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
succ₆ :
  HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p)
        ((χ : (a : R) → R') (↑p : R) : R') *
      gaussSum χ ψ =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n * (↑p : R)) : R') (gaussSum χ ψ)
⊢ gaussSum χ ψ ^ p ^ (n + 1) =
    HMul.hMul (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) (n + 1)) : R') (gaussSum χ ψ)
have succ₇ : HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R') p)
      ((χ : (a : R) → R') (↑p : R) : R') *
    gaussSum χ ψ =
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R')
      ((χ : (a : R) → R') (↑p : R) : R') *
    gaussSum χ ψ
Tactic: rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul,
      ← pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]