∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [SecondCountableTopology F] (f : E → F) (s : Set E)
  (f' : E → E →L[ℝ] F),
  (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
    ∀ (r : (E →L[ℝ] F) → NNReal),
      (∀ (A : E →L[ℝ] F), r A ≠ 0) →
        ∃ t A,
          (∀ (n : ℕ), IsClosed (t n)) ∧
            s ⊆ ⋃ n, t n ∧
              (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧
                (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)