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 : E → G
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
x : E
hfx : ContDiffAt ℝ (↑k : WithTop ℕ∞) f x
hgx : ContDiffAt ℝ (↑k : WithTop ℕ∞) g x
⊢ ContDiffAt ℝ (↑k : WithTop ℕ∞) g x

Tactic:
simp [hfx, hgx, hf.contDiffAt, hg.contDiffAt]

Premises used: ContDiffPointwiseHolderAt.contDiffAt
-- 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 : E → G
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
⊢ IsBigO (E := ContinuousMultilinearMap ℝ (fun (i : Fin k) ↦ E) (F × G)) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      (HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k f x)
            (iteratedFDeriv ℝ k f a)).prod
        (M₁ := fun (i : Fin k) ↦ E)
        (HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G) (iteratedFDeriv ℝ k g x)
          (iteratedFDeriv ℝ k g a)))
    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
k : ℕ
α : (↑I : Type)
f : E → F
a : E
g : E → G
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
refine :
  IsBigO (E := ℝ) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      ‖(HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k f x)
              (iteratedFDeriv ℝ k f a)).prod
          (M₁ := fun (i : Fin k) ↦ E)
          (HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G) (iteratedFDeriv ℝ k g x)
            (iteratedFDeriv ℝ k g a))‖)
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
⊢ IsBigO (E := ContinuousMultilinearMap ℝ (fun (i : Fin k) ↦ E) (F × G)) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      (HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k f x)
            (iteratedFDeriv ℝ k f a)).prod
        (M₁ := fun (i : Fin k) ↦ E)
        (HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G) (iteratedFDeriv ℝ k g x)
          (iteratedFDeriv ℝ k g a)))
    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
k : ℕ
α : (↑I : Type)
f : E → F
a : E
g : E → G
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
simp :
  IsBigO (E := ℝ) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      ‖(HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k f x)
            (iteratedFDeriv ℝ k f a),
          HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G) (iteratedFDeriv ℝ k g x)
            (iteratedFDeriv ℝ k g a))‖)
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      ‖(HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k f x)
              (iteratedFDeriv ℝ k f a)).prod
          (M₁ := fun (i : Fin k) ↦ E)
          (HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G) (iteratedFDeriv ℝ k g x)
            (iteratedFDeriv ℝ k g a))‖)
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
simp only [ContinuousMultilinearMap.opNorm_prod, ← Prod.norm_mk]

Premises used: Prod.norm_mk, ContinuousMultilinearMap.opNorm_prod
-- 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 : E → G
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      ‖(HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k f x)
            (iteratedFDeriv ℝ k f a),
          HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G) (iteratedFDeriv ℝ k g x)
            (iteratedFDeriv ℝ k g a))‖)
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
(hf.isBigO.prod_left hg.isBigO).norm_left

Premises used: Asymptotics.IsBigO.norm_left, ContDiffPointwiseHolderAt.isBigO, Asymptotics.IsBigO.prod_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
k : ℕ
α : (↑I : Type)
f : E → F
a : E
g : E → G
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      ‖(HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (iteratedFDeriv ℝ k f x)
            (iteratedFDeriv ℝ k f a),
          HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G) (iteratedFDeriv ℝ k g x)
            (iteratedFDeriv ℝ k g a))‖)
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
exact (hf.isBigO.prod_left hg.isBigO).norm_left

Premises used: Asymptotics.IsBigO.norm_left, ContDiffPointwiseHolderAt.isBigO, Asymptotics.IsBigO.prod_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
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
⊢ Ne (α := WithTop ℕ∞) (↑k : WithTop ℕ∞) (↑⊤ : WithTop ℕ∞)

Tactic:
simp
-- 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
h :
  ∀ (x : E) (hfx : ContDiffAt ℝ (↑k : WithTop ℕ∞) f x) (hgx : ContDiffAt ℝ (↑k : WithTop ℕ∞) g (f x)),
    HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G) (iteratedFDeriv ℝ k (g ∘ f) x)
        (iteratedFDeriv ℝ k (g ∘ f) a) =
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G)
        (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f x)) (ftaylorSeries ℝ f x) k)
        (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f a)) (ftaylorSeries ℝ f a) k)
