Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: case hp_bdd
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
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
⊢ ∀ k_1 ≤ k, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ g (f x) k_1‖

pp: case hpf
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
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
⊢ ∀ k_1 ≤ k, (fun a_2 ↦ ftaylorSeries ℝ g (f a_2) k_1 - ftaylorSeries ℝ g (f a) k_1) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α

pp: case hq₁_bdd
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
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
⊢ ∀ k_1 ≤ k, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f x k_1‖

pp: case hq₂_bdd
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
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
⊢ ∀ k_1 ≤ k, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f a k_1‖

pp: case hqf
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
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
⊢ ∀ k_1 ≤ k, (fun a_2 ↦ ftaylorSeries ℝ f a_2 k_1 - ftaylorSeries ℝ f a k_1) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α

Tactic:
<;>

Goal state after:
case hp_bdd
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
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
⊢ ∀ k_1 ≤ k, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ g (f x) k_1‖

case hpf
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
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
⊢ ∀ k_1 ≤ k, (fun a_2 ↦ ftaylorSeries ℝ g (f a_2) k_1 - ftaylorSeries ℝ g (f a) k_1) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α

case hq₁_bdd
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
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
⊢ ∀ k_1 ≤ k, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f x k_1‖

case hq₂_bdd
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
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
⊢ ∀ k_1 ≤ k, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f a k_1‖

case hqf
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
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
⊢ ∀ k_1 ≤ k, (fun a_2 ↦ ftaylorSeries ℝ f a_2 k_1 - ftaylorSeries ℝ f a k_1) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α