awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k : ℕ
α : (↑I : Type)
f : E → F
a : E
hf : ContDiffPointwiseHolderAt k α f a
m : ℕ
ihm :
  ∀ {l : ℕ} (hl : l + m ≤ k),
    ContDiffPointwiseHolderAt (F := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin m) ↦ E) F) l α
      (iteratedFDeriv ℝ m f) a
l : ℕ
hl : l + 1 + m ≤ k
succ :
  ContDiffPointwiseHolderAt (F := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin (m + 1)) ↦ E) F) l α
    (Function.comp (β := E →L[ℝ] ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin m) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv ℝ (fun (x : Fin (m + 1)) ↦ E) F) :
            (E →L[ℝ] ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin m) ↦ E) F) ≃ₗᵢ[ℝ]
              ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (x : Fin (m + 1)) ↦ E) F) :
        (a : E →L[ℝ] ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ E) F) →
          ContinuousMultilinearMap ℝ (fun (x : Fin (m + 1)) ↦ E) F)
      (fderiv ℝ (iteratedFDeriv ℝ m f)))
    a
⊢ ContDiffPointwiseHolderAt (F := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin (m + 1)) ↦ E) F) l α
    (iteratedFDeriv ℝ (m + 1) f) a

Tactic:
simpa +unfoldPartialApp [iteratedFDeriv_succ_eq_comp_left] using (ihm hl).fderiv l.lt_add_one

Premises used: Nat.lt_add_one, ContDiffPointwiseHolderAt.fderiv, iteratedFDeriv_succ_eq_comp_left
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k l m : ℕ
α : (↑I : Type)
f : E → F
a : E
hf : ContDiffPointwiseHolderAt k α f a
hl : l + m ≤ k
zero :
  ∀ {l : ℕ} (hl : l + 0 ≤ k),
    ContDiffPointwiseHolderAt (F := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin 0) ↦ E) F) l α
      (iteratedFDeriv ℝ 0 f) a
succ :
  ∀ (m : ℕ)
    (ihm :
      ∀ {l : ℕ} (hl : l + m ≤ k),
        ContDiffPointwiseHolderAt (F := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin m) ↦ E) F) l α
          (iteratedFDeriv ℝ m f) a)
    {l : ℕ} (hl : l + (m + 1) ≤ k),
    ContDiffPointwiseHolderAt (F := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin (m + 1)) ↦ E) F) l α
      (iteratedFDeriv ℝ (m + 1) f) a
⊢ ContDiffPointwiseHolderAt (F := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin m) ↦ E) F) l α
    (iteratedFDeriv ℝ m f) a

Tactic:
induction m generalizing l with
  | zero =>
    simpa +unfoldPartialApp [iteratedFDeriv_zero_eq_comp] using hf.of_order_le hl
  | succ m ihm =>
    rw [← add_assoc, add_right_comm] at hl
    simpa +unfoldPartialApp [iteratedFDeriv_succ_eq_comp_left] using (ihm hl).fderiv l.lt_add_one

Premises used: add_assoc, add_right_comm, iteratedFDeriv_zero_eq_comp, iteratedFDeriv_succ_eq_comp_left, ContDiffPointwiseHolderAt.of_order_le
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k : ℕ
α : (↑I : Type)
f : E → F
a : E
g : E → F
hf : ContDiffPointwiseHolderAt k α f a
hfg : f =ᶠ[𝓝 a] g
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k g x)
        (iteratedFDeriv ℝ k g a))
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
EventuallyEq.trans_isBigO (.sub ?_ ?_) hf.isBigO

Premises used: ContDiffPointwiseHolderAt.isBigO, Filter.EventuallyEq.sub, Filter.EventuallyEq.trans_isBigO
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k : ℕ
α : (↑I : Type)
f : E → F
a : E
g : E → F
hf : ContDiffPointwiseHolderAt k α f a
hfg : f =ᶠ[𝓝 a] g
refine_1 :
  (𝓝 a).EventuallyEq (β := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k g)
    (iteratedFDeriv ℝ k f)
