awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
this : ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
h :
  ∀ (t : 𝕜)
    (ht :
      Membership.mem (γ := Set 𝕜)
        (preimage.{u_1, u_3} (β := E) (fun (t : 𝕜) ↦ x₀ + t • v) {x : E | ‖f x - f x₀‖ ≤ C * ‖x - x₀‖}) t),
    ‖f (x₀ + t • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖t - 0‖
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖x - 0‖

Tactic:
filter_upwards [(A.continuousAt (x := 0)).preimage_mem_nhds this] with t ht

Premises used: ContinuousAt.preimage_mem_nhds, Continuous.continuousAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
this : ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
t : 𝕜
ht :
  Membership.mem (γ := Set 𝕜)
    (preimage.{u_1, u_3} (β := E) (fun (t : 𝕜) ↦ x₀ + t • v) {x : E | ‖f x - f x₀‖ ≤ C * ‖x - x₀‖}) t
⊢ ‖f (x₀ + t • v) - f x₀‖ ≤ C * (‖v‖ * ‖t‖)

Tactic:
simp only [preimage_setOf_eq, add_sub_cancel_left, norm_smul, mem_setOf_eq, mul_comm (‖t‖)] at ht

Premises used: Norm.norm, norm_smul, add_sub_cancel_left, Set.mem_setOf_eq, Set.preimage_setOf_eq, mul_comm
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
this : ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
t : 𝕜
ht : ‖f (x₀ + t • v) - f x₀‖ ≤ C * (‖v‖ * ‖t‖)
⊢ ‖f (x₀ + t • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖t - 0‖

Tactic:
simpa [mul_assoc] using ht

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖f'‖ ≤ (↑C : ℝ) * ‖v‖

Tactic:
hf.le_of_lip' C.coe_nonneg ?_

Premises used: NNReal.coe_nonneg, HasLineDerivAt.le_of_lip'
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
refine : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
⊢ ‖f'‖ ≤ (↑C : ℝ) * ‖v‖

Tactic:
refine hf.le_of_lip' C.coe_nonneg ?_

Premises used: NNReal.coe_nonneg, HasLineDerivAt.le_of_lip'
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
x : E
hx : x ∈ s
⊢ ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖

Tactic:
hlip.norm_sub_le hx (mem_of_mem_nhds hs)

Premises used: LipschitzOnWith.norm_sub_le, mem_of_mem_nhds
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E | x ∈ s → Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖) x} x} a
h₁ h₂ : ∀ (x : E) (hx : x ∈ s), ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖

Tactic:
filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
C : ℝ≥0
hlip : LipschitzWith C f
⊢ ‖f'‖ ≤ (↑C : ℝ) * ‖v‖

Tactic:
hf.le_of_lipschitzOn univ_mem (lipschitzOnWith_univ.2 hlip)

Premises used: Iff.mpr, HasLineDerivAt.le_of_lipschitzOn, lipschitzOnWith_univ, Filter.univ_mem
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ 0 ≤ C * ‖v‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
apply : ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖x - 0‖
⊢ ‖lineDeriv 𝕜 f x₀ v‖ ≤ C * ‖v‖

Tactic:
apply norm_deriv_le_of_lip' (by positivity)

Premises used: norm_deriv_le_of_lip'
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v

Tactic:
have A : Continuous (fun (t : 𝕜) ↦ x₀ + t • v) := by fun_prop
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
⊢ ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖

Tactic:
simpa using hlip
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
⊢ ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖

