awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
α : (↑I : Type)
f : E → F
a : E
simp :
  ContDiffAt ℝ 0 f a →
    ((IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin 0) ↦ E) F) (F := ℝ) (𝓝 a)
        (fun (x : E) ↦
          HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv ℝ 0 f x)
            (iteratedFDeriv ℝ 0 f a))
        fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)) ↔
      IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ))
⊢ ContDiffPointwiseHolderAt 0 α f a ↔
    ContDiffAt ℝ 0 f a ∧
      IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
simp only [contDiffPointwiseHolderAt_iff, Nat.cast_zero, and_congr_right_iff]

Premises used: contDiffPointwiseHolderAt_iff, and_congr_right_iff, Nat.cast_zero
-- 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
α : (↑I : Type)
f : E → F
a : E
hfc : ContDiffAt ℝ 0 f a
simp :
  (IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin 0) ↦ E) F) (F := ℝ) (𝓝 a)
      (fun (x : E) ↦
        (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 ℝ E F) :
            (a : F) → ContinuousMultilinearMap ℝ (fun (i : Fin 0) ↦ E) F)
          (f x - f a))
      fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)) ↔
    IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
⊢ (IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin 0) ↦ E) F) (F := ℝ) (𝓝 a)
      (fun (x : E) ↦
        HSub.hSub (α := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv ℝ 0 f x)
          (iteratedFDeriv ℝ 0 f a))
      fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)) ↔
    IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
simp only [iteratedFDeriv_zero_eq_comp, Function.comp_def, ← map_sub]

Premises used: map_sub, Function.comp_def, iteratedFDeriv_zero_eq_comp
-- 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
α : (↑I : Type)
f : E → F
a : E
hfc : ContDiffAt ℝ 0 f a
rw :
  (IsBigO (E := ℝ) (F := ℝ) (𝓝 a)
      (fun (x : E) ↦
        norm (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin 0) ↦ E) F)
          ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 ℝ E F) :
                (a : F) → ContinuousMultilinearMap ℝ (fun (i : Fin 0) ↦ E) F)
              (f x - f a) :
            ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin 0) ↦ E) F))
      fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)) ↔
    IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
⊢ (IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin 0) ↦ E) F) (F := ℝ) (𝓝 a)
      (fun (x : E) ↦
        (LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 ℝ E F) :
            (a : F) → ContinuousMultilinearMap ℝ (fun (i : Fin 0) ↦ E) F)
          (f x - f a))
      fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)) ↔
    IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
rw [← isBigO_norm_left]

Premises used: Asymptotics.isBigO_norm_left
-- 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
α : (↑I : Type)
f : E → F
a : E
hfc : ContDiffAt ℝ 0 f a
simp_rw :
  (IsBigO (E := ℝ) (F := ℝ) (𝓝 a) (fun (x : E) ↦ ‖f x - f a‖) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)) ↔
    IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)
⊢ (IsBigO (E := ℝ) (F := ℝ) (𝓝 a)
      (fun (x : E) ↦
        norm (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin 0) ↦ E) F)
          ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 ℝ E F) :
                (a : F) → ContinuousMultilinearMap ℝ (fun (i : Fin 0) ↦ E) F)
              (f x - f a) :
            ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin 0) ↦ E) F))
      fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)) ↔
    IsBigO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 a) (fun (x : E) ↦ f x - f a) fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)

Tactic:
simp_rw [LinearIsometryEquiv.norm_map, isBigO_norm_left]

Premises used: LinearIsometryEquiv.norm_map, Asymptotics.isBigO_norm_left
-- 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
hle : β ≤ α
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 a) (fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)) fun (x : E) ↦ ‖x - a‖ ^ (↑β : ℝ)

Tactic:
.comp_tendsto (.rpow_rpow_nhdsGE_zero_of_le_of_imp hle fun hα ↦ ?_) ?_

Premises used: Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le_of_imp, Asymptotics.IsBigO.comp_tendsto
-- 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
hle : β ≤ α
refine_1 : ∀ (hα : (↑α : ℝ) = 0), (↑β : ℝ) = 0
refine_2 : Tendsto (β := ℝ) (fun (x : E) ↦ ‖x - a‖) (𝓝 a) (𝓝[≥] 0)
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 a) (fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)) fun (x : E) ↦ ‖x - a‖ ^ (↑β : ℝ)

