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))) : ℝ)
⊢ 0 < (↑(r (f' (↑z : E))) : ℝ) - ‖f' x - f' (↑z : E)‖

Tactic:
simpa only [sub_pos] using mem_ball_iff_norm.mp hz

Premises used: sub_pos, mem_ball_iff_norm, 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‖}
x : E
xs : x ∈ s
z : (↑s : Type u_1)
zT : z ∈ T
hz : f' x ∈ ball (f' (↑z : E)) (↑(r (f' (↑z : E))) : ℝ)
obtain :
  ∀ (ε : ℝ) (εpos : 0 < ε) (hε : ‖f' x - f' (↑z : E)‖ + ε ≤ (↑(r (f' (↑z : E))) : ℝ)),
    ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
⊢ ∃ (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

Premises used: Subtype.val
-- 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))) : ℝ)
⊢ ∃ (δ : ℝ),
    0 < δ ∧ ball x δ ∩ s ⊆ {y : E | ‖HSub.hSub (β := F) (f y - f x) ((f' x : (a : E) → F) (y - x) : F)‖ ≤ ε * ‖y - x‖}

Tactic:
Metric.mem_nhdsWithin_iff.1 ((hf' x xs).isLittleO.def εpos)

Premises used: Metric.mem_nhdsWithin_iff, Iff.mp, Asymptotics.IsLittleO.def, HasFDerivWithinAt.isLittleO
-- 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))) : ℝ)
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
⊢ ∃ (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)

Premises used: Metric.mem_nhdsWithin_iff, Iff.mp, Asymptotics.IsLittleO.def, HasFDerivWithinAt.isLittleO
-- 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 : ℕ), u n < δ

Tactic:
((tendsto_order.1 u_lim).2 _ δpos).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.right, 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‖}
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‖}
obtain : ∀ (n : ℕ) (hn : u n < δ), ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
⊢ ∃ (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

Premises used: tendsto_order, Filter.Eventually.exists, And.right, 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‖}
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

Tactic:
⟨n, ⟨z, zT⟩, ⟨xs, ?_⟩⟩

Premises used: Subtype.mk, And.intro, Exists.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‖}
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 < δ
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‖
⊢ ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z

Tactic:
refine ⟨n, ⟨z, zT⟩, ⟨xs, ?_⟩⟩
-- 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)
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)
⊢ ‖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
-- 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)
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))
⊢ 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:
simp only [ContinuousLinearMap.coe_sub', map_sub, Pi.sub_apply]

Premises used: map_sub, ContinuousLinearMap.coe_sub', Pi.sub_apply
-- 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)
⊢ 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:
abel
-- 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)
⊢ ‖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)‖ ≤
    ‖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)

Tactic:
norm_add_le _ _

Premises used: norm_add_le
-- 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)
⊢ ‖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‖

Tactic:
add_le_add (hδ ?_) (ContinuousLinearMap.le_opNorm _ _)

Premises used: ContinuousLinearMap.le_opNorm, add_le_add
-- 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)
refine : y ∈ ball x δ ∩ s
⊢ ‖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‖

Tactic:
refine add_le_add (hδ ?_) (ContinuousLinearMap.le_opNorm _ _)

Premises used: ContinuousLinearMap.le_opNorm, add_le_add