-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A
x x_1 x_2 : f.PreGNS
rw :
  (f : (a : A) → ℂ)
      (HMul.hMul (β := A)
        (star
          (HAdd.hAdd (α := A) (β := A) ((f.ofPreGNS : (a : f.PreGNS) → A) x : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_1 : A)))
        ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
    HAdd.hAdd (α := ℂ) (β := ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
rw₁ :
  (f : (a : A) → ℂ)
      (HMul.hMul (β := A)
        (HAdd.hAdd (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
          (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A))
        ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
    HAdd.hAdd (α := ℂ) (β := ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
rw₂ :
  (f : (a : A) → ℂ)
      (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
          ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A) +
        HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
          ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
    HAdd.hAdd (α := ℂ) (β := ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
rw₃ rw₄ :
  HAdd.hAdd (α := ℂ) (β := ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
⊢ (f : (a : A) → ℂ)
      (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) (x + x_1)) : A)
        ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) =
    HAdd.hAdd (α := ℂ) (β := ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)
      ((f : (a : A) → ℂ)
          (HMul.hMul (α := A) (β := A) (star ((f.ofPreGNS : (a : f.PreGNS) → A) x_1) : A)
            ((f.ofPreGNS : (a : f.PreGNS) → A) x_2 : A)) :
        ℂ)

Tactic:
rw [map_add, star_add, add_mul, map_add]

Premises used: add_mul, StarAddMonoid.star_add, map_add