awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
simp_rw : deriv (fun (x : 𝕜) ↦ f (x + -a)) x = deriv f (x + -a)
⊢ deriv (fun (x : 𝕜) ↦ f (x - a)) x = deriv f (x - a)

Tactic:
simp_rw [sub_eq_add_neg, deriv_comp_add_const]

Premises used: sub_eq_add_neg, deriv_comp_add_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ HasDerivAtFilter f f' (SProd.sprod (β := Filter 𝕜) L (pure x)) ↔
    Tendsto.{u, v} (β := F) (fun (y : 𝕜) ↦ slope f x y - (y - x)⁻¹ • (y - x) • f') L (𝓝 0)

Tactic:
simp only [hasDerivAtFilter_iff_tendsto, prod_pure, tendsto_map'_iff, Function.comp_def,
        ← norm_inv, ← norm_smul, ← tendsto_zero_iff_norm_tendsto_zero, slope_def_module, smul_sub]

Premises used: norm_smul, Filter.tendsto_map'_iff, norm_inv, smul_sub, Function.comp_def, hasDerivAtFilter_iff_tendsto, tendsto_zero_iff_norm_tendsto_zero, Filter.prod_pure, slope_def_module
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ ∀ a ∉ {x}ᶜ, slope f x a - (a - x)⁻¹ • (a - x) • f' = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ EventuallyEq.{u, v} (β := F) (L ⊓ 𝓟 {x}ᶜ) (fun (y : 𝕜) ↦ slope f x y - (y - x)⁻¹ • (y - x) • f') fun (y : 𝕜) ↦
    slope f x y - f'

Tactic:
(EqOn.eventuallyEq fun y hy ↦ ?_).filter_mono inf_le_right

Premises used: Filter.EventuallyEq.filter_mono, Set.EqOn.eventuallyEq, inf_le_right
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
refine : ∀ (y : 𝕜) (hy : Membership.mem (γ := Set 𝕜) {x}ᶜ y), slope f x y - (y - x)⁻¹ • (y - x) • f' = slope f x y - f'
⊢ EventuallyEq.{u, v} (β := F) (L ⊓ 𝓟 {x}ᶜ) (fun (y : 𝕜) ↦ slope f x y - (y - x)⁻¹ • (y - x) • f') fun (y : 𝕜) ↦
    slope f x y - f'

Tactic:
refine (EqOn.eventuallyEq fun y hy ↦ ?_).filter_mono inf_le_right

Premises used: Filter.EventuallyEq.filter_mono, Set.EqOn.eventuallyEq, inf_le_right
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) {x}ᶜ y
rw rw₁ : slope f x y - f' = slope f x y - f'
⊢ slope f x y - (y - x)⁻¹ • (y - x) • f' = slope f x y - f'