refine_2 :
  (𝓝 a).EventuallyEq (β := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F)
    (fun (x : E) ↦ iteratedFDeriv ℝ k g a) fun (x : E) ↦ iteratedFDeriv ℝ k f a
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k g x)
        (iteratedFDeriv ℝ k g a))
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
refine EventuallyEq.trans_isBigO (.sub ?_ ?_) hf.isBigO

Premises used: ContDiffPointwiseHolderAt.isBigO, Filter.EventuallyEq.sub, Filter.EventuallyEq.trans_isBigO
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k : ℕ
α : (↑I : Type)
f : E → F
a : E
g : E → F
hf : ContDiffPointwiseHolderAt k α f a
hfg : f =ᶠ[𝓝 a] g
⊢ (𝓝 a).EventuallyEq (β := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k g)
    (iteratedFDeriv ℝ k f)

Tactic:
hfg.symm.iteratedFDeriv ℝ _

Premises used: Real, Filter.EventuallyEq.iteratedFDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k : ℕ
α : (↑I : Type)
f : E → F
a : E
g : E → F
hf : ContDiffPointwiseHolderAt k α f a
hfg : f =ᶠ[𝓝 a] g
⊢ (𝓝 a).EventuallyEq (β := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k g)
    (iteratedFDeriv ℝ k f)

Tactic:
exact hfg.symm.iteratedFDeriv ℝ _

Premises used: Real, Filter.EventuallyEq.iteratedFDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k : ℕ
α : (↑I : Type)
f : E → F
a : E
g : E → F
hf : ContDiffPointwiseHolderAt k α f a
hfg : f =ᶠ[𝓝 a] g
refine_2 refine_2₁ :
  (𝓝 a).EventuallyEq (β := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F)
    (fun (x : E) ↦ iteratedFDeriv ℝ k f a) fun (x : E) ↦ iteratedFDeriv ℝ k f a
⊢ (𝓝 a).EventuallyEq (β := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F)
    (fun (x : E) ↦ iteratedFDeriv ℝ k g a) fun (x : E) ↦ iteratedFDeriv ℝ k f a

Tactic:
rw [hfg.symm.iteratedFDeriv ℝ _ |>.self_of_nhds]

Premises used: Real, Filter.Eventually.self_of_nhds, Filter.EventuallyEq.iteratedFDeriv, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
k : ℕ
α : (↑I : Type)
a : E
f : E → F →L[ℝ] G
g : E → F
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
⊢ DifferentiableAt ℝ (F := G) (fun (x : (F →L[ℝ] G) × F) ↦ (x.1 : (a : F) → G) x.2) (f a, g a)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
⊢ dslope f a a = deriv f a

Tactic:
update_self ..

Premises used: dslope, Function.update_self
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
⊢ dslope f a a = deriv f a

Tactic:
exact update_self ..

Premises used: Function.update_self
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
⊢ dslope f a a = deriv f a

Tactic:
classical
  exact update_self ..

Premises used: Function.update_self
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : 𝕜
f : 𝕜 → E
h : b ≠ a
⊢ dslope f a b = slope f a b

Tactic:
update_of_ne h ..

Premises used: dslope, Function.update_of_ne
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : 𝕜
f : 𝕜 → E
h : b ≠ a
⊢ dslope f a b = slope f a b

Tactic:
exact update_of_ne h ..

Premises used: Function.update_of_ne
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : 𝕜
f : 𝕜 → E
h : b ≠ a
⊢ dslope f a b = slope f a b

Tactic:
classical
  exact update_of_ne h ..
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
a b : 𝕜
H : a = b → DifferentiableAt 𝕜 g a
inl :
  ∀ (H : b = b → DifferentiableAt 𝕜 g b),
    Eq.{u_3 + 1} (α := F) (dslope ((⇑f : (a : E) → F) ∘ g) b b : F) ((f : (a : E) → F) (dslope g b b) : F)
inr :
  ∀ (hne : b ≠ a),
    Eq.{u_3 + 1} (α := F) (dslope ((⇑f : (a : E) → F) ∘ g) a b : F) ((f : (a : E) → F) (dslope g a b) : F)
⊢ Eq.{u_3 + 1} (α := F) (dslope ((⇑f : (a : E) → F) ∘ g) a b : F) ((f : (a : E) → F) (dslope g a b) : F)

