-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : Field F
inst_1 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
rw :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ t : F,
      ∑ x : F,
        HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R))
          ((ψ : (a : F) → R) t : R)
rw₁ rw₂ rw₃ :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    HAdd.hAdd (α := R)
      (∑ x ∈ univ \ {0},
        ∑ x_1 : F,
          HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x_1 : R) ((φ : (a : F) → R) (x - x_1) : R))
            ((ψ : (a : F) → R) x : R))
      (∑ x : F,
        HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (0 - x) : R))
          ((ψ : (a : F) → R) 0 : R))
rw₄ :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    HAdd.hAdd (α := R)
      (∑ x ∈ univ \ {0},
        ∑ x_1 : F,
          HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x_1 : R) ((φ : (a : F) → R) (x - x_1) : R))
            ((ψ : (a : F) → R) x : R))
      (∑ x : F, HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) (-1) : R) ((χ * φ : (a : F) → R) x : R))
rw₅ :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      ∑ x_1 : F,
        HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x_1 : R) ((φ : (a : F) → R) (x - x_1) : R))
          ((ψ : (a : F) → R) x : R)
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ
have rw₆ : ∀
  (sum_eq :
    ∀ (t : F),
      Membership.mem (γ := Finset F) (univ \ {0}) t →
        HMul.hMul (α := R) (β := R)
            (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R) : R)
            ((ψ : (a : F) → R) t : R) =
          HMul.hMul (α := R) (β := R)
            (∑ y : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (t * y) : R) ((φ : (a : F) → R) (t - t * y) : R) :
              R)
            ((ψ : (a : F) → R) t : R)),
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      ∑ x_1 : F,
        HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x_1 : R) ((φ : (a : F) → R) (x - x_1) : R))
          ((ψ : (a : F) → R) x : R)
Tactic: classical
  rw [gaussSum_mul _ _ ψ, sum_eq_sum_diff_singleton_add (mem_univ (0 : F))]
  conv =>
    enter [2, 2, 2, x]
    rw [zero_sub, neg_eq_neg_one_mul x, map_mul, mul_left_comm (χ x) (φ (-1)),
      ← MulChar.mul_apply, ψ.map_zero_eq_one, mul_one]
  rw [← mul_sum _ _ (φ (-1)), MulChar.sum_eq_zero_of_ne_one h, mul_zero, add_zero]
  have sum_eq : ∀ t ∈ univ \ {0}, (∑ x : F, χ x * φ (t - x)) * ψ t =
      (∑ y : F, χ (t * y) * φ (t - (t * y))) * ψ t := by
    intro t ht
    simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at ht
    exact congrArg (· * ψ t) (Equiv.sum_comp (Equiv.mulLeft₀ t ht) _).symm
  simp_rw [← sum_mul, sum_congr rfl sum_eq, ← mul_one_sub, map_mul, mul_assoc]
  conv => enter [2, 2, t, 1, 2, x, 2]; rw [← mul_assoc, mul_comm (χ x) (φ t)]
  simp_rw [← mul_assoc, ← MulChar.mul_apply, mul_assoc, ← mul_sum, mul_right_comm]
  rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_diff_singleton_add (mem_univ (0 : F)),
    (χ * φ).map_zero, zero_mul, add_zero]