awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
⊢ s =ᶠ[𝓝 x] t

Tactic:
h
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
h₁ : F 0 = x
⊢ s =ᶠ[𝓝 (F 0)] t

Tactic:
convert! h
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
⊢ F 0 = x

Tactic:
simp [F]
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
⊢ s =ᶠ[𝓝 (F 0)] t

Tactic:
have : s =ᶠ[𝓝 (F 0)] t := by convert! h; simp [F]
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
this : s =ᶠ[𝓝 (F 0)] t
⊢ EventuallyEq.{u_1, 0} (α := 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)

Tactic:
B.preimage_mem_nhds this

Premises used: Set.Mem, Filter.Eventually, setOf, ContinuousAt.preimage_mem_nhds, Filter.EventuallyEq, Set.preimage
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
this : s =ᶠ[𝓝 (F 0)] t
⊢ EventuallyEq.{u_1, 0} (α := 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)

Tactic:
exact B.preimage_mem_nhds this

Premises used: ContinuousAt.preimage_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
f₀ f₁ : E → F
f' : F
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
h₁ : EventuallyEq.{u_1, u_2} (β := F) (𝓝 0) (fun (t : 𝕜) ↦ f₀ (x + t • v)) fun (t : 𝕜) ↦ f₁ (x + t • v)
⊢ HasLineDerivAt 𝕜 f₀ f' x v ↔ HasLineDerivAt 𝕜 f₁ f' x v

Tactic:
apply hasDerivAt_iff

Premises used: Filter.EventuallyEq.hasDerivAt_iff
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
h₁ :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F
⊢ ContinuousAt F 0

Tactic:
apply Continuous.continuousAt

Premises used: Continuous.continuousAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
⊢ ContinuousAt F 0

Tactic:
have B : ContinuousAt F 0 := by apply Continuous.continuousAt; fun_prop
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
⊢ f₀ =ᶠ[𝓝 x] f₁

Tactic:
h
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
h₁ : F 0 = x
⊢ f₀ =ᶠ[𝓝 (F 0)] f₁

Tactic:
convert! h
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
⊢ F 0 = x

Tactic:
simp [F]
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
⊢ f₀ =ᶠ[𝓝 (F 0)] f₁

Tactic:
have : f₀ =ᶠ[𝓝 (F 0)] f₁ := by convert! h; simp [F]
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
this : f₀ =ᶠ[𝓝 (F 0)] f₁
⊢ EventuallyEq.{u_1, u_2} (β := F_1) (𝓝 0) (fun (t : 𝕜) ↦ f₀ (x + t • v)) fun (t : 𝕜) ↦ f₁ (x + t • v)

Tactic:
B.preimage_mem_nhds this

Premises used: Set.Mem, Filter.Eventually, setOf, ContinuousAt.preimage_mem_nhds, Filter.EventuallyEq, Set.preimage
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
this : f₀ =ᶠ[𝓝 (F 0)] f₁
⊢ EventuallyEq.{u_1, u_2} (β := F_1) (𝓝 0) (fun (t : 𝕜) ↦ f₀ (x + t • v)) fun (t : 𝕜) ↦ f₁ (x + t • v)

Tactic:
exact B.preimage_mem_nhds this

Premises used: ContinuousAt.preimage_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
f₀ f₁ : E → F
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
⊢ LineDifferentiableAt 𝕜 f₀ x v ↔ LineDifferentiableAt 𝕜 f₁ x v

Tactic:
⟨fun h' ↦ (h.hasLineDerivAt_iff.1 h'.hasLineDerivAt).lineDifferentiableAt,
  fun h' ↦ (h.hasLineDerivAt_iff.2 h'.hasLineDerivAt).lineDifferentiableAt⟩

Premises used: Iff.mpr, HasLineDerivAt.lineDifferentiableAt, Iff.intro, Iff.mp, LineDifferentiableAt.hasLineDerivAt, Filter.EventuallyEq.hasLineDerivAt_iff
-- 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
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
h₁ :
  EventuallyEq.{u_1, u_2} (β := F) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) (fun (t : 𝕜) ↦ f₀ (x + t • v)) fun (t : 𝕜) ↦
    f₁ (x + t • v)
