-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
h : u ∈ t.powerset
simp_rw :
  Eq (α := ℂ)
    (𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
    (𝔼 i : G,
      HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)))
        ((HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) i : ℂ))
simp_rw₁ :
  Eq (α := ℂ)
    (𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
    (𝔼 i : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
        HMul.hMul (α := ℂ) (β := ℂ) ((∑ ψ ∈ u, ψ : (a : G) → ℂ) i : ℂ) ((∑ ψ ∈ t \ u, ψ : (a : G) → ℂ) (-i) : ℂ))
simp_rw₂ :
  Eq (α := ℂ)
    (𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
    (𝔼 i : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
        HMul.hMul (α := ℂ) (∏ i_1 ∈ u, (i_1 : (a : G) → ℂ) i) (∏ i_1 ∈ t \ u, (i_1 : (a : G) → ℂ) (-i)))
simp_rw₃ :
  Eq (α := ℂ)
    (𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
    (𝔼 i : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ i_1 ∈ u, (i_1 : (a : G) → ℂ) i) *
        HMul.hMul (α := ℂ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) (∏ i_1 ∈ t \ u, (i_1 : (a : G) → ℂ) (-i)))
⊢ 𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)) =
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
      𝔼 a : G, (HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) a
have simp_rw₄ : Eq (α := ℂ)
  (𝔼 a : G,
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
      (∏ ψ ∈ t \ u,
        HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
  (𝔼 i : G,
    HMul.hMul (α := ℂ) (∏ x ∈ u, HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ))
      (∏ x ∈ t \ u, HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d x) : ℂ) ((x : (a : G) → ℂ) (-i) : ℂ)))
Tactic: simp_rw [mul_expect, AddChar.sub_apply, AddChar.sum_apply, mul_mul_mul_comm,
          ← prod_mul_distrib, AddChar.map_neg_eq_conj]