Tactic:
have : ∀ᶠ x in 𝓝 (x₀ + (0 : 𝕜) • v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖ := by simpa using hlip
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
this : ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
h :
  ∀ (t : 𝕜)
    (ht :
      Membership.mem (γ := Set 𝕜)
        (preimage.{u_1, u_3} (β := E) (fun (t : 𝕜) ↦ x₀ + t • v) {x : E | ‖f x - f x₀‖ ≤ C * ‖x - x₀‖}) t),
    ‖f (x₀ + t • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖t - 0‖
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖x - 0‖

Tactic:
filter_upwards [(A.continuousAt (x := 0)).preimage_mem_nhds this] with t ht

Premises used: ContinuousAt.preimage_mem_nhds, Continuous.continuousAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
this : ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
t : 𝕜
ht :
  Membership.mem (γ := Set 𝕜)
    (preimage.{u_1, u_3} (β := E) (fun (t : 𝕜) ↦ x₀ + t • v) {x : E | ‖f x - f x₀‖ ≤ C * ‖x - x₀‖}) t
⊢ ‖f (x₀ + t • v) - f x₀‖ ≤ C * (‖v‖ * ‖t‖)

Tactic:
simp only [preimage_setOf_eq, add_sub_cancel_left, norm_smul, mem_setOf_eq, mul_comm (‖t‖)] at ht

Premises used: Norm.norm, norm_smul, add_sub_cancel_left, Set.mem_setOf_eq, Set.preimage_setOf_eq, mul_comm
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
this : ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
t : 𝕜
ht : ‖f (x₀ + t • v) - f x₀‖ ≤ C * (‖v‖ * ‖t‖)
⊢ ‖f (x₀ + t • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖t - 0‖

Tactic:
simpa [mul_assoc] using ht

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖lineDeriv 𝕜 f x₀ v‖ ≤ (↑C : ℝ) * ‖v‖

Tactic:
norm_lineDeriv_le_of_lip' 𝕜 C.coe_nonneg ?_

Premises used: NNReal.coe_nonneg, norm_lineDeriv_le_of_lip'
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
refine : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
⊢ ‖lineDeriv 𝕜 f x₀ v‖ ≤ (↑C : ℝ) * ‖v‖

Tactic:
refine norm_lineDeriv_le_of_lip' 𝕜 C.coe_nonneg ?_

Premises used: NNReal.coe_nonneg, norm_lineDeriv_le_of_lip'
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
x : E
hx : x ∈ s
⊢ ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖

Tactic:
hlip.norm_sub_le hx (mem_of_mem_nhds hs)

Premises used: LipschitzOnWith.norm_sub_le, mem_of_mem_nhds
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E | x ∈ s → Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖) x} x} a
h₁ h₂ : ∀ (x : E) (hx : x ∈ s), ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖

Tactic:
filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ≥0
hlip : LipschitzWith C f
⊢ ‖lineDeriv 𝕜 f x₀ v‖ ≤ (↑C : ℝ) * ‖v‖

Tactic:
norm_lineDeriv_le_of_lipschitzOn 𝕜 univ_mem (lipschitzOnWith_univ.2 hlip)

Premises used: Iff.mpr, norm_lineDeriv_le_of_lipschitzOn, lipschitzOnWith_univ, Filter.univ_mem
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x : E
⊢ HasLineDerivWithinAt 𝕜 f 0 s x 0

Tactic:
simp [HasLineDerivWithinAt, hasDerivWithinAt_const]

Premises used: HasLineDerivWithinAt, hasDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x : E
⊢ HasLineDerivAt 𝕜 f 0 x 0

Tactic:
simp [HasLineDerivAt, hasDerivAt_const]

Premises used: hasDerivAt_const, HasLineDerivAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x : E
⊢ LineDifferentiableWithinAt 𝕜 f s x 0

Tactic:
hasLineDerivWithinAt_zero.lineDifferentiableWithinAt

Premises used: hasLineDerivWithinAt_zero, HasLineDerivWithinAt.lineDifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x : E
⊢ LineDifferentiableAt 𝕜 f x 0

Tactic:
hasLineDerivAt_zero.lineDifferentiableAt

Premises used: HasLineDerivAt.lineDifferentiableAt, hasLineDerivAt_zero
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x : E
⊢ lineDeriv 𝕜 f x 0 = 0

Tactic:
hasLineDerivAt_zero.lineDeriv

