Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
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
i : ℕ
hi : i ≤ k
⊢ (fun a_1 ↦ ftaylorSeries ℝ g (f a_1) i - ftaylorSeries ℝ g (f a) i) =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
i : ℕ
hi : i ≤ k
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f x i‖

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
i : ℕ
hi : i ≤ k
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f a i‖

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
i : ℕ
hi : i ≤ k
⊢ (fun a_1 ↦ ftaylorSeries ℝ f a_1 i - ftaylorSeries ℝ f a i) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α

Tactic:
· by_cases hfd : DifferentiableAt ℝ f a
        · refine ((hg.of_order_le hi).isBigO.comp_tendsto hf.continuousAt).trans ?_
          refine .rpow α.2.1 (.of_forall fun _ ↦ norm_nonneg _) <| .norm_norm ?_
          exact hfd.isBigO_sub
        · obtain rfl : k = 0 := by
            contrapose! hfd
            exact hf.differentiableAt hfd
          obtain rfl : i = 0 := by rwa [nonpos_iff_eq_zero] at hi
          refine .of_norm_left ?_
          simp only [ftaylorSeries, iteratedFDeriv_zero_eq_comp, Function.comp_apply, ← map_sub,
            LinearIsometryEquiv.norm_map, isBigO_norm_left]
          refine ((hd.resolve_right hfd).isBigO_sub.comp_tendsto hf.continuousAt).trans ?_
          exact (zero_order_iff.mp hf).2

Goal state after:
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
i : ℕ
hi : i ≤ k
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f x i‖

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
i : ℕ
hi : i ≤ k
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖ftaylorSeries ℝ f a i‖

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
i : ℕ
hi : i ≤ k
⊢ (fun a_1 ↦ ftaylorSeries ℝ f a_1 i - ftaylorSeries ℝ f a i) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α