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 : 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
h :
  ∀ (x_1 : (i : Fin k) → E),
    Eq (α := F × G)
      ((HSub.hSub (α := ContinuousMultilinearMap ℝ (fun (i : Fin k) ↦ E) (F × G))
              (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin k) ↦ E) (iteratedFDeriv ℝ k f x)
                (iteratedFDeriv ℝ k g x))
              (ContinuousMultilinearMap.prod (M₁ := fun (i : Fin k) ↦ E) (iteratedFDeriv ℝ k f a)
                (iteratedFDeriv ℝ k g a)) :
            (a : (i : Fin k) → E) → F × G)
          x_1 :
        F × G)
      (((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)) :
            (a : (i : Fin k) → E) → F × G)
          x_1 :
        F × G)
rw : ContDiffAt ℝ (↑k : WithTop ℕ∞) f a
⊢ ∀ (x_1 : (i : Fin k) → E),
    Eq (α := F × G)
      ((HSub.hSub (α := ContinuousMultilinearMap ℝ (fun (i : Fin k) ↦ E) (F × G))
              (iteratedFDeriv ℝ k (fun (x : E) ↦ (f x, g x)) x) (iteratedFDeriv ℝ k (fun (x : E) ↦ (f x, g x)) a) :
            (a : (i : Fin k) → E) → F × G)
          x_1 :
        F × G)
      (((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)) :
            (a : (i : Fin k) → E) → F × G)
          x_1 :
        F × G)
have rw₁ : ContDiffAt ℝ (↑k : WithTop ℕ∞) g a
Tactic: rw [iteratedFDeriv_prodMk _ _ le_rfl, iteratedFDeriv_prodMk _ _ le_rfl]
-- 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 : 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‖ ^ (↑α : ℝ)
have 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‖ ^ (↑α : ℝ)
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
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)).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‖ ^ (↑α : ℝ)
have 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‖ ^ (↑α : ℝ)
Tactic: simp only [ContinuousMultilinearMap.opNorm_prod, ← Prod.norm_mk]
-- 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
⊢ (𝓝 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)
have 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)
Tactic: filter_upwards [hf.contDiffAt.eventually (by simp),
        hf.continuousAt.eventually (hg.contDiffAt.eventually (by simp))] with x hfx hgx
-- 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
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)
have 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)
Tactic: rw [iteratedFDeriv_comp hgx hfx le_rfl,
        iteratedFDeriv_comp hg.contDiffAt hf.contDiffAt le_rfl]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [iteratedFDeriv_comp hgx hfx le_rfl,
        iteratedFDeriv_comp hg.contDiffAt hf.contDiffAt le_rfl]
-- 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
⊢ 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‖ ^ (↑α : ℝ)
have 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)
Tactic: apply FormalMultilinearSeries.taylorComp_sub_taylorComp_isBigO
-- 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
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)
⊢ 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‖ ^ (↑α : ℝ)
have 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‖ ^ (↑α : ℝ)
Tactic: apply FormalMultilinearSeries.taylorComp_sub_taylorComp_isBigO
-- 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
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‖ ^ (↑α : ℝ)
⊢ 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‖ ^ (↑α : ℝ)
have 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)
Tactic: apply FormalMultilinearSeries.taylorComp_sub_taylorComp_isBigO
-- 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
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)
⊢ 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‖ ^ (↑α : ℝ)
have 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)
Tactic: apply FormalMultilinearSeries.taylorComp_sub_taylorComp_isBigO
-- 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
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)
⊢ 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‖ ^ (↑α : ℝ)
have 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‖ ^ (↑α : ℝ)
Tactic: apply FormalMultilinearSeries.taylorComp_sub_taylorComp_isBigO
-- 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
⊢ 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 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‖ ^ (↑α : ℝ)
Tactic: by_cases hfd : DifferentiableAt ℝ f a
-- 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
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‖ ^ (↑α : ℝ)
⊢ 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 : ∀ (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: by_cases hfd : DifferentiableAt ℝ f a
-- 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
⊢ 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 pos : IsBigO (E := ℝ) (F := ℝ) (𝓝 a) ((fun (x : F) ↦ ‖x - f a‖ ^ (↑α : ℝ)) ∘ f) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
Tactic: refine ((hg.of_order_le hi).isBigO.comp_tendsto hf.continuousAt).trans ?_
-- 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
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 a) ((fun (x : F) ↦ ‖x - f a‖ ^ (↑α : ℝ)) ∘ f) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
have 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
Tactic: refine .rpow α.2.1 (.of_forall fun _ ↦ norm_nonneg _) <| .norm_norm ?_