Expanding products of character sums in Lean: use rw, not simp, to keep summation order

To prove (Σ_x Σ_y ψ(t x y)) * (Σ_z ψ(t z)) * (Σ_s ψ(-t s)) = Σ_{p ∈ X ×ˢ Y ×ˢ Z ×ˢ S} ψ(t(xy+z-s)), simp only [sum_mul, mul_sum, sum_product] scrambles which bound variable goes with which set, because it rewrites bottom-up and both sum_mul and mul_sum fire. Instead go one level at a time: rw [sum_product, mul_assoc, sum_mul]; refine sum_congr rfl fun x _ ↦ ?_; rw [sum_product, fc, sum_mul]; ...; rw [sum_product, fc, fc, sum_mul_sum, mul_sum] etc., then rw [← AddChar.map_add_eq_mul] and congrArg ψ (by ring). Other gotchas from the same proof: (Equiv.mulLeft₀ t ht).sum_comp f resolves to Equiv.Perm.sum_comp (needs a Finset), so write Equiv.sum_comp (Equiv.mulLeft₀ t ht) f. Also, in a statement min (card F * #A / 2) ... is computed in ℕ unless you ascribe (… : ℝ) inside the min. Garaev's F_p sum-product then follows from orthogonality (AddChar.sum_mulShift with ZMod.isPrimitive_stdAddChar).