-- 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)
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)
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},
        HMul.hMul (α := R) (β := R)
          (∑ x_1 : F,
              HMul.hMul (α := R) ((χ : (a : F) → R) x : R)
                (HMul.hMul (α := R) ((χ : (a : F) → R) x_1 : R)
                  (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) x : R) ((φ : (a : F) → R) (1 - x_1) : R))) :
            R)
          ((ψ : (a : F) → R) x : R)
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 χ φ =
      ∑ t ∈ univ \ {0},
        HMul.hMul (α := R) (β := R)
          (∑ x : F,
              HMul.hMul (α := R) ((χ : (a : F) → R) t : R)
                (HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) t : R) ((χ : (a : F) → R) x : R))
                  ((φ : (a : F) → R) (1 - x) : R)) :
            R)
          ((ψ : (a : F) → R) t : 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},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) *
        ∑ i : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) i : R) ((φ : (a : F) → R) (1 - i) : 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]