-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt [SecondCountableTopology F]
    (f : E → F) (s : Set E) (f' : E → E →L[ℝ] F) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
    (r : (E →L[ℝ] F) → ℝ≥0) (rpos : ∀ A, r A ≠ 0) :
    ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
      (∀ 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)

Proof state:
case intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z => {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
n : ℕ
z : ↑T
x : E
xs : x ∈ s
hx : x ∈ closure (M n z)
y : E
hy : y ∈ s ∩ ball x (u n)
a : ℕ → E
aM : ∀ (k : ℕ), a k ∈ M n z
a_lim : Tendsto a atTop (𝓝 x)
L1 : Tendsto (fun k => ‖f y - f (a k) - (f' ↑↑z) (y - a k)‖) atTop (𝓝 ‖f y - f x - (f' ↑↑z) (y - x)‖)
⊢ ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖

Tactic:
have L2 : Tendsto (fun k : ℕ => (r (f' z) : ℝ) * ‖y - a k‖) atTop (𝓝 (r (f' z) * ‖y - x‖)) :=
  (tendsto_const_nhds.sub a_lim).norm.const_mul _

Result:
case intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z => {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
n : ℕ
z : ↑T
x : E
xs : x ∈ s
hx : x ∈ closure (M n z)
y : E
hy : y ∈ s ∩ ball x (u n)
a : ℕ → E
aM : ∀ (k : ℕ), a k ∈ M n z
a_lim : Tendsto a atTop (𝓝 x)
L1 : Tendsto (fun k => ‖f y - f (a k) - (f' ↑↑z) (y - a k)‖) atTop (𝓝 ‖f y - f x - (f' ↑↑z) (y - x)‖)
L2 : Tendsto (fun k => ↑(r (f' ↑↑z)) * ‖y - a k‖) atTop (𝓝 (↑(r (f' ↑↑z)) * ‖y - x‖))
⊢ ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖

Proof state:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F✝ : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : SecondCountableTopology F✝
f : E → F✝
s : Set E
f' : E → E →L[ℝ] F✝
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F✝) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z => {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E := fun n z p => closure (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed (K n z p)
F : ℕ → ℕ × ↑T × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : ↑T
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
q : ℕ
hq : F q = (n, z, p)
⊢ x ∈ ⋃ n, (fun q => K (F q).1 (F q).2.1 (F q).2.2) n

Tactic:
apply mem_iUnion.2 ⟨q, _⟩

Result:
E : Type u_1
F✝ : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : SecondCountableTopology F✝
f : E → F✝
s : Set E
f' : E → E →L[ℝ] F✝
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F✝) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z => {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E := fun n z p => closure (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed (K n z p)
F : ℕ → ℕ × ↑T × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : ↑T
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
q : ℕ
hq : F q = (n, z, p)
⊢ x ∈ K (F q).1 (F q).2.1 (F q).2.2

Proof state:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z => {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E := fun n z p => closure (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed (K n z p)
this✝ : Encodable ↑T
this : Nonempty ↑T
⊢ ∃ F, Function.Surjective F

Tactic:
inhabit ↥T

Result:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z => {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E := fun n z p => closure (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed (K n z p)
this✝ : Encodable ↑T
this : Nonempty ↑T
inhabited_h : Inhabited ↑T
⊢ ∃ F, Function.Surjective F