hx₁ : f₀ (x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v) = f₁ (x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)
⊢ HasLineDerivWithinAt 𝕜 f₀ f' s x v ↔ HasLineDerivWithinAt 𝕜 f₁ f' s x v

Tactic:
apply hasDerivWithinAt_iff

Premises used: Filter.EventuallyEq.hasDerivWithinAt_iff
-- 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
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ 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
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ 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
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x + t • v
⊢ x = x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v

Tactic:
simp
-- 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
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x + t • v
⊢ EventuallyEq.{u_1, u_2} (β := F) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) (fun (t : 𝕜) ↦ f₀ (x + t • v)) fun (t : 𝕜) ↦
    f₁ (x + t • v)

Tactic:
exact A.continuousWithinAt.preimage_mem_nhdsWithin'' h (by simp)

Premises used: ContinuousWithinAt.preimage_mem_nhdsWithin'', Continuous.continuousWithinAt
-- 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
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ f₀ (x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v) = f₁ (x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)

Tactic:
simpa using hx
-- 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
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : x ∈ s
⊢ HasLineDerivWithinAt 𝕜 f₀ f' s x v ↔ HasLineDerivWithinAt 𝕜 f₁ f' s x v

Tactic:
h.hasLineDerivWithinAt_iff (h.eq_of_nhdsWithin hx)

Premises used: Filter.EventuallyEq.eq_of_nhdsWithin, Filter.EventuallyEq.hasLineDerivWithinAt_iff
-- 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
f₀ f₁ : E → F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ LineDifferentiableWithinAt 𝕜 f₀ s x v ↔ LineDifferentiableWithinAt 𝕜 f₁ s x v

Tactic:
⟨fun h' ↦ ((h.hasLineDerivWithinAt_iff hx).1 h'.hasLineDerivWithinAt).lineDifferentiableWithinAt,
  fun h' ↦ ((h.hasLineDerivWithinAt_iff hx).2 h'.hasLineDerivWithinAt).lineDifferentiableWithinAt⟩

Premises used: Iff.mpr, LineDifferentiableWithinAt.hasLineDerivWithinAt, HasLineDerivWithinAt.lineDifferentiableWithinAt, Iff.intro, Iff.mp, Filter.EventuallyEq.hasLineDerivWithinAt_iff
-- 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
f₀ f₁ : E → F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : x ∈ s
⊢ LineDifferentiableWithinAt 𝕜 f₀ s x v ↔ LineDifferentiableWithinAt 𝕜 f₁ s x v

Tactic:
h.lineDifferentiableWithinAt_iff (h.eq_of_nhdsWithin hx)

Premises used: Filter.EventuallyEq.lineDifferentiableWithinAt_iff, Filter.EventuallyEq.eq_of_nhdsWithin
-- 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
f f₁ : E → F
f' : F
s : Set E
x v : E
hf : HasLineDerivWithinAt 𝕜 f f' s x v
h'f : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ HasLineDerivWithinAt 𝕜 f₁ f' s x v

Tactic:
h'f.symm.hasLineDerivWithinAt_iff hx.symm |>.mp hf

Premises used: Iff.mp, Eq.symm, Filter.EventuallyEq.symm, Filter.EventuallyEq.hasLineDerivWithinAt_iff
-- 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
f f₁ : E → F
f' : F
x v : E
h : HasLineDerivAt 𝕜 f f' x v
h₁ : f₁ =ᶠ[𝓝 x] f
⊢ HasLineDerivAt 𝕜 f₁ f' x v

Tactic:
(EventuallyEq.hasLineDerivAt_iff h₁.symm).mp h

