awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
h : ContDiffAt 𝕜' (↑n : WithTop ℕ∞) f x
h' : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f Set.univ x
⊢ (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDeriv 𝕜' n f))
    (iteratedFDeriv 𝕜 n f)
have h₁ : 𝓝 x = 𝓝[Set.univ] x
Tactic: convert! (h'.restrictScalars_iteratedFDerivWithin_eventuallyEq _ trivial)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
h : ContDiffAt 𝕜' (↑n : WithTop ℕ∞) f x
h' : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f Set.univ x
h₁ : 𝓝 x = 𝓝[Set.univ] x
⊢ (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDeriv 𝕜' n f))
    (iteratedFDeriv 𝕜 n f)
have h₂ : Eq (α := E → ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜' n f)
  (iteratedFDerivWithin 𝕜' n f Set.univ)
Tactic: convert! (h'.restrictScalars_iteratedFDerivWithin_eventuallyEq _ trivial)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
h : ContDiffAt 𝕜' (↑n : WithTop ℕ∞) f x
h' : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f Set.univ x
h₁ : 𝓝 x = 𝓝[Set.univ] x
h₂ :
  Eq (α := E → ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜' n f)
    (iteratedFDerivWithin 𝕜' n f Set.univ)
⊢ (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDeriv 𝕜' n f))
    (iteratedFDeriv 𝕜 n f)
have h₃ : Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f)
  (iteratedFDerivWithin 𝕜 n f Set.univ)
Tactic: convert! (h'.restrictScalars_iteratedFDerivWithin_eventuallyEq _ trivial)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n : ℕ
h : ContDiffAt 𝕜' (↑n : WithTop ℕ∞) f x
h' : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f Set.univ x
h₁ : 𝓝 x = 𝓝[Set.univ] x
h₂ :
  Eq (α := E → ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜' n f)
    (iteratedFDerivWithin 𝕜' n f Set.univ)
h₃ :
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f)
    (iteratedFDerivWithin 𝕜 n f Set.univ)
⊢ (𝓝 x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDeriv 𝕜' n f))
    (iteratedFDeriv 𝕜 n f)
have convert_8 : UniqueDiffOn.{u_1, u_3} 𝕜 (E := E) Set.univ
Tactic: convert! (h'.restrictScalars_iteratedFDerivWithin_eventuallyEq _ trivial)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
y : H
⊢ ContDiffWithinAt 𝕜 n f t y ↔
    ∀ (i : ι), ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) t y
have rw : (∀ (i : ι),
    ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) n
      (fun (x : H) ↦ ((⇑(PiLp.continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) t y) ↔
  ∀ (i : ι), ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) t y
Tactic: rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffWithinAt_iff, contDiffWithinAt_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
y : H
⊢ ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) y
have rw : (∀ (i : ι),
    ContDiffAt.{u_1, u_4, u_3} 𝕜 (F := E i) n
      (fun (x : H) ↦ ((⇑(PiLp.continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) y) ↔
  ∀ (i : ι), ContDiffAt.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) y
Tactic: rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffAt_iff, contDiffAt_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
⊢ ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) t
have rw : (∀ (i : ι),
    ContDiffOn.{u_1, u_4, u_3} 𝕜 (F := E i) n
      (fun (x : H) ↦ ((⇑(PiLp.continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) t) ↔
  ∀ (i : ι), ContDiffOn.{u_1, u_4, u_3} 𝕜 (F := E i) n (fun (x : H) ↦ (f x).ofLp i) t
Tactic: rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffOn_iff, contDiffOn_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Fintype ι
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
⊢ ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff.{u_1, u_4, u_3} 𝕜 (F := E i) n fun (x : H) ↦ (f x).ofLp i
have rw : (∀ (i : ι),
    ContDiff.{u_1, u_4, u_3} 𝕜 (F := E i) n fun (x : H) ↦
      ((⇑(PiLp.continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) ↔
  ∀ (i : ι), ContDiff.{u_1, u_4, u_3} 𝕜 (F := E i) n fun (x : H) ↦ (f x).ofLp i
Tactic: rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiff_iff, contDiff_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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 : ℕ
f : E → F
a : E
⊢ ContDiffPointwiseHolderAt k 0 f a ↔ ContDiffAt ℝ (↑k : WithTop ℕ∞) f a
have refine : ∀ (h : ContDiffAt ℝ (↑k : WithTop ℕ∞) f a),
  IsBigO (E := ContinuousMultilinearMap.{0, 0, u_1, u_2} ℝ (fun (i : Fin k) ↦ E) F) (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))
    fun (x : E) ↦ HPow.hPow (β := ℝ) ‖x - a‖ (↑0 : ℝ)
Tactic: refine ⟨contDiffAt, fun h ↦ ⟨h, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
⊢ 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‖ ^ (↑α : ℝ)
have 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‖ ^ (↑α : ℝ))
Tactic: simp only [contDiffPointwiseHolderAt_iff, Nat.cast_zero, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
⊢ (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‖ ^ (↑α : ℝ)
have 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‖ ^ (↑α : ℝ)
Tactic: simp only [iteratedFDeriv_zero_eq_comp, Function.comp_def, ← map_sub]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
⊢ (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‖ ^ (↑α : ℝ)
have 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‖ ^ (↑α : ℝ)
Tactic: rw [← isBigO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
⊢ (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‖ ^ (↑α : ℝ)
have 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‖ ^ (↑α : ℝ)
Tactic: simp_rw [LinearIsometryEquiv.norm_map, isBigO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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‖ ^ (↑β : ℝ)
have refine_1 : ∀ (hα : (↑α : ℝ) = 0), (↑β : ℝ) = 0
Tactic: refine .comp_tendsto (.rpow_rpow_nhdsGE_zero_of_le_of_imp hle fun hα ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise (goal)
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
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 a) (fun (x : E) ↦ ‖x - a‖ ^ (↑α : ℝ)) fun (x : E) ↦ ‖x - a‖ ^ (↑β : ℝ)
have refine_2 : Tendsto (β := ℝ) (fun (x : E) ↦ ‖x - a‖) (𝓝 a) (𝓝[≥] 0)
Tactic: refine .comp_tendsto (.rpow_rpow_nhdsGE_zero_of_le_of_imp hle fun hα ↦ ?_) ?_
-- 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
⊢ (𝓝 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))
have 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))
Tactic: filter_upwards [hf.contDiffAt.eventually (by simp),
        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 : 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
⊢ 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))
have 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)
Tactic: apply DFunLike.ext
-- 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
⊢ ∀ (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 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)
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
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)
⊢ ∀ (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 ℕ∞) f a
Tactic: rw [iteratedFDeriv_prodMk _ _ le_rfl, iteratedFDeriv_prodMk _ _ le_rfl]