Tactic:
refine .comp_tendsto (.rpow_rpow_nhdsGE_zero_of_le_of_imp hle fun hα ↦ ?_) ?_
-- 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
hle : β ≤ α
hα : (↑α : ℝ) = 0
⊢ (↑β : ℝ) = 0

Tactic:
le_antisymm (le_trans (mod_cast hle) hα.le) β.2.1

Premises used: Eq.le, le_antisymm, And.left, Subtype.property, le_trans
-- 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
hle : β ≤ α
hα : (↑α : ℝ) = 0
⊢ (↑β : ℝ) = 0

Tactic:
exact le_antisymm (le_trans (mod_cast hle) hα.le) β.2.1

Premises used: Eq.le, le_antisymm, And.left, Subtype.property, le_trans
-- 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
hle : β ≤ α
⊢ Tendsto (β := ℝ) (fun (x : E) ↦ ‖x - a‖) (𝓝 a) (𝓝[≥] 0)

Tactic:
tendsto_norm_sub_self_nhdsGE a

Premises used: tendsto_norm_sub_self_nhdsGE
-- 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
hle : β ≤ α
⊢ Tendsto (β := ℝ) (fun (x : E) ↦ ‖x - a‖) (𝓝 a) (𝓝[≥] 0)

Tactic:
exact tendsto_norm_sub_self_nhdsGE a

Premises used: tendsto_norm_sub_self_nhdsGE
-- 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
hlt : l < k
⊢ ContDiffPointwiseHolderAt l β f a

Tactic:
hf.contDiffAt.contDiffPointwiseHolderAt (mod_cast hlt) _

Premises used: ContDiffAt.contDiffPointwiseHolderAt, ContDiffPointwiseHolderAt.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
l : ℕ
α β : (↑I : Type)
f : E → F
a : E
hf :
  ContDiffPointwiseHolderAt
    ((ofLex : (a : Lex (ℕ × (↑I : Type))) → ℕ × (↑I : Type))
        ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type))) (l, β) : Lex (ℕ × (↑I : Type)))).1
    α f a
hle_1 :
  LE.le (α := Lex (ℕ × (↑I : Type)))
    ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type))) (l, β) : Lex (ℕ × (↑I : Type)))
    ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type)))
        (((ofLex : (a : Lex (ℕ × (↑I : Type))) → ℕ × (↑I : Type))
              ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type))) (l, β) : Lex (ℕ × (↑I : Type)))).1,
          α) :
      Lex (ℕ × (↑I : Type)))
hle :
  LE.le (α := (↑I : Type))
    ((ofLex : (a : Lex (ℕ × (↑I : Type))) → ℕ × (↑I : Type))
        ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type))) (l, β) : Lex (ℕ × (↑I : Type)))).2
    ((ofLex : (a : Lex (ℕ × (↑I : Type))) → ℕ × (↑I : Type))
        ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type)))
            (((ofLex : (a : Lex (ℕ × (↑I : Type))) → ℕ × (↑I : Type))
                  ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type))) (l, β) : Lex (ℕ × (↑I : Type)))).1,
              α) :
          Lex (ℕ × (↑I : Type)))).2
⊢ ContDiffPointwiseHolderAt l β f a

Tactic:
hf.of_exponent_le hle

Premises used: ContDiffPointwiseHolderAt.of_exponent_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
l : ℕ
α β : (↑I : Type)
f : E → F
a : E
hf :
  ContDiffPointwiseHolderAt
    ((ofLex : (a : Lex (ℕ × (↑I : Type))) → ℕ × (↑I : Type))
        ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type))) (l, β) : Lex (ℕ × (↑I : Type)))).1
    α f a
hle_1 :
  LE.le (α := Lex (ℕ × (↑I : Type)))
    ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type))) (l, β) : Lex (ℕ × (↑I : Type)))
    ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type)))
        (((ofLex : (a : Lex (ℕ × (↑I : Type))) → ℕ × (↑I : Type))
              ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type))) (l, β) : Lex (ℕ × (↑I : Type)))).1,
          α) :
      Lex (ℕ × (↑I : Type)))
