-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
ι : Type u_2
inst : Fintype ι
hb : 0 < b.re
c : ι → ℂ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-(b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (HAdd.hAdd (α := ℂ) (-∑ i : ι, b * HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2) (∑ i : ι, c i * (↑(v i) : ℂ)))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₂ :
  ∏ i : ι, ((↑π : ℂ) / b) ^ (1 / 2) * cexp (HPow.hPow (β := ℕ) (c i) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₃ :
  ∏ x : ι, HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹ * cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₄ :
  HMul.hMul (α := ℂ) (∏ x : ι, HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹)
      (∏ x : ι, cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₅ :
  HPow.hPow (β := ℂ) ((↑π : ℂ) / b) 2⁻¹ ^ Finset.card.{u_2} (α := ι) Finset.univ *
      ∏ x : ι, cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₆ :
  ((↑π : ℂ) / b) ^ HMul.hMul (α := ℂ) (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℂ) 2⁻¹ *
      ∏ x : ι, cexp (HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₇ :
  ((↑π : ℂ) / b) ^ HMul.hMul (α := ℂ) (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℂ) 2⁻¹ *
      cexp (∑ x : ι, HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
simp_rw₈ :
  ((↑π : ℂ) / b) ^ HMul.hMul (α := ℂ) (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℂ) 2⁻¹ *
      cexp (∑ x : ι, HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ι → ℝ) ↦
      cexp (-b * ∑ i : ι, HPow.hPow (β := ℕ) (↑(v i) : ℂ) 2 + ∑ i : ι, c i * (↑(v i) : ℂ))) =
    ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Fintype.card ι) : ℂ) 2 *
      cexp ((∑ i : ι, HPow.hPow (β := ℕ) (c i) 2) / (4 * b))
have simp_rw₉ : ((↑π : ℂ) / b) ^ HMul.hMul (α := ℂ) (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℂ) 2⁻¹ *
    cexp (∑ x : ι, HPow.hPow (β := ℕ) (c x) 2 / (4 * b)) =
  ((↑π : ℂ) / b) ^ HDiv.hDiv (α := ℂ) (↑(Finset.card.{u_2} (α := ι) Finset.univ) : ℂ) 2 *
    cexp (∑ i : ι, HPow.hPow (β := ℕ) (c i) 2 / (4 * b))
Tactic: simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c, one_div,
    Finset.prod_mul_distrib, Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum, Fintype.card,
    Finset.sum_div, div_eq_mul_inv]