awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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)
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hi : i ≤ k
hfd : ¬DifferentiableAt ℝ f a
⊢ k = 0
have contrapose! : ∀ (hfd : k ≠ 0), DifferentiableAt ℝ f a
Tactic: contrapose! hfd
Cleared hypotheses: hfd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (hypothesis)
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)
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hi : i ≤ k
hfd : ¬DifferentiableAt ℝ f a
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ F) G) (F := ℝ) (𝓝 a)
    (fun (a_1 : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ F) G) (ftaylorSeries ℝ g (f a_1) i)
        (ftaylorSeries ℝ g (f a) i))
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
have hg₁ : ContDiffPointwiseHolderAt 0 α g (f a)
Tactic: obtain rfl : k = 0 := by
            contrapose! hfd
            exact hf.differentiableAt hfd
Cleared hypotheses: k, hg, hf, hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (hypothesis)
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)
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hi : i ≤ k
hfd : ¬DifferentiableAt ℝ f a
hg₁ : ContDiffPointwiseHolderAt 0 α g (f a)
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ F) G) (F := ℝ) (𝓝 a)
    (fun (a_1 : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ F) G) (ftaylorSeries ℝ g (f a_1) i)
        (ftaylorSeries ℝ g (f a) i))
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
have hf₁ : ContDiffPointwiseHolderAt 0 α f a
Tactic: obtain rfl : k = 0 := by
            contrapose! hfd
            exact hf.differentiableAt hfd
Cleared hypotheses: k, hg, hf, hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (hypothesis)
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)
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hi : i ≤ k
hfd : ¬DifferentiableAt ℝ f a
hg₁ : ContDiffPointwiseHolderAt 0 α g (f a)
hf₁ : ContDiffPointwiseHolderAt 0 α f a
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ F) G) (F := ℝ) (𝓝 a)
    (fun (a_1 : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ F) G) (ftaylorSeries ℝ g (f a_1) i)
        (ftaylorSeries ℝ g (f a) i))
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
have hi₁ : i ≤ 0
Tactic: obtain rfl : k = 0 := by
            contrapose! hfd
            exact hf.differentiableAt hfd
Cleared hypotheses: k, hg, hf, hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
α : (↑I : Type)
f : E → F
a : E
g : F → G
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hfd : ¬DifferentiableAt ℝ f a
hg : ContDiffPointwiseHolderAt 0 α g (f a)
hf : ContDiffPointwiseHolderAt 0 α f a
hi : i ≤ 0
⊢ i = 0
have rwa : ∀ (hi : i = 0), i = 0
Tactic: rwa [nonpos_iff_eq_zero] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
α : (↑I : Type)
f : E → F
a : E
g : F → G
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hfd : ¬DifferentiableAt ℝ f a
hg : ContDiffPointwiseHolderAt 0 α g (f a)
hf : ContDiffPointwiseHolderAt 0 α f a
hi : i ≤ 0
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ F) G) (F := ℝ) (𝓝 a)
    (fun (a_1 : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ F) G) (ftaylorSeries ℝ g (f a_1) i)
        (ftaylorSeries ℝ g (f a) i))
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
have neg : ∀ (hi : LE.le (α := ℕ) 0 0),
  IsBigO (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ F) G) (F := ℝ) (𝓝 a)
    (fun (a_1 : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ F) G) (ftaylorSeries ℝ g (f a_1) 0)
        (ftaylorSeries ℝ g (f a) 0))
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
Tactic: obtain rfl : i = 0 := by rwa [nonpos_iff_eq_zero] at hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
α : (↑I : Type)
f : E → F
a : E
g : F → G
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
hfd : ¬DifferentiableAt ℝ f a
hg : ContDiffPointwiseHolderAt 0 α g (f a)
hf : ContDiffPointwiseHolderAt 0 α f a
hi : LE.le (α := ℕ) 0 0
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ F) G) (F := ℝ) (𝓝 a)
    (fun (a_1 : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ F) G) (ftaylorSeries ℝ g (f a_1) 0)
        (ftaylorSeries ℝ g (f a) 0))
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
have neg : IsBigO (E := ℝ) (F := ℝ) (𝓝 a)
  (fun (x : E) ↦
    ‖HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ F) G) (ftaylorSeries ℝ g (f x) 0)
        (ftaylorSeries ℝ g (f a) 0)‖)
  fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
