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 : AddCommGroup E
inst_4 : Module 𝕜 E
f f₁ : E → F
s : Set E
x v : E
hs : EqOn f₁ f s
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 : AddCommGroup E
inst_4 : Module 𝕜 E
f f₁ : E → F
s : Set E
x v : E
hs : EqOn f₁ f s
hx : x ∈ s
⊢ lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v

Tactic:
lineDerivWithin_congr hs (hs hx)

Premises used: lineDerivWithin_congr
-- 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
f' : F
x v : E
⊢ HasLineDerivAt 𝕜 f f' x v ↔ Tendsto (fun (t : 𝕜) ↦ t⁻¹ • (f (x + t • v) - f x)) (𝓝[≠] 0) (𝓝 f')

Tactic:
simp only [HasLineDerivAt, hasDerivAt_iff_tendsto_slope_zero, zero_add,
    zero_smul, add_zero]

Premises used: zero_add, hasDerivAt_iff_tendsto_slope_zero, zero_smul, HasLineDerivAt, add_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
f' : F
x v : E
inst_5 : Preorder 𝕜
h : HasLineDerivAt 𝕜 f f' x v
⊢ Tendsto (fun (t : 𝕜) ↦ t⁻¹ • (f (x + t • v) - f x)) (𝓝[>] 0) (𝓝 f')

Tactic:
h.tendsto_slope_zero.mono_left (nhdsGT_le_nhdsNE 0)

Premises used: HasLineDerivAt.tendsto_slope_zero, nhdsGT_le_nhdsNE, Filter.Tendsto.mono_left, 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
f' : F
x v : E
inst_5 : Preorder 𝕜
h : HasLineDerivAt 𝕜 f f' x v
⊢ Tendsto (fun (t : 𝕜) ↦ t⁻¹ • (f (x + t • v) - f x)) (𝓝[<] 0) (𝓝 f')

Tactic:
h.tendsto_slope_zero.mono_left (nhdsLT_le_nhdsNE 0)

Premises used: HasLineDerivAt.tendsto_slope_zero, nhdsLT_le_nhdsNE, Filter.Tendsto.mono_left, 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
f' : F
s : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' s x v
hs : ∀ᶠ (t : 𝕜) in 𝓝 0, x + t • v ∈ s
⊢ HasLineDerivAt 𝕜 f f' x v

Tactic:
h.hasDerivAt hs

Premises used: HasDerivWithinAt.hasDerivAt, 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 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
apply : Membership.mem (γ := Filter 𝕜) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)
⊢ HasLineDerivWithinAt 𝕜 f f' s x v

Tactic:
apply HasDerivWithinAt.mono_of_mem_nhdsWithin h

Premises used: HasDerivWithinAt.mono_of_mem_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 : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
⊢ 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 : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
apply : ContinuousWithinAt.{u_1, u_3} (Y := E) (fun (t : 𝕜) ↦ x + t • v) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
⊢ Membership.mem (γ := Filter 𝕜) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)

Tactic:
apply ContinuousWithinAt.preimage_mem_nhdsWithin'' _ hst (by simp)

Premises used: ContinuousWithinAt.preimage_mem_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 : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
h₁ :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x + t • v
⊢ ContinuousWithinAt.{u_1, u_3} (Y := E) (fun (t : 𝕜) ↦ x + t • v) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0

Tactic:
apply Continuous.continuousWithinAt

Premises used: 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 : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] 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 : E → F
f' : F
s : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' s x v
hs : s ∈ 𝓝 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 : E → F
f' : F
s : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' s x v
hs : s ∈ 𝓝 x
⊢ x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v = x

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 : E → F
s : Set E
x v : E
h : LineDifferentiableWithinAt 𝕜 f s x v
hs : s ∈ 𝓝 x
⊢ LineDifferentiableAt 𝕜 f x v

Tactic:
(h.hasLineDerivWithinAt.hasLineDerivAt hs).lineDifferentiableAt

