awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ ContDiffPointwiseHolderAt 0 α g (f a)

Tactic:
obtain rfl : k = 0 := by
            contrapose! hfd
            exact hf.differentiableAt hfd

Premises used: rfl
-- 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)
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)
⊢ ContDiffPointwiseHolderAt 0 α f a

Tactic:
obtain rfl : k = 0 := by
            contrapose! hfd
            exact hf.differentiableAt hfd

Premises used: rfl
-- 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)
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
⊢ i ≤ 0

Tactic:
obtain rfl : k = 0 := by
            contrapose! hfd
            exact hf.differentiableAt hfd

Premises used: rfl
-- 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
α : (↑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
rwa rwa₁ rwa₂ rwa₃ : ∀ (hi : i = 0), i = 0
⊢ i = 0

Tactic:
rwa [nonpos_iff_eq_zero] at hi

Premises used: nonpos_iff_eq_zero
-- 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
α : (↑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
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‖ ^ (↑α : ℝ)
⊢ 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‖ ^ (↑α : ℝ)

Tactic:
obtain rfl : i = 0 := by rwa [nonpos_iff_eq_zero] at hi

Premises used: rfl
-- 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
α : (↑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‖ ^ (↑α : ℝ)

Tactic:
.of_norm_left ?_

Premises used: Asymptotics.IsBigO.of_norm_left
-- 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
α : (↑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
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‖ ^ (↑α : ℝ)
⊢ 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:
refine .of_norm_left ?_
-- 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
α : (↑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
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‖ ^ (↑α : ℝ)
⊢ 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:
simp only [ftaylorSeries, iteratedFDeriv_zero_eq_comp, Function.comp_apply, ← map_sub,
            LinearIsometryEquiv.norm_map, isBigO_norm_left]

Premises used: map_sub, LinearIsometryEquiv.norm_map, ftaylorSeries, Asymptotics.isBigO_norm_left, iteratedFDeriv_zero_eq_comp, Function.comp_apply
-- 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
α : (↑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‖ ^ (↑α : ℝ)

Tactic:
((hd.resolve_right hfd).isBigO_sub.comp_tendsto hf.continuousAt).trans ?_

Premises used: DifferentiableAt.isBigO_sub, Asymptotics.IsBigO.trans, Or.resolve_right, Asymptotics.IsBigO.comp_tendsto, ContDiffPointwiseHolderAt.continuousAt
-- 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
α : (↑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
neg : IsBigO (E := F) (F := ℝ) (𝓝 a) ((fun (x : F) ↦ x - f a) ∘ f) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
⊢ 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:
refine ((hd.resolve_right hfd).isBigO_sub.comp_tendsto hf.continuousAt).trans ?_

Premises used: DifferentiableAt.isBigO_sub, Asymptotics.IsBigO.trans, Or.resolve_right, Asymptotics.IsBigO.comp_tendsto, ContDiffPointwiseHolderAt.continuousAt
-- 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
α : (↑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) (F := ℝ) (𝓝 a) ((fun (x : F) ↦ x - f a) ∘ f) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
(zero_order_iff.mp hf).2

Premises used: And.right, Iff.mp, ContDiffPointwiseHolderAt.zero_order_iff
-- 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
α : (↑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) (F := ℝ) (𝓝 a) ((fun (x : F) ↦ x - f a) ∘ f) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
exact (zero_order_iff.mp hf).2

Premises used: And.right, Iff.mp, ContDiffPointwiseHolderAt.zero_order_iff
-- 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)
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
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 a) fun (x : E) ↦
    norm (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin i) ↦ E) F) (ftaylorSeries ℝ f x i)

Tactic:
(hf.contDiffAt.continuousAt_iteratedFDeriv (mod_cast hi)).norm.isBoundedUnder_le

Premises used: Filter.Tendsto.isBoundedUnder_le, ftaylorSeries, ContDiffPointwiseHolderAt.contDiffAt, ContinuousAt.norm, ContDiffAt.continuousAt_iteratedFDeriv
-- 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)
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
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 a) fun (x : E) ↦
    norm (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin i) ↦ E) F) (ftaylorSeries ℝ f x i)