Tactic: refine .of_norm_left ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
α : (↑I : Type)
f : E → F
a : E
g : F → G
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
hfd : ¬DifferentiableAt ℝ f a
hg : ContDiffPointwiseHolderAt 0 α g (f a)
hf : ContDiffPointwiseHolderAt 0 α f a
hi : LE.le (α := ℕ) 0 0
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      ‖HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ F) G) (ftaylorSeries ℝ g (f x) 0)
          (ftaylorSeries ℝ g (f a) 0)‖)
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
have neg : IsBigO.{u_1, u_3, 0} (E := G) (F := ℝ) (𝓝 a) (fun (x : E) ↦ g (f x) - g (f a)) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
Tactic: simp only [ftaylorSeries, iteratedFDeriv_zero_eq_comp, Function.comp_apply, ← map_sub,
            LinearIsometryEquiv.norm_map, isBigO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
α : (↑I : Type)
f : E → F
a : E
g : F → G
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
hfd : ¬DifferentiableAt ℝ f a
hg : ContDiffPointwiseHolderAt 0 α g (f a)
hf : ContDiffPointwiseHolderAt 0 α f a
hi : LE.le (α := ℕ) 0 0
⊢ IsBigO.{u_1, u_3, 0} (E := G) (F := ℝ) (𝓝 a) (fun (x : E) ↦ g (f x) - g (f a)) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
have neg : IsBigO (E := F) (F := ℝ) (𝓝 a) ((fun (x : F) ↦ x - f a) ∘ f) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
Tactic: refine ((hd.resolve_right hfd).isBigO_sub.comp_tendsto hf.continuousAt).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (hypothesis)
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 + (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
have hl₁ : l + 1 + m ≤ k
Tactic: rw [← add_assoc, add_right_comm] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
⊢ ContDiffPointwiseHolderAt (F := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin (m + 1)) ↦ E) F) l α
    (iteratedFDeriv ℝ (m + 1) f) a
have 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
Tactic: simpa +unfoldPartialApp [iteratedFDeriv_succ_eq_comp_left] using (ihm hl).fderiv l.lt_add_one
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
⊢ ContDiffPointwiseHolderAt (F := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin m) ↦ E) F) l α
    (iteratedFDeriv ℝ m f) a
have 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
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
Cleared hypotheses: l, m, hl
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
⊢ ContDiffPointwiseHolderAt (F := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin m) ↦ E) F) l α
    (iteratedFDeriv ℝ m f) a
have 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
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
Cleared hypotheses: l, m, hl
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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‖ ^ (↑α : ℝ)
have refine_1 : (𝓝 a).EventuallyEq (β := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k g)
  (iteratedFDeriv ℝ k f)
Tactic: refine EventuallyEq.trans_isBigO (.sub ?_ ?_) hf.isBigO
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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)
⊢ 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‖ ^ (↑α : ℝ)
have 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
Tactic: refine EventuallyEq.trans_isBigO (.sub ?_ ?_) hf.isBigO
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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)
    (fun (x : E) ↦ iteratedFDeriv ℝ k g a) fun (x : E) ↦ iteratedFDeriv ℝ k f a