Tactic:
rcases eq_or_ne b a with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
inl : Eq.{u_3 + 1} (α := F) (deriv ((⇑f : (a : E) → F) ∘ g) b : F) ((f : (a : E) → F) (deriv g b) : F)
⊢ Eq.{u_3 + 1} (α := F) (dslope ((⇑f : (a : E) → F) ∘ g) b b : F) ((f : (a : E) → F) (dslope g b b) : F)

Tactic:
simp only [dslope_same]

Premises used: dslope_same
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
⊢ Eq.{u_3 + 1} (α := F) (deriv ((⇑f : (a : E) → F) ∘ g) b : F) ((f : (a : E) → F) (deriv g b) : F)

Tactic:
(f.hasFDerivAt.comp_hasDerivAt b (H rfl).hasDerivAt).deriv

Premises used: ContinuousLinearMap.hasFDerivAt, DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasFDerivAt.comp_hasDerivAt, rfl
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
b : 𝕜
H : b = b → DifferentiableAt 𝕜 g b
⊢ Eq.{u_3 + 1} (α := F) (deriv ((⇑f : (a : E) → F) ∘ g) b : F) ((f : (a : E) → F) (deriv g b) : F)

Tactic:
exact (f.hasFDerivAt.comp_hasDerivAt b (H rfl).hasDerivAt).deriv

Premises used: ContinuousLinearMap.hasFDerivAt, DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasFDerivAt.comp_hasDerivAt, rfl
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
g : 𝕜 → E
a b : 𝕜
H : a = b → DifferentiableAt 𝕜 g a
hne : b ≠ a
⊢ Eq.{u_3 + 1} (α := F) (dslope ((⇑f : (a : E) → F) ∘ g) a b : F) ((f : (a : E) → F) (dslope g a b) : F)

Tactic:
simpa only [dslope_of_ne _ hne] using f.toLinearMap.slope_comp g a b

Premises used: ContinuousLinearMap.toLinearMap, dslope_of_ne, LinearMap.slope_comp
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
⊢ EqOn (dslope f a) (slope f a) {a}ᶜ

Tactic:
fun _ =>
  dslope_of_ne f

Premises used: Set.Mem, setOf, Set.EqOn, dslope_of_ne, Set.singleton, Not
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : 𝕜
f : 𝕜 → E
h : b ≠ a
⊢ dslope f a =ᶠ[𝓝 b] slope f a

Tactic:
(eqOn_dslope_slope f a).eventuallyEq_of_mem (isOpen_ne.mem_nhds h)

Premises used: Set.EqOn.eventuallyEq_of_mem, eqOn_dslope_slope, isOpen_ne, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a : 𝕜
f : 𝕜 → E
⊢ dslope f a =ᶠ[𝓝[≠] a] slope f a

Tactic:
(eqOn_dslope_slope f a).eventuallyEq_of_mem self_mem_nhdsWithin

Premises used: Set.EqOn.eventuallyEq_of_mem, eqOn_dslope_slope, self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
inl : (b - b) • dslope f b b = f b - f b
inr : ∀ (hne : b ≠ a), (b - a) • dslope f a b = f b - f a
⊢ (b - a) • dslope f a b = f b - f a

Tactic:
rcases eq_or_ne b a with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
b : 𝕜
⊢ (b - b) • dslope f b b = f b - f b

Tactic:
simp [dslope_of_ne, *]

Premises used: dslope_of_ne
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
hne : b ≠ a
⊢ (b - a) • dslope f a b = f b - f a

Tactic:
simp [dslope_of_ne, *]

Premises used: dslope_of_ne
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : 𝕜
f : 𝕜 → E
h : b ≠ a
rw : slope (PE := E) (fun (x : 𝕜) ↦ (x - a) • f x) a b = f b
rw₁ rw₂ : f b = f b
⊢ dslope (fun (x : 𝕜) ↦ (x - a) • f x) a b = f b

Tactic:
rw [dslope_of_ne _ h, slope_sub_smul _ h.symm]