Premises used: Iff.mp, Filter.EventuallyEq.hasLineDerivAt_iff, Filter.EventuallyEq.symm
-- 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
f f₁ : E → F
s : Set E
x v : E
h : LineDifferentiableWithinAt 𝕜 f s x v
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ LineDifferentiableWithinAt 𝕜 f₁ s x v

Tactic:
(h.hasLineDerivWithinAt.congr_of_eventuallyEq h₁ hx).differentiableWithinAt

Premises used: LineDifferentiableWithinAt.hasLineDerivWithinAt, HasDerivWithinAt.differentiableWithinAt, LineDifferentiableWithinAt, HasLineDerivWithinAt.congr_of_eventuallyEq
-- 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
f f₁ : E → F
x v : E
h : LineDifferentiableAt 𝕜 f x v
hL : f₁ =ᶠ[𝓝 x] f
⊢ LineDifferentiableAt 𝕜 f₁ x v

Tactic:
hL.symm.lineDifferentiableAt_iff.mp h

Premises used: Iff.mp, Filter.EventuallyEq.lineDifferentiableAt_iff, Filter.EventuallyEq.symm
-- 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
f f₁ : E → F
s : Set E
x v : E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ f₁ (x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v) = f (x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)

Tactic:
simpa using hx
-- 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
f f₁ : E → F
s : Set E
x v : E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
apply :
  EventuallyEq.{u_1, u_2} (β := F) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) (fun (t : 𝕜) ↦ f₁ (x + t • v)) fun (t : 𝕜) ↦
    f (x + t • v)
⊢ lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v

Tactic:
apply derivWithin_eq ?_ (by simpa using hx)

Premises used: Filter.EventuallyEq.derivWithin_eq
-- 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
f f₁ : E → F
s : Set E
x v : E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f 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
f f₁ : E → F
s : Set E
x v : E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f 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
f f₁ : E → F
s : Set E
x v : E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x + t • v
⊢ x = x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v

Tactic:
simp
-- 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
f f₁ : E → F
s : Set E
x v : E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x + t • v
⊢ EventuallyEq.{u_1, u_2} (β := F) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) (fun (t : 𝕜) ↦ f₁ (x + t • v)) fun (t : 𝕜) ↦
    f (x + t • v)

Tactic:
exact A.continuousWithinAt.preimage_mem_nhdsWithin'' hs (by simp)

Premises used: ContinuousWithinAt.preimage_mem_nhdsWithin'', Continuous.continuousWithinAt
-- 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
f f₁ : E → F
s : Set E
x v : E
h : f₁ =ᶠ[𝓝 x] f
⊢ lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v

Tactic:
(h.filter_mono nhdsWithin_le_nhds).lineDerivWithin_eq h.self_of_nhds

Premises used: Filter.EventuallyEq.filter_mono, Filter.EventuallyEq.lineDerivWithin_eq, Filter.Eventually.self_of_nhds, nhdsWithin_le_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
f f₁ : E → F
x v : E
h : f₁ =ᶠ[𝓝 x] f
rw : lineDerivWithin 𝕜 f₁ univ x v = lineDeriv 𝕜 f x v
rw₁ : lineDerivWithin 𝕜 f₁ univ x v = lineDerivWithin 𝕜 f univ x v
rw₂ rw₃ : lineDerivWithin 𝕜 f univ x v = lineDerivWithin 𝕜 f univ x v
⊢ lineDeriv 𝕜 f₁ x v = lineDeriv 𝕜 f x v

Tactic:
rw [← lineDerivWithin_univ, ← lineDerivWithin_univ, h.lineDerivWithin_eq_nhds]

Premises used: lineDerivWithin_univ, Filter.EventuallyEq.lineDerivWithin_eq_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
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
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₀‖
apply : ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖x - 0‖
⊢ ‖f'‖ ≤ C * ‖v‖

Tactic:
apply HasDerivAt.le_of_lip' hf (by positivity)

Premises used: HasDerivAt.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
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
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₀‖
⊢ 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
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
⊢ ∀ᶠ (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
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
⊢ ∀ᶠ (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