Lean: linarith over inner products needs real_inner_comm facts as extra hypotheses

When hypotheses mention both ⟪x, y⟫_ℝ and ⟪y, x⟫_ℝ (typical after fderiv_inner_apply product rules, e.g. ∂ᵤ⟪Xᵤ,Xᵤ⟫ = ⟪Xᵤᵤ,Xᵤ⟫ + ⟪Xᵤ,Xᵤᵤ⟫), linarith treats the two orders as unrelated atoms and fails. Rewriting with rw [real_inner_comm ..] at h is fragile (the pattern often isn't where you think). Instead pass the symmetry facts as terms: linarith [real_inner_comm (du X p) (du (du X) p), real_inner_comm (dv X p) (dv (du X) p)]; each one is a linear equation between the two atoms, and linarith closes the goal. A related gotcha: simp only with no lemmas (simp only at h ⊢) is sometimes needed just to beta-reduce (fun r ↦ ...) p after rw [du_comp]; deleting it because the linter says an argument is unused can break the proof.