Premises used: HasLineDerivAt.lineDeriv, hasLineDerivAt_zero
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
E' : Type u_4
inst_5 : AddCommGroup E'
inst_6 : Module 𝕜 E'
f : E → F
f' : F
x : E'
L : E' →ₗ[𝕜] E
v : E'
hf : HasLineDerivAt 𝕜 (f ∘ (⇑L : (a : E') → E)) f' x v
⊢ HasLineDerivAt 𝕜 f f' ((L : (a : E') → E) x) ((L : (a : E') → E) v)

Tactic:
simpa [HasLineDerivAt] using hf

Premises used: HasLineDerivAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
E' : Type u_4
inst_5 : AddCommGroup E'
inst_6 : Module 𝕜 E'
f : E → F
x : E'
L : E' →ₗ[𝕜] E
v : E'
hf : LineDifferentiableAt 𝕜 (f ∘ (⇑L : (a : E') → E)) x v
⊢ LineDifferentiableAt 𝕜 f ((L : (a : E') → E) x) ((L : (a : E') → E) v)

Tactic:
hf.hasLineDerivAt.of_comp.lineDifferentiableAt

Premises used: HasLineDerivAt.lineDifferentiableAt, HasLineDerivAt.of_comp, LineDifferentiableAt.hasLineDerivAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
h : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
c : 𝕜
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ c • t
s' : Set 𝕜 := (fun (t : 𝕜) ↦ x + t • v) ⁻¹' s
⊢ HasDerivAt g c 0

Tactic:
simpa using (hasDerivAt_id (0 : 𝕜)).const_smul c

Premises used: HasDerivAt.const_smul, hasDerivAt_id, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
h : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
c : 𝕜
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ c • t
s' : Set 𝕜 := (fun (t : 𝕜) ↦ x + t • v) ⁻¹' s
⊢ HasDerivAt g c 0

Tactic:
have A : HasDerivAt g c 0 := by simpa using (hasDerivAt_id (0 : 𝕜)).const_smul c
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
h : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
c : 𝕜
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ c • t
s' : Set 𝕜 := (fun (t : 𝕜) ↦ x + t • v) ⁻¹' s
A : HasDerivAt g c 0
⊢ HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' s' (g 0)

Tactic:
simpa [g] using h
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
h : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
c : 𝕜
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ c • t
s' : Set 𝕜 := (fun (t : 𝕜) ↦ x + t • v) ⁻¹' s
A : HasDerivAt g c 0
⊢ HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' s' (g 0)

Tactic:
have B : HasDerivWithinAt (fun t ↦ f (x + t • v)) f' s' (g 0) := by simpa [g] using h
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
h : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
c : 𝕜
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ c • t
s' : Set 𝕜 := (fun (t : 𝕜) ↦ x + t • v) ⁻¹' s
A : HasDerivAt g c 0
B : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' s' (g 0)
⊢ HasDerivWithinAt ((fun (t : 𝕜) ↦ f (x + t • v)) ∘ g) (c • f') (g ⁻¹' s') 0

Tactic:
have Z := B.scomp (0 : 𝕜) A.hasDerivWithinAt (mapsTo_preimage g s')
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
h : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
c : 𝕜
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ c • t
s' : Set 𝕜 := (fun (t : 𝕜) ↦ x + t • v) ⁻¹' s
A : HasDerivAt g c 0
B : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' s' (g 0)
Z : HasDerivWithinAt ((fun (t : 𝕜) ↦ f (x + t • v)) ∘ g) (c • f') (g ⁻¹' s') 0
⊢ HasDerivWithinAt (fun (x_1 : 𝕜) ↦ f (x + x_1 • c • v)) (c • f')
    (preimage (β := 𝕜) (fun (t : 𝕜) ↦ t * c) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s)) 0

Tactic:
simp only [g, s', Function.comp_def, smul_eq_mul, mul_comm c, ← smul_smul] at Z

Premises used: smul_smul, Function.comp_def, mul_comm, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
h : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
c : 𝕜
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ c • t
s' : Set 𝕜 := (fun (t : 𝕜) ↦ x + t • v) ⁻¹' s
A : HasDerivAt g c 0
B : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' s' (g 0)
Z :
  HasDerivWithinAt (fun (x_1 : 𝕜) ↦ f (x + x_1 • c • v)) (c • f')
    (preimage (β := 𝕜) (fun (t : 𝕜) ↦ t * c) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s)) 0
⊢ HasDerivWithinAt (fun (x_1 : 𝕜) ↦ f (x + x_1 • c • v)) (c • f')
    (preimage (β := 𝕜) (fun (t : 𝕜) ↦ t * c) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s)) 0

Tactic:
Z
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
h : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
c : 𝕜
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ c • t
s' : Set 𝕜 := (fun (t : 𝕜) ↦ x + t • v) ⁻¹' s
A : HasDerivAt g c 0
B : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' s' (g 0)
Z :
  HasDerivWithinAt (fun (x_1 : 𝕜) ↦ f (x + x_1 • c • v)) (c • f')
    (preimage (β := 𝕜) (fun (t : 𝕜) ↦ t * c) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s)) 0
h₁ :
  Eq.{u_1 + 1} (α := Set 𝕜) ((fun (t : 𝕜) ↦ x + t • c • v) ⁻¹' s)
    (preimage (β := 𝕜) (fun (t : 𝕜) ↦ t * c) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s))
⊢ HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • c • v)) (c • f') ((fun (t : 𝕜) ↦ x + t • c • v) ⁻¹' s) 0

Tactic:
convert! Z