-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem exists_partition_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),
      Pairwise (Disjoint on t) ∧
        (∀ n, MeasurableSet (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.intro.intro.refine_2
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
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
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed (t n)
st : s ⊆ ⋃ n, t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
n : ℕ
⊢ ApproximatesLinearOn f (A n) (s ∩ disjointed t n) (r (A n))

Tactic:
exact (t_approx n).mono_set (inter_subset_inter_right _ (disjointed_subset _ _))

Result:
no goals

Proof state:
case 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✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
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
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed (t n)
st : s ⊆ ⋃ n, t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ ∃ t A,
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (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)

Tactic:
refine
  ⟨disjointed t, A, disjoint_disjointed _,
    MeasurableSet.disjointed fun n => (t_closed n).measurableSet, ?_, ?_, ht⟩

Result:
case intro.intro.intro.intro.intro.refine_1
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
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
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed (t n)
st : s ⊆ ⋃ n, t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ s ⊆ ⋃ n, disjointed t n

case intro.intro.intro.intro.intro.refine_2
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
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
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed (t n)
st : s ⊆ ⋃ n, t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ disjointed t n) (r (A n))

Proof state:
case intro.intro.intro.intro.intro.refine_2
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
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
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed (t n)
st : s ⊆ ⋃ n, t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ disjointed t n) (r (A n))

Tactic:
intro n

Result:
case intro.intro.intro.intro.intro.refine_2
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
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
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed (t n)
st : s ⊆ ⋃ n, t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
n : ℕ
⊢ ApproximatesLinearOn f (A n) (s ∩ disjointed t n) (r (A n))

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✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
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
⊢ ∃ t A,
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (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)

Tactic:
rcases exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' r rpos with
  ⟨t, A, t_closed, st, t_approx, ht⟩

Result:
case 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✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
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
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed (t n)
st : s ⊆ ⋃ n, t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ ∃ t A,
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (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)