Premises used: Ne.symm, dslope_of_ne, slope_sub_smul
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
⊢ EqOn (dslope (fun (x : 𝕜) ↦ (x - a) • f x) a) f {a}ᶜ

Tactic:
fun _ => dslope_sub_smul_of_ne f

Premises used: Set.Mem, setOf, dslope_sub_smul_of_ne, Set.EqOn, Set.singleton, Not
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : DecidableEq 𝕜
f : 𝕜 → E
a : 𝕜
⊢ dslope (fun (x : 𝕜) ↦ (x - a) • f x) a = update (β := fun (a : 𝕜) ↦ E) f a (deriv (fun (x : 𝕜) ↦ (x - a) • f x) a)

Tactic:
eq_update_iff.2 ⟨dslope_same _ _, eqOn_dslope_sub_smul f a⟩

Premises used: Iff.mpr, eqOn_dslope_sub_smul, dslope_same, Function.eq_update_iff, And.intro
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
⊢ ContinuousAt (dslope f a) a ↔ DifferentiableAt 𝕜 f a

Tactic:
simp only [dslope, continuousAt_update_same, ← hasDerivAt_deriv_iff, hasDerivAt_iff_tendsto_slope]

Premises used: hasDerivAt_deriv_iff, dslope, hasDerivAt_iff_tendsto_slope, continuousAt_update_same
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : ContinuousWithinAt (dslope f a) s b
⊢ ContinuousWithinAt.{u_1, u_2} (Y := E) (fun (x : 𝕜) ↦ (x - a) • dslope f a x + f a) s b

Tactic:
have : ContinuousWithinAt (fun x => (x - a) • dslope f a x + f a) s b :=
    ((continuousWithinAt_id.sub continuousWithinAt_const).smul h).add continuousWithinAt_const
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : ContinuousWithinAt (dslope f a) s b
this : ContinuousWithinAt.{u_1, u_2} (Y := E) (fun (x : 𝕜) ↦ (x - a) • dslope f a x + f a) s b
⊢ ContinuousWithinAt f s b

Tactic:
simpa only [sub_smul_dslope, sub_add_cancel] using this

Premises used: sub_smul_dslope, sub_add_cancel
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
h : ContinuousAt (dslope f a) b
⊢ ContinuousAt f b

Tactic:
(continuousWithinAt_univ _ _).1 h.continuousWithinAt.of_dslope

Premises used: continuousWithinAt_univ, ContinuousAt.continuousWithinAt, ContinuousWithinAt.of_dslope, Iff.mp
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
s : Set 𝕜
h : ContinuousOn (dslope f a) s
⊢ ContinuousOn f s

Tactic:
fun x hx =>
  (h x hx).of_dslope

Premises used: ContinuousWithinAt.of_dslope, ContinuousOn
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
⊢ ContinuousWithinAt (dslope f a) s b ↔ ContinuousWithinAt f s b

Tactic:
⟨ContinuousWithinAt.of_dslope, fun hc => ?_⟩

Premises used: ContinuousWithinAt.of_dslope, Iff.intro
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
refine : ∀ (hc : ContinuousWithinAt f s b), ContinuousWithinAt (dslope f a) s b
⊢ ContinuousWithinAt (dslope f a) s b ↔ ContinuousWithinAt f s b

Tactic:
refine ⟨ContinuousWithinAt.of_dslope, fun hc => ?_⟩
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hc : ContinuousWithinAt f s b
simp : ContinuousWithinAt (slope f a) s b
⊢ ContinuousWithinAt (dslope f a) s b

Tactic:
simp only [dslope, continuousWithinAt_update_of_ne h]

Premises used: dslope, continuousWithinAt_update_of_ne
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hc : ContinuousWithinAt f s b
⊢ ContinuousWithinAt (slope f a) s b

Tactic:
((continuousWithinAt_id.sub continuousWithinAt_const).inv₀ (sub_ne_zero.2 h)).smul
    (hc.sub continuousWithinAt_const)

Premises used: Iff.mpr, sub_ne_zero, ContinuousWithinAt.sub, continuousWithinAt_id, slope, ContinuousWithinAt.inv₀, continuousWithinAt_const, ContinuousWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hc : ContinuousWithinAt f s b
⊢ ContinuousWithinAt (slope f a) s b

