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‖}
x : E
xs : x ∈ s
⊢ Membership.mem (γ := Set (E →L[ℝ] F)) (⋃ z ∈ T, ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)) (f' x)
have rw : Membership.mem (γ := Set (E →L[ℝ] F)) (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ)) (f' x)
Tactic: rw [hT]
-- 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‖}
x : E
xs : x ∈ s
⊢ Membership.mem (γ := Set (E →L[ℝ] F)) (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ)) (f' x)
have refine : f' x ∈
  ball (f' (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ s) x xs) : E))
    (↑(r (f' (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ s) x xs) : E))) : ℝ)
Tactic: refine mem_iUnion.2 ⟨⟨x, xs⟩, ?_⟩
-- 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‖}
x : E
xs : x ∈ s
⊢ ∃ z ∈ T, f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
have this : Membership.mem (γ := Set (E →L[ℝ] F)) (⋃ z ∈ T, ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)) (f' x)
Tactic: 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
-- 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‖}
x : E
xs : x ∈ s
this : Membership.mem (γ := Set (E →L[ℝ] F)) (⋃ z ∈ T, ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)) (f' x)
⊢ ∃ z ∈ T, f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
have rwa : ∀ (this : ∃ (i : (↑s : Type u_1)) (_ : i ∈ T), f' x ∈ ball (f' (↑i : E)) (↑(r (f' (↑i : E))) : ℝ)),
  ∃ z ∈ T, f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
Tactic: rwa [mem_iUnion₂, bex_def] at this
Cleared hypotheses: this
-- 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‖}
x : E
xs : x ∈ s
this : Membership.mem (γ := Set (E →L[ℝ] F)) (⋃ z ∈ T, ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)) (f' x)
rwa :
  ∀ (this : ∃ (i : (↑s : Type u_1)) (_ : i ∈ T), f' x ∈ ball (f' (↑i : E)) (↑(r (f' (↑i : E))) : ℝ)),
    ∃ z ∈ T, f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
⊢ ∃ z ∈ T, f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
have rwa₁ : ∀ (this : ∃ x_1 ∈ T, f' x ∈ ball (f' (↑x_1 : E)) (↑(r (f' (↑x_1 : E))) : ℝ)),
  ∃ z ∈ T, f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
Tactic: rwa [mem_iUnion₂, bex_def] at this
Cleared hypotheses: this
-- 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‖}
x : E
xs : x ∈ s
⊢ ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
have obtain : ∀ (z : (↑s : Type u_1)) (zT : z ∈ T) (hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)),
  ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
Tactic: 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
-- 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‖}
x : E
xs : x ∈ s
z : (↑s : Type u_1)
zT : z ∈ T
hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
⊢ ∃ (ε : ℝ), 0 < ε ∧ ‖f' x - f' (↑z : E)‖ + ε ≤ (↑(r (f' (↑z : E))) : ℝ)
have refine : 0 < (↑(r (f' (↑z : E))) : ℝ) - ‖f' x - f' (↑z : E)‖
Tactic: refine ⟨r (f' z) - ‖f' x - f' z‖, ?_, le_of_eq (by abel)⟩
-- 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‖}
x : E
xs : x ∈ s
z : (↑s : Type u_1)
zT : z ∈ T
hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
⊢ ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
have obtain : ∀ (ε : ℝ) (εpos : 0 < ε) (hε : ‖f' x - f' (↑z : E)‖ + ε ≤ (↑(r (f' (↑z : E))) : ℝ)),
  ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
Tactic: 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
-- 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‖}
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))) : ℝ)
⊢ ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
have obtain : ∀ (δ : ℝ) (δ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 : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
Tactic: 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)
-- 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‖}
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 : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
have obtain : ∀ (n : ℕ) (hn : u n < δ), ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
Tactic: obtain ⟨n, hn⟩ : ∃ n, u n < δ := ((tendsto_order.1 u_lim).2 _ δpos).exists
-- 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‖}
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 < δ
⊢ ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
have refine : ∀ y ∈ s ∩ ball x (u n),
  ‖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: refine ⟨n, ⟨z, zT⟩, ⟨xs, ?_⟩⟩
-- 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‖}
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)
⊢ ‖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)‖
have e_a : 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)
Tactic: congr 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‖}
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)
⊢ 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)
have e_a : f y - f x - HSub.hSub (α := F) (β := F) ((f' (↑z : E) : (a : E) → F) y : F) ((f' (↑z : E) : (a : E) → F) x : F) =
  f y - f x - HSub.hSub (α := F) (β := F) ((f' x : (a : E) → F) y : F) ((f' x : (a : E) → F) x : F) +
    (HSub.hSub (α := F) (β := F) ((f' x : (a : E) → F) y : F) ((f' (↑z : E) : (a : E) → F) y : F) -
      HSub.hSub (α := F) (β := F) ((f' x : (a : E) → F) x : F) ((f' (↑z : E) : (a : E) → F) x : F))
Tactic: simp only [ContinuousLinearMap.coe_sub', map_sub, Pi.sub_apply]
-- 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‖}
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)
⊢ ‖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‖
have refine : y ∈ ball x δ ∩ s
Tactic: refine add_le_add (hδ ?_) (ContinuousLinearMap.le_opNorm _ _)
-- 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‖}
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 ∈ ball x δ ∩ s
have rw : y ∈ s ∩ ball x δ
Tactic: rw [inter_comm]