Tactic:
exact (hf.contDiffAt.continuousAt_iteratedFDeriv (mod_cast hi)).norm.isBoundedUnder_le

Premises used: Filter.Tendsto.isBoundedUnder_le, ContDiffPointwiseHolderAt.contDiffAt, ContinuousAt.norm, ContDiffAt.continuousAt_iteratedFDeriv
-- 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)
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
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 a) fun (x : E) ↦
    norm (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin i) ↦ E) F) (ftaylorSeries ℝ f a i)

Tactic:
isBoundedUnder_const

Premises used: Filter.isBoundedUnder_const
-- 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)
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
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 a) fun (x : E) ↦
    norm (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin i) ↦ E) F) (ftaylorSeries ℝ f a i)

Tactic:
exact isBoundedUnder_const

Premises used: Filter.isBoundedUnder_const
-- 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)
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
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin i) ↦ E) F) (F := ℝ) (𝓝 a)
    (fun (a_1 : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin i) ↦ E) F) (ftaylorSeries ℝ f a_1 i)
        (ftaylorSeries ℝ f a i))
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
(hf.of_order_le hi).isBigO

Premises used: ContDiffPointwiseHolderAt.isBigO, ContDiffPointwiseHolderAt.of_order_le
-- 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)
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
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin i) ↦ E) F) (F := ℝ) (𝓝 a)
    (fun (a_1 : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin i) ↦ E) F) (ftaylorSeries ℝ f a_1 i)
        (ftaylorSeries ℝ f a i))
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
exact (hf.of_order_le hi).isBigO

Premises used: ContDiffPointwiseHolderAt.isBigO, ContDiffPointwiseHolderAt.of_order_le
-- 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)
f : E → F
a : E
g : F → G
hg : ContDiffPointwiseHolderAt k α g (f a)
hf : ContDiffPointwiseHolderAt k α f a
hk : k ≠ 0
⊢ ContDiffPointwiseHolderAt k α (g ∘ f) a

Tactic:
hg.comp_of_differentiableAt a hf (.inl <| hg.differentiableAt hk)

Premises used: ContDiffPointwiseHolderAt.comp_of_differentiableAt, ContDiffPointwiseHolderAt.differentiableAt, Or.inl
-- 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
H : Type u_4
inst_6 : NormedAddCommGroup H
inst_7 : NormedSpace ℝ H
g : F × G → H
f₁ : E → F
f₂ : E → G
hg : ContDiffPointwiseHolderAt k α g (f₁ a, f₂ a)
hf₁ : ContDiffPointwiseHolderAt k α f₁ a
hf₂ : ContDiffPointwiseHolderAt k α f₂ a
hdiff : DifferentiableAt ℝ g (f₁ a, f₂ a) ∨ DifferentiableAt ℝ f₁ a ∧ DifferentiableAt ℝ f₂ a
⊢ ContDiffPointwiseHolderAt.{u_1, u_4} (F := H) k α (fun (x : E) ↦ g (f₁ x, f₂ x)) a

Tactic:
hg.comp_of_differentiableAt a (hf₁.prodMk hf₂) <| hdiff.imp_right fun h ↦
    h.left.prodMk h.right

Premises used: ContDiffPointwiseHolderAt.comp_of_differentiableAt, ContDiffPointwiseHolderAt.prodMk, Or.imp_right
-- 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)
a : E
f : E →L[ℝ] F
⊢ ContDiffPointwiseHolderAt.{u_1, u_2} (F := F) k α (⇑f : (a : E) → F) a

Tactic:
f.contDiff.contDiffAt.contDiffPointwiseHolderAt (WithTop.coe_lt_top _) _

Premises used: WithTop.coe_lt_top, ContDiffAt.contDiffPointwiseHolderAt, ContinuousLinearMap.contDiff, ContDiff.contDiffAt
-- 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)
a : E
f : E ≃L[ℝ] F
⊢ ContDiffPointwiseHolderAt.{u_1, u_2} (F := F) k α (⇑f : (a : E) → F) a