Tactic:
exact ((continuousWithinAt_id.sub continuousWithinAt_const).inv₀ (sub_ne_zero.2 h)).smul
    (hc.sub continuousWithinAt_const)

Premises used: Iff.mpr, sub_ne_zero, ContinuousWithinAt.sub, continuousWithinAt_id, ContinuousWithinAt.inv₀, continuousWithinAt_const, ContinuousWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hc : ContinuousWithinAt f s b
simp : ContinuousWithinAt (slope f a) s b
⊢ ContinuousWithinAt (dslope f a) s b

Tactic:
classical
  simp only [dslope, continuousWithinAt_update_of_ne h]
  exact ((continuousWithinAt_id.sub continuousWithinAt_const).inv₀ (sub_ne_zero.2 h)).smul
    (hc.sub continuousWithinAt_const)

Premises used: Iff.mpr, sub_ne_zero, ContinuousWithinAt.sub, continuousWithinAt_id, ContinuousWithinAt.inv₀, dslope, continuousWithinAt_const, ContinuousWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
h : b ≠ a
⊢ ContinuousAt (dslope f a) b ↔ ContinuousAt f b

Tactic:
simp only [← continuousWithinAt_univ, continuousWithinAt_dslope_of_ne h]

Premises used: continuousWithinAt_univ, continuousWithinAt_dslope_of_ne
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
⊢ ContinuousOn (dslope f a) s ↔ ContinuousOn f s ∧ DifferentiableAt 𝕜 f a

Tactic:
⟨fun hc => ⟨hc.of_dslope, continuousAt_dslope_same.1 <| hc.continuousAt h⟩, ?_⟩

Premises used: continuousAt_dslope_same, ContinuousOn.of_dslope, And.intro, Iff.intro, Iff.mp, ContinuousOn.continuousAt
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
refine : ContinuousOn f s ∧ DifferentiableAt 𝕜 f a → ContinuousOn (dslope f a) s
⊢ ContinuousOn (dslope f a) s ↔ ContinuousOn f s ∧ DifferentiableAt 𝕜 f a

Tactic:
refine ⟨fun hc => ⟨hc.of_dslope, continuousAt_dslope_same.1 <| hc.continuousAt h⟩, ?_⟩
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
hc : ContinuousOn f s
hd : DifferentiableAt 𝕜 f a
x : 𝕜
hx : x ∈ s
inl : ∀ (h : s ∈ 𝓝 x) (hd : DifferentiableAt 𝕜 f x), ContinuousWithinAt (dslope f x) s x
inr : ∀ (hne : x ≠ a), ContinuousWithinAt (dslope f a) s x
⊢ ContinuousWithinAt (dslope f a) s x

Tactic:
rcases eq_or_ne x a with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
s : Set 𝕜
hc : ContinuousOn f s
x : 𝕜
hx : x ∈ s
h : s ∈ 𝓝 x
hd : DifferentiableAt 𝕜 f x
⊢ ContinuousWithinAt (dslope f x) s x

Tactic:
(continuousAt_dslope_same.2 hd).continuousWithinAt

Premises used: Iff.mpr, ContinuousAt.continuousWithinAt, continuousAt_dslope_same
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 a
hc : ContinuousOn f s
hd : DifferentiableAt 𝕜 f a
x : 𝕜
hx : x ∈ s
hne : x ≠ a
⊢ ContinuousWithinAt (dslope f a) s x

Tactic:
(continuousWithinAt_dslope_of_ne hne).2 (hc x hx)

Premises used: Iff.mpr, continuousWithinAt_dslope_of_ne
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
s : Set 𝕜
hc : ContinuousOn f s
x : 𝕜
hx : x ∈ s
h : s ∈ 𝓝 x
hd : DifferentiableAt 𝕜 f x
⊢ ContinuousWithinAt (dslope f x) s x

Tactic:
exacts [(continuousAt_dslope_same.2 hd).continuousWithinAt,
    (continuousWithinAt_dslope_of_ne hne).2 (hc x hx)]

Premises used: Iff.mpr, ContinuousAt.continuousWithinAt, continuousAt_dslope_same