have 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
Tactic: rw [hfg.symm.iteratedFDeriv ℝ _ |>.self_of_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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
⊢ Eq.{u_3 + 1} (α := F) (dslope ((⇑f : (a : E) → F) ∘ g) a b : F) ((f : (a : E) → F) (dslope g a b) : F)
have 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)
Tactic: rcases eq_or_ne b a with (rfl | hne)
Cleared hypotheses: a, H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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)
⊢ Eq.{u_3 + 1} (α := F) (dslope ((⇑f : (a : E) → F) ∘ g) a b : F) ((f : (a : E) → F) (dslope g a b) : F)
have 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)
Tactic: rcases eq_or_ne b a with (rfl | hne)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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) (dslope ((⇑f : (a : E) → F) ∘ g) b b : F) ((f : (a : E) → F) (dslope g b b) : F)
have inl : Eq.{u_3 + 1} (α := F) (deriv ((⇑f : (a : E) → F) ∘ g) b : F) ((f : (a : E) → F) (deriv g b) : F)
Tactic: simp only [dslope_same]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
⊢ (b - a) • dslope f a b = f b - f a
have inl : (b - b) • dslope f b b = f b - f b
Tactic: rcases eq_or_ne b a with (rfl | hne)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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
⊢ (b - a) • dslope f a b = f b - f a
have inr : ∀ (hne : b ≠ a), (b - a) • dslope f a b = f b - f a
Tactic: rcases eq_or_ne b a with (rfl | hne)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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 (fun (x : 𝕜) ↦ (x - a) • f x) a b = f b
have rw : slope (PE := E) (fun (x : 𝕜) ↦ (x - a) • f x) a b = f b
Tactic: rw [dslope_of_ne _ h, slope_sub_smul _ h.symm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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
⊢ dslope (fun (x : 𝕜) ↦ (x - a) • f x) a b = f b
have rw₁ : f b = f b
Tactic: rw [dslope_of_ne _ h, slope_sub_smul _ h.symm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (hypothesis)
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 f s b
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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
have refine : ∀ (hc : ContinuousWithinAt f s b), ContinuousWithinAt (dslope f a) s b
Tactic: refine ⟨ContinuousWithinAt.of_dslope, fun hc => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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 (dslope f a) s b
have simp : ContinuousWithinAt (slope f a) s b
Tactic: simp only [dslope, continuousWithinAt_update_of_ne h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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 (dslope f a) s b
have simp : ContinuousWithinAt (slope 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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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
have refine : ContinuousOn f s ∧ DifferentiableAt 𝕜 f a → ContinuousOn (dslope f a) s
Tactic: refine ⟨fun hc => ⟨hc.of_dslope, continuousAt_dslope_same.1 <| hc.continuousAt h⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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
⊢ ContinuousWithinAt (dslope f a) s x
have inl : ∀ (h : s ∈ 𝓝 x) (hd : DifferentiableAt 𝕜 f x), ContinuousWithinAt (dslope f x) s x
Tactic: rcases eq_or_ne x a with (rfl | hne)
Cleared hypotheses: a, h, hd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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
⊢ ContinuousWithinAt (dslope f a) s x
have inr : ∀ (hne : x ≠ a), ContinuousWithinAt (dslope f a) s x
Tactic: rcases eq_or_ne x a with (rfl | hne)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b ↔ DifferentiableWithinAt 𝕜 f s b
have refine : ∀ (hd : DifferentiableWithinAt 𝕜 f s b), DifferentiableWithinAt 𝕜 (dslope f a) s b
Tactic: refine ⟨DifferentiableWithinAt.of_dslope, fun hd => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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
hd : DifferentiableWithinAt 𝕜 f s b
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b
have refine : dslope f a =ᶠ[𝓝[s] b] HSMul.hSMul (α := 𝕜 → 𝕜) (β := 𝕜 → E) (fun (y : 𝕜) ↦ id y - a)⁻¹ fun (y : 𝕜) ↦ f y - f a
Tactic: refine (((differentiableWithinAt_id.sub_const a).inv (sub_ne_zero.2 h)).smul
    (hd.sub_const (f a))).congr_of_eventuallyEq ?_ (dslope_of_ne _ h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
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
hd : DifferentiableWithinAt 𝕜 f s b
⊢ dslope f a =ᶠ[𝓝[s] b] HSMul.hSMul (α := 𝕜 → 𝕜) (β := 𝕜 → E) (fun (y : 𝕜) ↦ id y - a)⁻¹ fun (y : 𝕜) ↦ f y - f a
have refine : {a}ᶜ ∈ 𝓝[s] b
Tactic: refine (eqOn_dslope_slope _ _).eventuallyEq_of_mem ?_