Premises used: LineDifferentiableWithinAt.hasLineDerivWithinAt, HasLineDerivAt.lineDifferentiableAt, HasLineDerivWithinAt.hasLineDerivAt
-- 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 : Set E
x : E
L : E →L[𝕜] F_1
hf : HasFDerivWithinAt f L s x
v : E
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
⊢ x = F 0

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 : Set E
x : E
L : E →L[𝕜] F_1
hf : HasFDerivWithinAt f L s x
v : E
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
⊢ HasFDerivWithinAt f L s (F 0)

Tactic:
rw [show x = F (0 : 𝕜) by simp [F]] at hf
-- 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 : Set E
x : E
L : E →L[𝕜] F_1
v : E
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
hf : HasFDerivWithinAt f L s (F 0)
⊢ HasDerivWithinAt F (0 + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 1 v) (F ⁻¹' s) 0

Tactic:
have A : HasDerivWithinAt F (0 + (1 : 𝕜) • v) (F ⁻¹' s) 0 :=
    ((hasDerivAt_const (0 : 𝕜) x).add ((hasDerivAt_id' (0 : 𝕜)).smul_const v)).hasDerivWithinAt
-- 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 : Set E
x : E
L : E →L[𝕜] F_1
v : E
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
hf : HasFDerivWithinAt f L s (F 0)
A : HasDerivWithinAt F (0 + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 1 v) (F ⁻¹' s) 0
⊢ HasDerivWithinAt F v (F ⁻¹' s) 0

Tactic:
simp only [one_smul, zero_add] at A

Premises used: zero_add, one_smul
-- 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 : Set E
x : E
L : E →L[𝕜] F_1
v : E
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
hf : HasFDerivWithinAt f L s (F 0)
A : HasDerivWithinAt F v (F ⁻¹' s) 0
⊢ HasLineDerivWithinAt 𝕜 f ((L : (a : E) → F_1) v) s x v

Tactic:
hf.comp_hasDerivWithinAt (x := (0 : 𝕜)) A (mapsTo_preimage F s)

Premises used: HasLineDerivWithinAt, Set.mapsTo_preimage, HasFDerivWithinAt.comp_hasDerivWithinAt, OfNat.ofNat
-- 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 : Set E
x : E
L : E →L[𝕜] F_1
v : E
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
hf : HasFDerivWithinAt f L s (F 0)
A : HasDerivWithinAt F v (F ⁻¹' s) 0
⊢ HasLineDerivWithinAt 𝕜 f ((L : (a : E) → F_1) v) s x v

Tactic:
exact hf.comp_hasDerivWithinAt (x := (0 : 𝕜)) A (mapsTo_preimage F s)

Premises used: Set.mapsTo_preimage, HasFDerivWithinAt.comp_hasDerivWithinAt, 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 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F
s : Set E
x v : E
hf : DifferentiableWithinAt 𝕜 f s x
⊢ LineDifferentiableWithinAt 𝕜 f s x v

Tactic:
hf.hasFDerivWithinAt.hasLineDerivWithinAt _ |>.lineDifferentiableWithinAt

Premises used: HasFDerivWithinAt.hasLineDerivWithinAt, HasLineDerivWithinAt.lineDifferentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- 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 : E → F
x : E
L : E →L[𝕜] F
hf : HasFDerivAt f L x
v : E
rw : HasLineDerivWithinAt 𝕜 f ((L : (a : E) → F) v) univ x v
⊢ HasLineDerivAt 𝕜 f ((L : (a : E) → F) v) x v

Tactic:
rw [← hasLineDerivWithinAt_univ]

Premises used: hasLineDerivWithinAt_univ
-- 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 : E → F
x : E
L : E →L[𝕜] F
hf : HasFDerivAt f L x
v : E
⊢ HasLineDerivWithinAt 𝕜 f ((L : (a : E) → F) v) univ x v

Tactic:
hf.hasFDerivWithinAt.hasLineDerivWithinAt v

Premises used: HasFDerivWithinAt.hasLineDerivWithinAt, HasFDerivAt.hasFDerivWithinAt
-- 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 : E → F
x : E
L : E →L[𝕜] F
hf : HasFDerivAt f L x
v : E
⊢ HasLineDerivWithinAt 𝕜 f ((L : (a : E) → F) v) univ x v

Tactic:
exact hf.hasFDerivWithinAt.hasLineDerivWithinAt v

Premises used: HasFDerivWithinAt.hasLineDerivWithinAt, HasFDerivAt.hasFDerivWithinAt
-- 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 : E → F
x v : E
hf : DifferentiableAt 𝕜 f x
⊢ LineDifferentiableAt 𝕜 f x v

Tactic:
hf.hasFDerivAt.hasLineDerivAt _ |>.lineDifferentiableAt

Premises used: HasLineDerivAt.lineDifferentiableAt, HasFDerivAt.hasLineDerivAt, DifferentiableAt.hasFDerivAt
-- 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 : E → F
x v : E
hf : DifferentiableAt 𝕜 f x
⊢ lineDeriv 𝕜 f x v = (fderiv 𝕜 f x : (a : E) → F) v

Tactic:
(hf.hasFDerivAt.hasLineDerivAt v).lineDeriv

Premises used: HasLineDerivAt.lineDeriv, HasFDerivAt.hasLineDerivAt, DifferentiableAt.hasFDerivAt
-- 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 : E → F
s t : Set E
x v : E
h : LineDifferentiableWithinAt 𝕜 f s x v
hst : s ∈ 𝓝[t] x
⊢ LineDifferentiableWithinAt 𝕜 f t x v

Tactic:
(h.hasLineDerivWithinAt.mono_of_mem_nhdsWithin hst).lineDifferentiableWithinAt

Premises used: HasLineDerivWithinAt.mono_of_mem_nhdsWithin, LineDifferentiableWithinAt.hasLineDerivWithinAt, 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 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 x
h₁ : Membership.mem (γ := Filter 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s)
⊢ lineDerivWithin 𝕜 f s x v = lineDeriv 𝕜 f x v

Tactic:
apply derivWithin_of_mem_nhds

Premises used: derivWithin_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
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 x
⊢ s ∈ 𝓝 (x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)

Tactic:
simpa 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 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 x
apply :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x + t • v
⊢ Membership.mem (γ := Filter 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s)

Tactic:
apply (Continuous.continuousAt _).preimage_mem_nhds (by simpa using h)

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
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 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 : E → F
s : Set E
x v : E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hx : x ∈ s
⊢ lineDerivWithin 𝕜 f s x v = lineDeriv 𝕜 f x v

Tactic:
lineDerivWithin_of_mem_nhds (hs.mem_nhds hx)

Premises used: lineDerivWithin_of_mem_nhds, IsOpen.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 : E → F
f' : F
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
h₁ : EventuallyEq.{u_1, 0} (α := 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)
⊢ HasLineDerivWithinAt 𝕜 f f' s x v ↔ HasLineDerivWithinAt 𝕜 f f' t x v

Tactic:
apply hasDerivWithinAt_congr_set

Premises used: hasDerivWithinAt_congr_set
-- 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
f' : F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
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 : E → F_1
f' : F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
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 : E → F_1
f' : F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
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 : E → F_1
f' : 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
f' : 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
f' : 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
f' : 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
f' : 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
f' : 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 : E → F
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
⊢ LineDifferentiableWithinAt 𝕜 f s x v ↔ LineDifferentiableWithinAt 𝕜 f t x v

Tactic:
⟨fun h' ↦ ((hasLineDerivWithinAt_congr_set h).1
    h'.hasLineDerivWithinAt).lineDifferentiableWithinAt,
  fun h' ↦ ((hasLineDerivWithinAt_congr_set h.symm).1
    h'.hasLineDerivWithinAt).lineDifferentiableWithinAt⟩

Premises used: LineDifferentiableWithinAt.hasLineDerivWithinAt, HasLineDerivWithinAt.lineDifferentiableWithinAt, Iff.intro, Iff.mp, hasLineDerivWithinAt_congr_set, 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 : E → F
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
h₁ : EventuallyEq.{u_1, 0} (α := 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)
⊢ lineDerivWithin 𝕜 f s x v = lineDerivWithin 𝕜 f t x v

Tactic:
apply derivWithin_congr_set

Premises used: derivWithin_congr_set
-- 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
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 : E → F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
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 : E → F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
⊢ ContinuousAt F 0

Tactic:
have B : ContinuousAt F 0 := by apply Continuous.continuousAt; fun_prop