⊢ (𝓝 a).EventuallyEq (β := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G)
    (fun (x : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G)
        (iteratedFDeriv ℝ k (g ∘ f) x) (iteratedFDeriv ℝ k (g ∘ f) a))
    fun (x : E) ↦
    HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G)
      (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f x)) (ftaylorSeries ℝ f x) k)
      (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f a)) (ftaylorSeries ℝ f a) k)

Tactic:
filter_upwards [hf.contDiffAt.eventually (by simp),
        hf.continuousAt.eventually (hg.contDiffAt.eventually (by simp))] with x hfx hgx

Premises used: Filter.Tendsto.eventually, ContDiffPointwiseHolderAt.contDiffAt, ContDiffAt.eventually, 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
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
x : E
hfx : ContDiffAt ℝ (↑k : WithTop ℕ∞) f x
hgx : ContDiffAt ℝ (↑k : WithTop ℕ∞) g (f x)
h :
  HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G)
      (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f x)) (ftaylorSeries ℝ f x) k)
      (iteratedFDeriv ℝ k (g ∘ f) a) =
    HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G)
      (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f x)) (ftaylorSeries ℝ f x) k)
      (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f a)) (ftaylorSeries ℝ f a) k)
h₁ h₂ :
  HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G)
      (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f x)) (ftaylorSeries ℝ f x) k)
      (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f a)) (ftaylorSeries ℝ f a) k) =
    HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G)
      (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f x)) (ftaylorSeries ℝ f x) k)
      (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f a)) (ftaylorSeries ℝ f a) k)
⊢ HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G) (iteratedFDeriv ℝ k (g ∘ f) x)
      (iteratedFDeriv ℝ k (g ∘ f) a) =
    HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G)
      (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f x)) (ftaylorSeries ℝ f x) k)
      (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f a)) (ftaylorSeries ℝ f a) k)

Tactic:
rw [iteratedFDeriv_comp hgx hfx le_rfl,
        iteratedFDeriv_comp hg.contDiffAt hf.contDiffAt le_rfl]

Premises used: iteratedFDeriv_comp, le_rfl, ContDiffPointwiseHolderAt.contDiffAt
-- 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
hp_bdd :
  ∀ k_1 ≤ k,
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 a) fun (x : E) ↦
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin k_1) ↦ F) G) (ftaylorSeries ℝ g (f x) k_1)
hpf :
  ∀ k_1 ≤ k,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin k_1) ↦ F) G) (F := ℝ) (𝓝 a)
      (fun (a_2 : E) ↦
        HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin k_1) ↦ F) G)
          (ftaylorSeries ℝ g (f a_2) k_1) (ftaylorSeries ℝ g (f a) k_1))
      fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
hq₁_bdd :
  ∀ k_1 ≤ k,
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 a) fun (x : E) ↦
      norm (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k_1) ↦ E) F) (ftaylorSeries ℝ f x k_1)
hq₂_bdd :
  ∀ k_1 ≤ k,
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 a) fun (x : E) ↦
      norm (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k_1) ↦ E) F) (ftaylorSeries ℝ f a k_1)
hqf :
  ∀ k_1 ≤ k,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k_1) ↦ E) F) (F := ℝ) (𝓝 a)
      (fun (a_2 : E) ↦
        HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k_1) ↦ E) F)
          (ftaylorSeries ℝ f a_2 k_1) (ftaylorSeries ℝ f a k_1))
      fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G) (F := ℝ) (𝓝 a)
    (fun (x : E) ↦
      HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_3} ℝ (fun (i : Fin k) ↦ E) G)
        (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f x)) (ftaylorSeries ℝ f x) k)
        (FormalMultilinearSeries.taylorComp (ftaylorSeries ℝ g (f a)) (ftaylorSeries ℝ f a) k))
    fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