Tactic:
f.toContinuousLinearMap.contDiffPointwiseHolderAt

Premises used: ContinuousLinearMap.contDiffPointwiseHolderAt, ContinuousLinearEquiv.toContinuousLinearMap
-- 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)
f : E → F
a : E
hf : ContDiffPointwiseHolderAt k α f a
g : F →L[ℝ] G
⊢ ContDiffPointwiseHolderAt.{u_1, u_3} (F := G) k α ((⇑g : (a : F) → G) ∘ f) a

Tactic:
g.contDiffPointwiseHolderAt.comp_of_differentiableAt a hf <| .inl g.differentiableAt

Premises used: ContDiffPointwiseHolderAt.comp_of_differentiableAt, ContinuousLinearMap.contDiffPointwiseHolderAt, ContinuousLinearMap.differentiableAt, Or.inl
-- 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)
f : E → F
a : E
g : F ≃L[ℝ] G
h : ContDiffPointwiseHolderAt.{u_1, u_3} (F := G) k α ((⇑g : (a : F) → G) ∘ f) a
⊢ ContDiffPointwiseHolderAt k α f a

Tactic:
simpa [Function.comp_def] using h.continuousLinearMap_comp (g.symm : G →L[ℝ] F)

Premises used: ContinuousLinearEquiv.symm, ContDiffPointwiseHolderAt.continuousLinearMap_comp, Function.comp_def, ContinuousLinearEquiv.toContinuousLinearMap
-- 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)
f : E → F
a : E
g : F ≃ₗᵢ[ℝ] G
⊢ ContDiffPointwiseHolderAt.{u_1, u_3} (F := G) k α ((⇑g : (a : F) → G) ∘ f) a ↔ ContDiffPointwiseHolderAt k α f a

Tactic:
g.toContinuousLinearEquiv.contDiffPointwiseHolderAt_left_comp

Premises used: LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.contDiffPointwiseHolderAt_left_comp
-- Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
k : ℕ
α : (↑I : Type)
a : E
⊢ ContDiffPointwiseHolderAt k α id a

Tactic:
ContinuousLinearMap.id ℝ E |>.contDiffPointwiseHolderAt

Premises used: Real, ContinuousLinearMap.contDiffPointwiseHolderAt, ContinuousLinearMap.id
-- 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)
a : E
b : F
⊢ ContDiffPointwiseHolderAt k α (Function.const E b) a

Tactic:
contDiffAt_const.contDiffPointwiseHolderAt (WithTop.coe_lt_top _) α

Premises used: WithTop.coe_lt_top, ContDiffAt.contDiffPointwiseHolderAt, contDiffAt_const
-- 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 : ℕ
α : (↑I : Type)
f : E → F
a : E
hf : ContDiffPointwiseHolderAt k α f a
hl : l < k
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      ‖HSub.hSub (α := ContinuousMultilinearMap ℝ (fun (i : Fin l) ↦ E) (E →L[ℝ] F)) (iteratedFDeriv ℝ l (fderiv ℝ f) x)
          (iteratedFDeriv ℝ l (fderiv ℝ f) a)‖)
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
simpa [iteratedFDeriv_succ_eq_comp_right, Function.comp_def, ← dist_eq_norm_sub]
      using hf.of_order_le (Nat.add_one_le_iff.mpr hl) |>.isBigO |>.norm_left

Premises used: Iff.mpr, Asymptotics.IsBigO.norm_left, ContDiffPointwiseHolderAt.isBigO, dist_eq_norm_sub, Function.comp_def, Nat.add_one_le_iff, iteratedFDeriv_succ_eq_comp_right, 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
hf : ContDiffPointwiseHolderAt k α f a
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:
simpa +unfoldPartialApp [iteratedFDeriv_zero_eq_comp] using hf.of_order_le hl

Premises used: iteratedFDeriv_zero_eq_comp, 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
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
⊢ l + 1 + m ≤ k

Tactic:
rw [← add_assoc, add_right_comm] at hl

Premises used: add_assoc, add_right_comm