Tactic:
rw [inv_smul_smul₀ (sub_ne_zero.2 hy) f']

Premises used: Iff.mpr, inv_smul_smul₀, sub_ne_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
rw :
  Tendsto.{u, v} (β := F) (fun (y : 𝕜) ↦ slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔
    Tendsto (β := F) ((fun (x : F) ↦ x - f') ∘ slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 0)
⊢ Tendsto.{u, v} (β := F) (fun (y : 𝕜) ↦ slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔ Tendsto (slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 f')

Tactic:
rw [← nhds_translation_sub f', tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff, nhds_translation_sub
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ Tendsto.{u, v} (β := F) (fun (y : 𝕜) ↦ slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔
    Tendsto (β := F) ((fun (x : F) ↦ x - f') ∘ slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 0)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
simp :
  HasDerivAtFilter f f' (SProd.sprod (β := Filter 𝕜) (𝓝 x ⊓ 𝓟 s) (pure x)) ↔
    Tendsto (slope f x) (𝓝 x ⊓ 𝓟 s ⊓ 𝓟 {x}ᶜ) (𝓝 f')
⊢ HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f')

Tactic:
simp only [HasDerivWithinAt, nhdsWithin, diff_eq, ← inf_assoc, inf_principal.symm]

Premises used: Filter.inf_principal, nhdsWithin, HasDerivWithinAt, Set.diff_eq, inf_assoc, Eq.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
⊢ HasDerivAtFilter f f' (SProd.sprod (β := Filter 𝕜) (𝓝 x ⊓ 𝓟 s) (pure x)) ↔
    Tendsto (slope f x) (𝓝 x ⊓ 𝓟 s ⊓ 𝓟 {x}ᶜ) (𝓝 f')

Tactic:
hasDerivAtFilter_iff_tendsto_slope

Premises used: Set.Mem, hasDerivAtFilter_iff_tendsto_slope, setOf
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
⊢ HasDerivAtFilter f f' (SProd.sprod (β := Filter 𝕜) (𝓝 x ⊓ 𝓟 s) (pure x)) ↔
    Tendsto (slope f x) (𝓝 x ⊓ 𝓟 s ⊓ 𝓟 {x}ᶜ) (𝓝 f')

Tactic:
exact hasDerivAtFilter_iff_tendsto_slope

Premises used: hasDerivAtFilter_iff_tendsto_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
hs : x ∉ s
rw : Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f') ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f')
rw₁ rw₂ : Tendsto (slope f x) (𝓝[s] x) (𝓝 f') ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f')
⊢ HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f')

Tactic:
rw [hasDerivWithinAt_iff_tendsto_slope, diff_singleton_eq_self hs]

Premises used: Set.diff_singleton_eq_self, hasDerivWithinAt_iff_tendsto_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
⊢ HasDerivAt f f' x ↔ Tendsto (slope f x) (𝓝[≠] x) (𝓝 f')

Tactic:
hasDerivAtFilter_iff_tendsto_slope

Premises used: nhdsWithin, hasDerivAtFilter_iff_tendsto_slope, HasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst_3 : LinearOrder 𝕜
⊢ HasDerivAt f f' x ↔ Tendsto (slope f x) (𝓝[<] x) (𝓝 f') ∧ Tendsto (slope f x) (𝓝[>] x) (𝓝 f')

Tactic:
simp [hasDerivAt_iff_tendsto_slope, ← Iio_union_Ioi, nhdsWithin_union]

Premises used: Set.Iio_union_Ioi, nhdsWithin_union, hasDerivAt_iff_tendsto_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
⊢ 𝓝[≠] x = map (fun (t : 𝕜) ↦ x + t) (𝓝[≠] 0)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
⊢ 𝓝[≠] x = map (fun (t : 𝕜) ↦ x + t) (𝓝[≠] 0)

Tactic:
have : 𝓝[≠] x = Filter.map (fun t ↦ x + t) (𝓝[≠] 0) := by simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
this : 𝓝[≠] x = map (fun (t : 𝕜) ↦ x + t) (𝓝[≠] 0)
⊢ HasDerivAt f f' x ↔ Tendsto (fun (t : 𝕜) ↦ t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f')

Tactic:
simp [hasDerivAt_iff_tendsto_slope, this, -map_add_left_nhdsNE, slope, Function.comp_def]

Premises used: Filter.map_add_left_nhdsNE, slope, Function.comp_def, hasDerivAt_iff_tendsto_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst_3 : Preorder 𝕜
h : HasDerivAt f f' x
⊢ Tendsto (fun (t : 𝕜) ↦ t⁻¹ • (f (x + t) - f x)) (𝓝[>] 0) (𝓝 f')

Tactic:
h.tendsto_slope_zero.mono_left (nhdsGT_le_nhdsNE 0)

Premises used: nhdsGT_le_nhdsNE, Filter.Tendsto.mono_left, HasDerivAt.tendsto_slope_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst_3 : Preorder 𝕜
h : HasDerivAt f f' x
⊢ Tendsto (fun (t : 𝕜) ↦ t⁻¹ • (f (x + t) - f x)) (𝓝[<] 0) (𝓝 f')

Tactic:
h.tendsto_slope_zero.mono_left (nhdsLT_le_nhdsNE 0)

Premises used: nhdsLT_le_nhdsNE, Filter.Tendsto.mono_left, HasDerivAt.tendsto_slope_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
pos :
  ∀ (H : UniqueDiffWithinAt 𝕜 s x),
    derivWithin f s x ∈
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
neg :
  ∀ (H : ¬UniqueDiffWithinAt 𝕜 s x),
    derivWithin f s x ∈
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)

Tactic:
by_cases H : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)

Tactic:
simpa [derivWithin_zero_of_not_uniqueDiffWithinAt H] using subset_closure (zero_mem _)

Premises used: subset_closure, derivWithin_zero_of_not_uniqueDiffWithinAt, ZeroMemClass.zero_mem
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
pos :
  ∀ (H' : DifferentiableWithinAt 𝕜 f s x),
    derivWithin f s x ∈
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
neg :
  ∀ (H' : ¬DifferentiableWithinAt 𝕜 f s x),
    derivWithin f s x ∈
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)

Tactic:
by_cases H' : DifferentiableWithinAt 𝕜 f s x

Premises used: DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : ¬DifferentiableWithinAt 𝕜 f s x
neg : 0 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)

Tactic:
rw [derivWithin_zero_of_not_differentiableWithinAt H']

Premises used: derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : ¬DifferentiableWithinAt 𝕜 f s x
⊢ 0 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)

Tactic:
subset_closure (zero_mem _)

Premises used: subset_closure, ZeroMemClass.zero_mem
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : ¬DifferentiableWithinAt 𝕜 f s x
⊢ 0 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)

Tactic:
exact subset_closure (zero_mem _)

Premises used: subset_closure, ZeroMemClass.zero_mem
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
rw : UniqueDiffWithinAt 𝕜 (s ∩ t) x
⊢ (𝓝[(s ∩ t) \ {x}] x).NeBot

Tactic:
rw [← accPt_principal_iff_nhdsWithin, ← uniqueDiffWithinAt_iff_accPt]

Premises used: uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
⊢ UniqueDiffWithinAt 𝕜 (s ∩ t) x

Tactic:
H.mono_closure h

Premises used: UniqueDiffWithinAt.mono_closure
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
⊢ UniqueDiffWithinAt 𝕜 (s ∩ t) x

Tactic:
exact H.mono_closure h

Premises used: UniqueDiffWithinAt.mono_closure
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
⊢ (𝓝[(s ∩ t) \ {x}] x).NeBot

Tactic:
have I : (𝓝[(s ∩ t) \ {x}] x).NeBot := by
    rw [← accPt_principal_iff_nhdsWithin, ← uniqueDiffWithinAt_iff_accPt]
    exact H.mono_closure h
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
apply : 𝓝[(s ∩ t) \ {x}] x ≤ 𝓝[s \ {x}] x
⊢ Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))

Tactic:
apply Tendsto.mono_left (hasDerivWithinAt_iff_tendsto_slope.1 H'.hasDerivWithinAt)

Premises used: DifferentiableWithinAt.hasDerivWithinAt, Iff.mp, Filter.Tendsto.mono_left, hasDerivWithinAt_iff_tendsto_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
rw : 𝓝[t ∩ (s \ {x})] x ≤ 𝓝[s \ {x}] x
⊢ 𝓝[(s ∩ t) \ {x}] x ≤ 𝓝[s \ {x}] x

Tactic:
rw [inter_comm, inter_diff_assoc]

Premises used: Set.inter_comm, Set.inter_diff_assoc
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
⊢ 𝓝[t ∩ (s \ {x})] x ≤ 𝓝[s \ {x}] x

Tactic:
nhdsWithin_mono _ inter_subset_right

Premises used: nhdsWithin_mono, Set.inter_subset_right
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
⊢ 𝓝[t ∩ (s \ {x})] x ≤ 𝓝[s \ {x}] x

Tactic:
exact nhdsWithin_mono _ inter_subset_right

Premises used: nhdsWithin_mono, Set.inter_subset_right
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
⊢ Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))

Tactic:
have : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x)) := by
    apply Tendsto.mono_left (hasDerivWithinAt_iff_tendsto_slope.1 H'.hasDerivWithinAt)
    rw [inter_comm, inter_diff_assoc]
    exact nhdsWithin_mono _ inter_subset_right
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
pos :
  derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (↑(Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) : Set F)
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)

Tactic:
rw [← closure_closure, ← Submodule.topologicalClosure_coe]

Premises used: Submodule.topologicalClosure_coe, closure_closure
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
pos :
  ∀ᶠ (x_1 : 𝕜) in 𝓝[(s ∩ t) \ {x}] x,
    slope f x x_1 ∈ (↑(Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) : Set F)
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (↑(Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) : Set F)

Tactic:
apply mem_closure_of_tendsto this

Premises used: mem_closure_of_tendsto
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
h₁ :
  ∀ (y : 𝕜) (hy : y ∈ (s ∩ t) \ {x}),
    slope f x y ∈ (↑(Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) : Set F)
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[(s ∩ t) \ {x}] x,
    slope f x x_1 ∈ (↑(Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) : Set F)

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
h₁ :
  Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t)))
    ((y - x)⁻¹ • (f y - f x))
⊢ slope f x y ∈ (↑(Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) : Set F)

Tactic:
simp only [slope, vsub_eq_sub, SetLike.mem_coe]

Premises used: slope, SetLike.mem_coe, vsub_eq_sub
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t)))
    ((y - x)⁻¹ • (f y - f x))

Tactic:
Submodule.smul_mem _ _ (Submodule.sub_mem _ ?_ ?_)

Premises used: Set.Mem, Submodule.sub_mem, Submodule.smul_mem
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
h₁ : Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) (f y)
h₂ : Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) (f x)
⊢ Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t)))
    ((y - x)⁻¹ • (f y - f x))

Tactic:
refine Submodule.smul_mem _ _ (Submodule.sub_mem _ ?_ ?_)

Premises used: Submodule.sub_mem, Submodule.smul_mem
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
h₁ : Membership.mem (γ := Submodule 𝕜 F) (Submodule.span 𝕜 (f '' t)) (f y)
⊢ Membership.mem (γ := Submodule 𝕜 F) (Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) (f y)

Tactic:
apply Submodule.le_topologicalClosure

Premises used: Submodule.le_topologicalClosure
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
h₁ : f y ∈ f '' t
⊢ Membership.mem (γ := Submodule 𝕜 F) (Submodule.span 𝕜 (f '' t)) (f y)

Tactic:
apply Submodule.subset_span

Premises used: Submodule.subset_span