Bilin Form Integrand mul smooth eq

theorem bilinFormIntegrand_mul_smooth_eq    {Ω : Set E} (hΩ : IsOpen Ω)    {u w η : E → ℝ}    (A : EllipticCoeff d Ω)    (hu : MemW1pWitness 2 u Ω)    (hw : MemW1pWitness 2 w Ω)    (hη : ContDiff ℝ (⊤ : ℕ∞) η)    {C₀ C₁ : ℝ} (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁)    (hη_bound : ∀ x, |η x| ≤ C₀)    (hη_grad_bound : ∀ x, ‖fderiv ℝ η x‖ ≤ C₁)    (hp : (1 : ENNReal) ≤ 2) :    ∀ x, bilinFormIntegrandOfCoeff A hu        (hw.mul_smooth_bounded_p (d := d) hp hΩ hη hC₀ hC₁ hη_bound hη_grad_bound) x =      η x * bilinFormIntegrandOfCoeff A hu hw x +      w x * ⟪matMulE (A.a x) (hu.weakGrad x),        (WithLp.toLp 2 fun i =>          (fderiv ℝ η x) (EuclideanSpace.single i 1) : E)⟫_ℝ := by  intro x  -- The weakGrad of mul_smooth_bounded_p at x is:  --   η x • hw.weakGrad x + toLp 2 (fun i => fderiv ℝ η x (single i 1) * w x)  -- The bilinear-form integrand ⟪A∇u, ∇(η·w)⟫ distributes over this sum  -- by bilinearity of the inner product.  simp only [bilinFormIntegrandOfCoeff, MemW1pWitness.mul_smooth_bounded_p,    inner_add_right, inner_smul_right]  congr 1  -- Factor w(x) out: ⟪v, toLp(f_i * c)⟫ = c * ⟪v, toLp(f_i)⟫  -- The goal is: Σᵢ ⟪row_i, f_i * w⟫ = (Σᵢ ⟪row_i, f_i⟫) * w  -- where ⟪a, b⟫_ℝ = a * b, so ⟪a, f_i * w⟫ = a * (f_i * w) = (a * f_i) * w = ⟪a, f_i⟫ * w  simp only [PiLp.inner_apply, matMulE, Matrix.mulVec]  rw [Finset.mul_sum]  congr 1  ext i  -- ⟪a, b * c⟫_ℝ = c * ⟪a, b⟫_ℝ for reals  rw [show (fderiv ℝ η x) (EuclideanSpace.single i 1) * w x =      w x • ((fderiv ℝ η x) (EuclideanSpace.single i 1)) from by rw [smul_eq_mul]; ring,    inner_smul_right]