hle :
  LE.le (α := (↑I : Type))
    ((ofLex : (a : Lex (ℕ × (↑I : Type))) → ℕ × (↑I : Type))
        ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type))) (l, β) : Lex (ℕ × (↑I : Type)))).2
    ((ofLex : (a : Lex (ℕ × (↑I : Type))) → ℕ × (↑I : Type))
        ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type)))
            (((ofLex : (a : Lex (ℕ × (↑I : Type))) → ℕ × (↑I : Type))
                  ((toLex : (a : ℕ × (↑I : Type)) → Lex (ℕ × (↑I : Type))) (l, β) : Lex (ℕ × (↑I : Type)))).1,
              α) :
          Lex (ℕ × (↑I : Type)))).2
⊢ ContDiffPointwiseHolderAt l β f a

Tactic:
exact hf.of_exponent_le hle

Premises used: ContDiffPointwiseHolderAt.of_exponent_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 l : ℕ
α : (↑I : Type)
f : E → F
a : E
hf : ContDiffPointwiseHolderAt k α f a
hl : l ≤ k
⊢ ContDiffPointwiseHolderAt l α f a

Tactic:
hf.of_toLex_le <| Prod.Lex.toLex_mono ⟨hl, le_rfl⟩

Premises used: le_rfl, ContDiffPointwiseHolderAt.of_toLex_le, And.intro, Prod.Lex.toLex_mono
-- 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
s : Set E
C : ℝ≥0
hf : ContDiffOn ℝ (↑k : WithTop ℕ∞) f s
hs : s ∈ 𝓝 a
hd :
  HolderOnWith (Y := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) C
    (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (↑α : ℝ) ⋯) (iteratedFDeriv ℝ k f) s
x : E
hx : x ∈ s
⊢ Membership.mem (γ := Set E)
    {x : E |
      (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)‖ ≤
            (↑C : ℝ) * ‖‖x - a‖ ^ (↑α : ℝ)‖)
        x}
    x

Tactic:
simpa [Real.abs_rpow_of_nonneg, ← dist_eq_norm, dist_nonneg]
      using hd.dist_le hx (mem_of_mem_nhds hs)

Premises used: dist_eq_norm, dist_nonneg, Real.abs_rpow_of_nonneg, mem_of_mem_nhds, HolderOnWith.dist_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)
a : E × F
⊢ ContDiffPointwiseHolderAt k α Prod.fst a

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

Premises used: WithTop.coe_lt_top, ContDiffAt.contDiffPointwiseHolderAt, contDiffAt_fst
-- 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
⊢ ContDiffPointwiseHolderAt k α Prod.snd a

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

Premises used: contDiffAt_snd, WithTop.coe_lt_top, ContDiffAt.contDiffPointwiseHolderAt
-- 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
⊢ 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 : E → G
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
h :
  ∀ (x : E) (hfx : ContDiffAt ℝ (↑k : WithTop ℕ∞) f x) (hgx : ContDiffAt ℝ (↑k : WithTop ℕ∞) g x),
    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) =
      (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).EventuallyEq (β := ContinuousMultilinearMap ℝ (fun (i : Fin k) ↦ E) (F × G))
    (fun (x : E) ↦
      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))
    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))

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

Premises used: ContDiffPointwiseHolderAt.contDiffAt, ContDiffAt.eventually
-- 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
h :
  ∀ (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)
⊢ 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) =
    (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))

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- 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
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
rw₁ : ContDiffAt ℝ (↑k : WithTop ℕ∞) g a
rw₂ : ContDiffAt ℝ (↑k : WithTop ℕ∞) f x
rw₃ : ContDiffAt ℝ (↑k : WithTop ℕ∞) g x
⊢ ∀ (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)

Tactic:
rw [iteratedFDeriv_prodMk _ _ le_rfl, iteratedFDeriv_prodMk _ _ le_rfl]

Premises used: le_rfl, iteratedFDeriv_prodMk
-- 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
⊢ ∀ (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)

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

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

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
x : E
hfx : ContDiffAt ℝ (↑k : WithTop ℕ∞) f x
hgx : ContDiffAt ℝ (↑k : WithTop ℕ∞) g x
⊢ ContDiffAt ℝ (↑k : WithTop ℕ∞) f x

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

Premises used: ContDiffPointwiseHolderAt.contDiffAt