awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
h : χ ^ (orderOf χ - 1) = χ⁻¹
rw :
  gaussSum χ ψ * gaussSum χ⁻¹ ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₁ :
  gaussSum χ ψ * HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (-1) : R') (gaussSum χ⁻¹ ψ⁻¹) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
have rw₂ : HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (-1) : R') (gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹) =
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
Tactic: rw [h, ← mul_gaussSum_inv_eq_gaussSum χ⁻¹, mul_left_comm, gaussSum_mul_gaussSum_eq_card hχ hψ,
    MulChar.inv_apply', inv_neg_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
h : χ ^ (orderOf χ - 1) = χ⁻¹
rw :
  gaussSum χ ψ * gaussSum χ⁻¹ ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₁ :
  gaussSum χ ψ * HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (-1) : R') (gaussSum χ⁻¹ ψ⁻¹) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₂ :
  HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (-1) : R') (gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
have rw₃ : HMul.hMul (α := R') (β := R') ((χ⁻¹ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R') =
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
Tactic: rw [h, ← mul_gaussSum_inv_eq_gaussSum χ⁻¹, mul_left_comm, gaussSum_mul_gaussSum_eq_card hχ hψ,
    MulChar.inv_apply', inv_neg_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
h : χ ^ (orderOf χ - 1) = χ⁻¹
rw :
  gaussSum χ ψ * gaussSum χ⁻¹ ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₁ :
  gaussSum χ ψ * HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (-1) : R') (gaussSum χ⁻¹ ψ⁻¹) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₂ :
  HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (-1) : R') (gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₃ :
  HMul.hMul (α := R') (β := R') ((χ⁻¹ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
have rw₄ : HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1)⁻¹ : R') ((↑(Fintype.card R) : R') : R') =
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
Tactic: rw [h, ← mul_gaussSum_inv_eq_gaussSum χ⁻¹, mul_left_comm, gaussSum_mul_gaussSum_eq_card hχ hψ,
    MulChar.inv_apply', inv_neg_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
h : χ ^ (orderOf χ - 1) = χ⁻¹
rw :
  gaussSum χ ψ * gaussSum χ⁻¹ ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₁ :
  gaussSum χ ψ * HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (-1) : R') (gaussSum χ⁻¹ ψ⁻¹) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₂ :
  HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (-1) : R') (gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹) =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₃ :
  HMul.hMul (α := R') (β := R') ((χ⁻¹ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
rw₄ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1)⁻¹ : R') ((↑(Fintype.card R) : R') : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
have rw₅ : HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R') =
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
Tactic: rw [h, ← mul_gaussSum_inv_eq_gaussSum χ⁻¹, mul_left_comm, gaussSum_mul_gaussSum_eq_card hχ hψ,
    MulChar.inv_apply', inv_neg_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
⊢ HPow.hPow (β := ℕ) (gaussSum χ ψ) 2 =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (-1) : R') ((↑(Fintype.card R) : R') : R')
have rw : gaussSum χ ψ * gaussSum χ ψ = gaussSum χ ψ * HMul.hMul (β := R') (gaussSum χ ψ⁻¹) ((χ : (a : R) → R') (-1) : R')
Tactic: rw [pow_two, ← gaussSum_mul_gaussSum_eq_card hχ₁ hψ, hχ₂.inv, mul_rotate']
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
⊢ gaussSum χ ψ * gaussSum χ ψ = gaussSum χ ψ * HMul.hMul (β := R') (gaussSum χ ψ⁻¹) ((χ : (a : R) → R') (-1) : R')
have e_a : gaussSum χ ψ = HMul.hMul (β := R') (gaussSum χ ψ⁻¹) ((χ : (a : R) → R') (-1) : R')
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : IsPrimitive.{u, v} (R := R) (R' := R') ψ
⊢ gaussSum χ ψ = HMul.hMul (β := R') (gaussSum χ ψ⁻¹) ((χ : (a : R) → R') (-1) : R')
have e_a : HMul.hMul (α := R') ((χ : (a : R) → R') (↑(-1) : R) : R') (gaussSum χ (ψ.mulShift (↑(-1) : R))) =
  HMul.hMul (α := R') ((χ : (a : R) → R') (-1) : R') (gaussSum χ (ψ.mulShift (-1)))
Tactic: rw [mul_comm, ← gaussSum_mulShift _ _ (-1 : Rˣ), inv_mulShift]
-- 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
χ : MulChar R R'
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p = gaussSum (χ ^ p) (ψ ^ p)
have rw : Eq.{v + 1} (α := R')
  (∑ x : R,
    (frobenius R' p : (a : R') → R')
      (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') x : R')))
  (∑ a : R, HMul.hMul (α := R') (β := R') ((χ ^ p : (a : R) → R') a : R') ((ψ ^ p : (a : R) → R') a : R'))
Tactic: rw [← frobenius_def, gaussSum, gaussSum, map_sum]
-- 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
χ : MulChar R R'
ψ : AddChar R R'
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      (frobenius R' p : (a : R') → R')
        (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') x : R')))
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ ^ p : (a : R) → R') a : R') ((ψ ^ p : (a : R) → R') a : R'))
have simp_rw : Eq.{v + 1} (α := R')
  (∑ x : R, HPow.hPow (α := R') ((χ : (a : R) → R') x : R') p * HPow.hPow (α := R') ((ψ : (a : R) → R') x : R') p)
  (∑ x : R, HMul.hMul (β := R') (HPow.hPow (α := R') ((χ : (a : R) → R') x : R') p) ((ψ ^ p : (a : R) → R') x : R'))
Tactic: simp_rw [pow_apply' χ fp.1.ne_zero, map_mul, frobenius_def]
-- 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 χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
have rw : gaussSum (χ ^ p) (ψ ^ p) = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
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 χ ψ)
⊢ gaussSum χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
have rw₁ : gaussSum (χ ^ p) (ψ.mulShift (↑p : R)) = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
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 χ ψ)
⊢ gaussSum χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
have rw₂ : gaussSum χ (ψ.mulShift (↑p : R)) = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
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 χ ψ)
⊢ gaussSum χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
have 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))))
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))))
⊢ gaussSum χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
have 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))
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))
⊢ gaussSum χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
have 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))
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))
⊢ gaussSum χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
have rw₆ : gaussSum χ (ψ.mulShift (↑p : R)) =
  HPow.hPow (α := R') (β := ℕ) ((χ : (a : R) → R') (↑p : R) : R') 2 * gaussSum χ (ψ.mulShift (↑p : 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))
⊢ gaussSum χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
have rw₇ : gaussSum χ (ψ.mulShift (↑p : R)) =
  HMul.hMul (α := R') ((HPow.hPow (β := ℕ) χ 2 : (a : R) → R') (↑p : R) : R') (gaussSum χ (ψ.mulShift (↑p : 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)))
⊢ gaussSum χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
have rw₈ : gaussSum χ (ψ.mulShift (↑p : R)) =
  HMul.hMul (α := R') ((1 : (a : R) → R') (↑p : R) : R') (gaussSum χ (ψ.mulShift (↑p : 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)))
⊢ gaussSum χ ψ ^ p = HMul.hMul (α := R') ((χ : (a : R) → R') (↑p : R) : R') (gaussSum χ ψ)
have rw₉ : gaussSum χ (ψ.mulShift (↑hp.unit : R)) =
  HMul.hMul (α := R') ((1 : (a : R) → R') (↑hp.unit : R) : 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]