@[simp]

theorem composite_model_objective_comp_apply {X : Type u} {Y : Type v} [AddCommMonoid X] [Module ℝ X] [AddCommMonoid Y] [Module ℝ Y] (f₁ : X → EReal) (f₂ : Y → EReal) (A : X →ₗ[ℝ] Y) (x : X) : composite_model_objective f₁ (f₂ ∘ ⇑A) x = f₁ x + f₂ (A x)

Evaluating the Chapter 10 composite owner at the linear-composite specialization recovers the textbook formula f₁(x) + f₂(Ax).