awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
z : (↑s : Type u_1)
zT : z ∈ T
hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
ε : ℝ
εpos : 0 < ε
hε : ‖f' x - f' (↑z : E)‖ + ε ≤ (↑(r (f' (↑z : E))) : ℝ)
δ : ℝ
δpos : 0 < δ
hδ : ball x δ ∩ s ⊆ {y : E | ‖HSub.hSub (β := F) (f y - f x) ((f' x : (a : E) → F) (y - x) : F)‖ ≤ ε * ‖y - x‖}
n : ℕ
hn : u n < δ
y : E
hy : y ∈ s ∩ ball x (u n)
rw : y ∈ s ∩ ball x δ
⊢ y ∈ ball x δ ∩ s

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
z : (↑s : Type u_1)
zT : z ∈ T
hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
ε : ℝ
εpos : 0 < ε
hε : ‖f' x - f' (↑z : E)‖ + ε ≤ (↑(r (f' (↑z : E))) : ℝ)
δ : ℝ
δpos : 0 < δ
hδ : ball x δ ∩ s ⊆ {y : E | ‖HSub.hSub (β := F) (f y - f x) ((f' x : (a : E) → F) (y - x) : F)‖ ≤ ε * ‖y - x‖}
n : ℕ
hn : u n < δ
y : E
hy : y ∈ s ∩ ball x (u n)
⊢ y ∈ s ∩ ball x δ

Tactic:
inter_subset_inter_right _ (ball_subset_ball hn.le) hy

Premises used: Set.inter_subset_inter_right, LT.lt.le, Metric.ball_subset_ball
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
z : (↑s : Type u_1)
zT : z ∈ T
hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
ε : ℝ
εpos : 0 < ε
hε : ‖f' x - f' (↑z : E)‖ + ε ≤ (↑(r (f' (↑z : E))) : ℝ)
δ : ℝ
δpos : 0 < δ
hδ : ball x δ ∩ s ⊆ {y : E | ‖HSub.hSub (β := F) (f y - f x) ((f' x : (a : E) → F) (y - x) : F)‖ ≤ ε * ‖y - x‖}
n : ℕ
hn : u n < δ
y : E
hy : y ∈ s ∩ ball x (u n)
⊢ y ∈ s ∩ ball x δ

Tactic:
exact inter_subset_inter_right _ (ball_subset_ball hn.le) hy

Premises used: Set.inter_subset_inter_right, LT.lt.le, Metric.ball_subset_ball
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
z : (↑s : Type u_1)
zT : z ∈ T
hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
ε : ℝ
εpos : 0 < ε
hε : ‖f' x - f' (↑z : E)‖ + ε ≤ (↑(r (f' (↑z : E))) : ℝ)
δ : ℝ
δpos : 0 < δ
hδ : ball x δ ∩ s ⊆ {y : E | ‖HSub.hSub (β := F) (f y - f x) ((f' x : (a : E) → F) (y - x) : F)‖ ≤ ε * ‖y - x‖}
n : ℕ
hn : u n < δ
y : E
hy : y ∈ s ∩ ball x (u n)
rw : (‖f' x - f' (↑z : E)‖ + ε) * ‖y - x‖ ≤ (↑(r (f' (↑z : E))) : ℝ) * ‖y - x‖
⊢ ε * ‖y - x‖ + ‖f' x - f' (↑z : E)‖ * ‖y - x‖ ≤ (↑(r (f' (↑z : E))) : ℝ) * ‖y - x‖

Tactic:
rw [← add_mul, add_comm]

Premises used: add_mul, add_comm
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
z : (↑s : Type u_1)
zT : z ∈ T
hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
ε : ℝ
εpos : 0 < ε
hε : ‖f' x - f' (↑z : E)‖ + ε ≤ (↑(r (f' (↑z : E))) : ℝ)
δ : ℝ
δpos : 0 < δ
hδ : ball x δ ∩ s ⊆ {y : E | ‖HSub.hSub (β := F) (f y - f x) ((f' x : (a : E) → F) (y - x) : F)‖ ≤ ε * ‖y - x‖}
n : ℕ
hn : u n < δ
y : E
hy : y ∈ s ∩ ball x (u n)
ha : 0 ≤ ‖y - x‖
⊢ (‖f' x - f' (↑z : E)‖ + ε) * ‖y - x‖ ≤ (↑(r (f' (↑z : E))) : ℝ) * ‖y - x‖

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
x : E
xs : x ∈ s
z : (↑s : Type u_1)
zT : z ∈ T
hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
ε : ℝ
εpos : 0 < ε
hε : ‖f' x - f' (↑z : E)‖ + ε ≤ (↑(r (f' (↑z : E))) : ℝ)
δ : ℝ
δpos : 0 < δ
hδ : ball x δ ∩ s ⊆ {y : E | ‖HSub.hSub (β := F) (f y - f x) ((f' x : (a : E) → F) (y - x) : F)‖ ≤ ε * ‖y - x‖}
n : ℕ
hn : u n < δ
y : E
hy : y ∈ s ∩ ball x (u n)
y₁ :
  ‖HSub.hSub (β := F) (f y - f x) ((f' (↑z : E) : (a : E) → F) (y - x) : F)‖ =
    ‖HAdd.hAdd (β := F) (HSub.hSub (β := F) (f y - f x) ((f' x : (a : E) → F) (y - x) : F))
        ((f' x - f' (↑z : E) : (a : E) → F) (y - x) : F)‖
y₂ :
  ‖HSub.hSub (β := F) (f y - f x) ((f' x : (a : E) → F) (y - x) : F)‖ +
      norm.{u_2} (E := F) ((f' x - f' (↑z : E) : (a : E) → F) (y - x) : F) ≤
    ε * ‖y - x‖ + ‖f' x - f' (↑z : E)‖ * ‖y - x‖
y₃ : ε * ‖y - x‖ + ‖f' x - f' (↑z : E)‖ * ‖y - x‖ ≤ (↑(r (f' (↑z : E))) : ℝ) * ‖y - x‖
⊢ ‖HSub.hSub (β := F) (f y - f x)
        ((f' (↑(↑(Subtype.mk (p := fun (x : (↑s : Type u_1)) ↦ x ∈ T) z zT) : (↑s : Type u_1)) : E) : (a : E) → F)
            (y - x) :
          F)‖ ≤
    (↑(r (f' (↑(↑(Subtype.mk (p := fun (x : (↑s : Type u_1)) ↦ x ∈ T) z zT) : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖

Tactic:
calc
      ‖f y - f x - (f' z) (y - x)‖ = ‖f y - f x - (f' x) (y - x) + (f' x - f' z) (y - x)‖ := by
        congr 1
        simp only [ContinuousLinearMap.coe_sub', map_sub, Pi.sub_apply]
        abel
      _ ≤ ‖f y - f x - (f' x) (y - x)‖ + ‖(f' x - f' z) (y - x)‖ := norm_add_le _ _
      _ ≤ ε * ‖y - x‖ + ‖f' x - f' z‖ * ‖y - x‖ := by
        refine add_le_add (hδ ?_) (ContinuousLinearMap.le_opNorm _ _)
        rw [inter_comm]
        exact inter_subset_inter_right _ (ball_subset_ball hn.le) hy
      _ ≤ r (f' z) * ‖y - x‖ := by
        rw [← add_mul, add_comm]
        gcongr

Premises used: HSub.hSub, norm_add_le, Subtype.val, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
⊢ ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z

Tactic:
have s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : T), x ∈ M n z := by
    intro x xs
    obtain ⟨z, zT, hz⟩ : ∃ z ∈ T, f' x ∈ ball (f' (z : E)) (r (f' z)) := by
      have : f' x ∈ ⋃ z ∈ T, ball (f' (z : E)) (r (f' z)) := by
        rw [hT]
        refine mem_iUnion.2 ⟨⟨x, xs⟩, ?_⟩
        simpa only [mem_ball, Subtype.coe_mk, dist_self] using (rpos (f' x)).bot_lt
      rwa [mem_iUnion₂, bex_def] at this
    obtain ⟨ε, εpos, hε⟩ : ∃ ε : ℝ, 0 < ε ∧ ‖f' x - f' z‖ + ε ≤ r (f' z) := by
      refine ⟨r (f' z) - ‖f' x - f' z‖, ?_, le_of_eq (by abel)⟩
      simpa only [sub_pos] using mem_ball_iff_norm.mp hz
    obtain ⟨δ, δpos, hδ⟩ :
      ∃ (δ : ℝ), 0 < δ ∧ ball x δ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖} :=
      Metric.mem_nhdsWithin_iff.1 ((hf' x xs).isLittleO.def εpos)
    obtain ⟨n, hn⟩ : ∃ n, u n < δ := ((tendsto_order.1 u_lim).2 _ δpos).exists
    refine ⟨n, ⟨z, zT⟩, ⟨xs, ?_⟩⟩
    intro y hy
    calc
      ‖f y - f x - (f' z) (y - x)‖ = ‖f y - f x - (f' x) (y - x) + (f' x - f' z) (y - x)‖ := by
        congr 1
        simp only [ContinuousLinearMap.coe_sub', map_sub, Pi.sub_apply]
        abel
      _ ≤ ‖f y - f x - (f' x) (y - x)‖ + ‖(f' x - f' z) (y - x)‖ := norm_add_le _ _
      _ ≤ ε * ‖y - x‖ + ‖f' x - f' z‖ * ‖y - x‖ := by
        refine add_le_add (hδ ?_) (ContinuousLinearMap.le_opNorm _ _)
        rw [inter_comm]
        exact inter_subset_inter_right _ (ball_subset_ball hn.le) hy
      _ ≤ r (f' z) * ‖y - x‖ := by
        rw [← add_mul, add_comm]
        gcongr
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
n : ℕ
z : (↑T : Type u_1)
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)
⊢ x ∈ M n z

Tactic:
⟨xs, fun y hy => ?_⟩

Premises used: Set.Mem, setOf, And.intro
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
n : ℕ
z : (↑T : Type u_1)
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)
refine :
  ∀ (y : E) (hy : y ∈ s ∩ ball x (u n)),
    ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
      (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖
⊢ x ∈ M n z

Tactic:
refine ⟨xs, fun y hy => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
n : ℕ
z : (↑T : Type u_1)
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)
y : E
hy : y ∈ s ∩ ball x (u n)
⊢ ∃ (a : ℕ → E), (∀ (k : ℕ), a k ∈ M n z) ∧ Tendsto a atTop (𝓝 x)

Tactic:
mem_closure_iff_seq_limit.1 hx

Premises used: mem_closure_iff_seq_limit, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
n : ℕ
z : (↑T : Type u_1)
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)
y : E
hy : y ∈ s ∩ ball x (u n)
obtain :
  ∀ (a : ℕ → E) (aM : ∀ (k : ℕ), a k ∈ M n z) (a_lim : Tendsto a atTop (𝓝 x)),
    ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
      (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖
⊢ ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
    (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖

Tactic:
obtain ⟨a, aM, a_lim⟩ : ∃ a : ℕ → E, (∀ k, a k ∈ M n z) ∧ Tendsto a atTop (𝓝 x) :=
      mem_closure_iff_seq_limit.1 hx

Premises used: mem_closure_iff_seq_limit, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
n : ℕ
z : (↑T : Type u_1)
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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)
h :
  Tendsto
    (fun (x : ℕ) ↦ HSub.hSub (β := F) (f y - f (a x)) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - a x) : F))
    atTop (𝓝 (HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)))
⊢ Tendsto
    (fun (k : ℕ) ↦
      ‖HSub.hSub (β := F) (f y - f (a k)) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - a k) : F)‖)
    atTop (𝓝 ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖)

Tactic:
apply Tendsto.norm

Premises used: Filter.Tendsto.norm
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
n : ℕ
z : (↑T : Type u_1)
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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)
apply : Tendsto a atTop (𝓝[s] x)
⊢ Tendsto (fun (k : ℕ) ↦ f (a k)) atTop (𝓝 (f x))

Tactic:
apply (hf' x xs).continuousWithinAt.tendsto.comp

Premises used: HasFDerivWithinAt.continuousWithinAt, Filter.Tendsto.comp, ContinuousWithinAt.tendsto
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : 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 : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x) : F)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
n : ℕ
z : (↑T : Type u_1)
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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)
apply : ∀ᶠ (x : ℕ) in atTop, a x ∈ s
⊢ Tendsto a atTop (𝓝[s] x)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ a_lim

Premises used: tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within