apply FormalMultilinearSeries.taylorComp_sub_taylorComp_isBigO

Premises used: FormalMultilinearSeries.taylorComp_sub_taylorComp_isBigO
-- 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_2, u_3} ℝ (fun (i : Fin i) ↦ F) G) (ftaylorSeries ℝ g (f x) i)

Tactic:
((hg.contDiffAt.continuousAt_iteratedFDeriv (mod_cast hi)).comp hf.continuousAt)
          |>.norm.isBoundedUnder_le

Premises used: Filter.Tendsto.isBoundedUnder_le, ftaylorSeries, ContinuousAt.comp, ContDiffPointwiseHolderAt.contDiffAt, ContinuousAt.norm, iteratedFDeriv, ContDiffAt.continuousAt_iteratedFDeriv, 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
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_2, u_3} ℝ (fun (i : Fin i) ↦ F) G) (ftaylorSeries ℝ g (f x) i)

Tactic:
exact ((hg.contDiffAt.continuousAt_iteratedFDeriv (mod_cast hi)).comp hf.continuousAt)
          |>.norm.isBoundedUnder_le

Premises used: Filter.Tendsto.isBoundedUnder_le, ContinuousAt.comp, ContDiffPointwiseHolderAt.contDiffAt, ContinuousAt.norm, ContDiffAt.continuousAt_iteratedFDeriv, 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
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
pos :
  ∀ (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‖ ^ (↑α : ℝ)
neg :
  ∀ (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‖ ^ (↑α : ℝ)
⊢ 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:
by_cases hfd : DifferentiableAt ℝ f a

Premises used: Real, DifferentiableAt
-- 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
⊢ 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:
((hg.of_order_le hi).isBigO.comp_tendsto hf.continuousAt).trans ?_

Premises used: ContDiffPointwiseHolderAt.isBigO, Asymptotics.IsBigO.trans, Asymptotics.IsBigO.comp_tendsto, ContDiffPointwiseHolderAt.continuousAt, 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
hfd : DifferentiableAt ℝ f a
pos : IsBigO (E := ℝ) (F := ℝ) (𝓝 a) ((fun (x : F) ↦ ‖x - f a‖ ^ (↑α : ℝ)) ∘ f) 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:
refine ((hg.of_order_le hi).isBigO.comp_tendsto hf.continuousAt).trans ?_

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

Tactic:
.rpow α.2.1 (.of_forall fun _ ↦ norm_nonneg _) <| .norm_norm ?_

Premises used: HSub.hSub, Asymptotics.IsBigO.norm_norm, Filter.Eventually.of_forall, And.left, Asymptotics.IsBigO.rpow, norm_nonneg, Subtype.property
-- 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
pos : IsBigO.{u_1, u_2, u_1} (E := F) (F := E) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ x - a
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 a) ((fun (x : F) ↦ ‖x - f a‖ ^ (↑α : ℝ)) ∘ f) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
refine .rpow α.2.1 (.of_forall fun _ ↦ norm_nonneg _) <| .norm_norm ?_
-- 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
⊢ IsBigO.{u_1, u_2, u_1} (E := F) (F := E) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ x - a

Tactic:
hfd.isBigO_sub

Premises used: DifferentiableAt.isBigO_sub
-- 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
⊢ IsBigO.{u_1, u_2, u_1} (E := F) (F := E) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ x - a

Tactic:
exact hfd.isBigO_sub

Premises used: DifferentiableAt.isBigO_sub
-- 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
contrapose! : ∀ (hfd : k ≠ 0), DifferentiableAt ℝ f a
⊢ k = 0

Tactic:
contrapose! hfd
-- 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 : k ≠ 0
⊢ DifferentiableAt ℝ f a

Tactic:
hf.differentiableAt hfd

Premises used: ContDiffPointwiseHolderAt.differentiableAt
-- 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 : k ≠ 0
⊢ DifferentiableAt ℝ f a

Tactic:
exact hf.differentiableAt hfd

Premises used: ContDiffPointwiseHolderAt.differentiableAt