∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {φ : E → ℝ} {x₀ : E}
  {φ' : StrongDual ℝ E} {ι : Type u_3} [inst_3 : Fintype ι] {f : ι → E → ℝ} {f' : ι → StrongDual ℝ E},
  IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀ →
    (∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀) →
      HasStrictFDerivAt φ φ' x₀ → ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i, Λ i • f' i + Λ₀ • φ' = 0