-- Module: Mathlib.NumberTheory.GaussSum
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 χ ψ)
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 χ ψ
succ₈ :
  HMul.hMul (α := R') (β := R') ((χ ^ p : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R')
        ((χ : (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 χ ψ
succ₉ succ₁₀ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (HPow.hPow (α := R) (↑p : R) n) : R')
        ((χ : (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 χ ψ
⊢ gaussSum χ ψ ^ p ^ (n + 1) =
    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]

Premises used: pow_succ, mul_assoc, MulChar.IsQuadratic.pow_char, MulChar.pow_apply', Nat.cast, pow_mul, map_mul, HPow.hPow, Nat.Prime.ne_zero, MulChar.IsQuadratic.gaussSum_frob, mul_pow, Fact.out