awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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)
L : Tendsto (fun (k : ℕ) ↦ f (a k)) atTop (𝓝 (f x))
⊢ 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)))
have h : Tendsto.{0, u_2} (β := F) (fun (x : ℕ) ↦ ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - a x) : F)) atTop
  (𝓝 ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - x)) : Filter F)
Tactic: apply Tendsto.sub (tendsto_const_nhds.sub L)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
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)
⊢ ‖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‖
have L1 : 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: have L1 :
      Tendsto (fun k : ℕ => ‖f y - f (a k) - (f' z) (y - a k)‖) atTop
        (𝓝 ‖f y - f x - (f' z) (y - x)‖) := by
      apply Tendsto.norm
      have L : Tendsto (fun k => f (a k)) atTop (𝓝 (f x)) := by
        apply (hf' x xs).continuousWithinAt.tendsto.comp
        apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ a_lim
        exact Eventually.of_forall fun k => (aM k).1
      apply Tendsto.sub (tendsto_const_nhds.sub L)
      exact ((f' z).continuous.tendsto _).comp (tendsto_const_nhds.sub a_lim)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
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)
L1 :
  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)‖)
⊢ ‖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‖
have L2 : Tendsto (fun (k : ℕ) ↦ (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - a k‖) atTop
  (𝓝 ((↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖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 _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
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)
L1 :
  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)‖)
L2 :
  Tendsto (fun (k : ℕ) ↦ (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - a k‖) atTop
    (𝓝 ((↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖))
⊢ ∀ᶠ (k : ℕ) in atTop,
    ‖HSub.hSub (β := F) (f y - f (a k)) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - a k) : F)‖ ≤
      (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - a k‖
have L : Tendsto (fun (k : ℕ) ↦ dist y (a k)) atTop (𝓝 (dist y x))
Tactic: have L : Tendsto (fun k => dist y (a k)) atTop (𝓝 (dist y x)) :=
        tendsto_const_nhds.dist a_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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)
L1 :
  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)‖)
L2 :
  Tendsto (fun (k : ℕ) ↦ (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - a k‖) atTop
    (𝓝 ((↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖))
L : Tendsto (fun (k : ℕ) ↦ dist y (a k)) atTop (𝓝 (dist y x))
⊢ ∀ᶠ (k : ℕ) in atTop,
    ‖HSub.hSub (β := F) (f y - f (a k)) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - a k) : F)‖ ≤
      (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - a k‖
have h : ∀ (a_1 : ℕ),
  dist y (a a_1) < u n →
    ‖HSub.hSub (β := F) (f y - f (a a_1)) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - a a_1) : F)‖ ≤
      (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - a a_1‖
Tactic: filter_upwards [(tendsto_order.1 L).2 _ hy.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
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)
L1 :
  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)‖)
L2 :
  Tendsto (fun (k : ℕ) ↦ (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - a k‖) atTop
    (𝓝 ((↑(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‖
have I : ∀ᶠ (k : ℕ) in atTop,
  ‖HSub.hSub (β := F) (f y - f (a k)) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (y - a k) : F)‖ ≤
    (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - a k‖
Tactic: have I : ∀ᶠ k in atTop, ‖f y - f (a k) - (f' z) (y - a k)‖ ≤ r (f' z) * ‖y - a k‖ := by
      have L : Tendsto (fun k => dist y (a k)) atTop (𝓝 (dist y x)) :=
        tendsto_const_nhds.dist a_lim
      filter_upwards [(tendsto_order.1 L).2 _ hy.2]
      intro k hk
      exact (aM k).2 y ⟨hy.1, hk⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
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
⊢ ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
    (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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)
have closure_M_subset : ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
Tactic: have closure_M_subset : ∀ n z, s ∩ closure (M n z) ⊆ M n z := by
    rintro n z x ⟨xs, hx⟩
    refine ⟨xs, fun y hy => ?_⟩
    obtain ⟨a, aM, a_lim⟩ : ∃ a : ℕ → E, (∀ k, a k ∈ M n z) ∧ Tendsto a atTop (𝓝 x) :=
      mem_closure_iff_seq_limit.1 hx
    have L1 :
      Tendsto (fun k : ℕ => ‖f y - f (a k) - (f' z) (y - a k)‖) atTop
        (𝓝 ‖f y - f x - (f' z) (y - x)‖) := by
      apply Tendsto.norm
      have L : Tendsto (fun k => f (a k)) atTop (𝓝 (f x)) := by
        apply (hf' x xs).continuousWithinAt.tendsto.comp
        apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ a_lim
        exact Eventually.of_forall fun k => (aM k).1
      apply Tendsto.sub (tendsto_const_nhds.sub L)
      exact ((f' z).continuous.tendsto _).comp (tendsto_const_nhds.sub a_lim)
    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 _
    have I : ∀ᶠ k in atTop, ‖f y - f (a k) - (f' z) (y - a k)‖ ≤ r (f' z) * ‖y - a k‖ := by
      have L : Tendsto (fun k => dist y (a k)) atTop (𝓝 (dist y x)) :=
        tendsto_const_nhds.dist a_lim
      filter_upwards [(tendsto_order.1 L).2 _ hy.2]
      intro k hk
      exact (aM k).2 y ⟨hy.1, hk⟩
    exact le_of_tendsto_of_tendsto L1 L2 I
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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
closure_M_subset :
  ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
⊢ ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
    (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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)
have inr : ∀ (d : ℕ → E) (hd : DenseRange d),
  ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
    (∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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 TopologicalSpace.exists_dense_seq E with ⟨d, hd⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
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
closure_M_subset :
  ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → (↑T : Type u_1) → ℕ → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ) ↦
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
n : ℕ
z : (↑T : Type u_1)
p : ℕ
x : E
hx : x ∈ s ∩ K n z p
y : E
hy : y ∈ s ∩ K n z p
⊢ ‖HSub.hSub (β := F) (f x - f y) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (x - y) : F)‖ ≤
    (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖x - y‖
have yM : y ∈ M n z
Tactic: have yM : y ∈ M n z := closure_M_subset _ _ ⟨hy.1, hy.2.1⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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
closure_M_subset :
  ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → (↑T : Type u_1) → ℕ → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ) ↦
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
n : ℕ
z : (↑T : Type u_1)
p : ℕ
x : E
hx : x ∈ s ∩ K n z p
y : E
hy : y ∈ s ∩ K n z p
yM : y ∈ M n z
⊢ ‖HSub.hSub (β := F) (f x - f y) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F) (x - y) : F)‖ ≤
    (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖x - y‖
have refine : x ∈ ball y (u n)
Tactic: refine yM.2 _ ⟨hx.1, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
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
closure_M_subset :
  ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → (↑T : Type u_1) → ℕ → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ) ↦
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
n : ℕ
z : (↑T : Type u_1)
p : ℕ
x : E
hx : x ∈ s ∩ K n z p
y : E
hy : y ∈ s ∩ K n z p
yM : y ∈ M n z
⊢ u n / 3 + u n / 3 < u n
have linarith : u n ≤ u n / 3 + u n / 3 → 3 / 3 = 1
Tactic: linarith [u_pos n]