awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 f x) = ‖f x‖
have rw : norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
        f)
      x) =
  ‖f x‖
Tactic: rw [iteratedFDeriv_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
rw :
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
          f)
        x) =
    ‖f x‖
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 f x) = ‖f x‖
have rw₁ : norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
          (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
        (f x) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) =
  ‖f x‖
Tactic: rw [iteratedFDeriv_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
rw :
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
          f)
        x) =
    ‖f x‖
rw₁ :
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
          (f x) :
        ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) =
    ‖f x‖
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 f x) = ‖f x‖
have rw₂ : ‖f x‖ = ‖f x‖
Tactic: rw [iteratedFDeriv_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ
IH :
  tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
⊢ tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) f) ⊆
    tsupport f
have succ : tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f))) ⊆
  tsupport f
Tactic: rw [iteratedFDeriv_succ_eq_comp_left]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ
⊢ tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
have zero : tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 f) ⊆ tsupport f
Tactic: induction n with
  | zero =>
    rw [iteratedFDeriv_zero_eq_comp]
    exact closure_minimal ((support_comp_subset (map_zero _) _).trans subset_closure)
      isClosed_closure
  | succ n IH =>
    rw [iteratedFDeriv_succ_eq_comp_left]
    exact closure_minimal ((support_comp_subset (map_zero _) _).trans
      ((support_fderiv_subset 𝕜).trans IH)) isClosed_closure
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ
zero :
  tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 f) ⊆ tsupport f
⊢ tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
have succ : ∀ (n : ℕ)
  (IH :
    tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f) ⊆
      tsupport f),
  tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) f) ⊆
    tsupport f
Tactic: induction n with
  | zero =>
    rw [iteratedFDeriv_zero_eq_comp]
    exact closure_minimal ((support_comp_subset (map_zero _) _).trans subset_closure)
      isClosed_closure
  | succ n IH =>
    rw [iteratedFDeriv_succ_eq_comp_left]
    exact closure_minimal ((support_comp_subset (map_zero _) _).trans
      ((support_fderiv_subset 𝕜).trans IH)) isClosed_closure
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
⊢ norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) f x)
have rw : norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) =
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) x)
Tactic: rw [iteratedFDeriv_succ_eq_comp_left, comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
rw :
  norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
        (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
              (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
                ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
        (fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) x)
⊢ norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) f x)
have rw₁ : norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) =
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
        (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
Tactic: rw [iteratedFDeriv_succ_eq_comp_left, comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
rw :
  norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
        (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
              (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
                ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
        (fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) x)
rw₁ :
  norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
              (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
                ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
              ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
          (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) :
        ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
⊢ norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) f x)
have rw₂ : norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) =
  norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x)
Tactic: rw [iteratedFDeriv_succ_eq_comp_left, comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
⊢ (𝓝 x).EventuallyEq (β := FormalMultilinearSeries 𝕜 E F) (ftaylorSeries 𝕜 f₁) (ftaylorSeries 𝕜 f)
have h₁ : ∀ (e₁ : E) (he₁ : f₁ =ᶠ[𝓝 e₁] f), Eq (α := FormalMultilinearSeries 𝕜 E F) (ftaylorSeries 𝕜 f₁ e₁) (ftaylorSeries 𝕜 f e₁)
Tactic: filter_upwards [eventually_eventuallyEq_nhds.2 h] with e₁ he₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
e₁ : E
he₁ : f₁ =ᶠ[𝓝 e₁] f
⊢ Eq (α := FormalMultilinearSeries 𝕜 E F) (ftaylorSeries 𝕜 f₁ e₁) (ftaylorSeries 𝕜 f e₁)
have h₁ : ∀ (n : ℕ),
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (ftaylorSeries 𝕜 f₁ e₁ n)
    (ftaylorSeries 𝕜 f e₁ n)
Tactic: ext n : 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
m : ℕ
hmn : (↑m : ℕ∞ω) ≤ n
x : E
⊢ p x m = iteratedFDeriv 𝕜 m f x
have rw : p x m = iteratedFDerivWithin 𝕜 m f univ x
Tactic: rw [← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
m : ℕ
hmn : (↑m : ℕ∞ω) ≤ n
x : E
⊢ p x m = iteratedFDerivWithin 𝕜 m f univ x
have rw : ∀ (h : HasFTaylorSeriesUpToOn n f p univ) {m : ℕ} (hmn : (↑m : ℕ∞ω) ≤ n) (x : E),
  p x m = iteratedFDerivWithin 𝕜 m f univ x
Tactic: rw [← hasFTaylorSeriesUpToOn_univ_iff] at h
Cleared hypotheses: h, m, hmn, x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : E
hx : x ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDeriv 𝕜 n f x)
have rw : Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
  (iteratedFDerivWithin 𝕜 n f univ x)
Tactic: rw [← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
⊢ Eq (α := (x : E) → FormalMultilinearSeries 𝕜 E F) (ftaylorSeriesWithin 𝕜 f univ) (ftaylorSeries 𝕜 f)
have h : ∀ (x : E), Eq (α := FormalMultilinearSeries 𝕜 E F) (ftaylorSeriesWithin 𝕜 f univ x) (ftaylorSeries 𝕜 f x)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
⊢ Eq (α := FormalMultilinearSeries 𝕜 E F) (ftaylorSeriesWithin 𝕜 f univ x) (ftaylorSeries 𝕜 f x)
have h : ∀ (n : ℕ),
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (ftaylorSeriesWithin 𝕜 f univ x n)
    (ftaylorSeries 𝕜 f x n)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f univ x)
    (iteratedFDeriv 𝕜 n f x)
have h : Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f x)
  (iteratedFDeriv 𝕜 n f x)
Tactic: rw [iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) m : F)
    ((((iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin n) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1)) ↦ E) m) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last n)) :
      F)
have rw : Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f univ x : (a : (i : Fin (n + 1)) → E) → F) m : F)
  ((((iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f univ y) univ x : (a : (i : Fin n) → E) → E →L[𝕜] F)
            (init (α := fun (i : Fin (n + 1)) ↦ E) m) :
          E →L[𝕜] F) :
        (a : E) → F)
      (m (last n)) :
    F)
Tactic: rw [← iteratedFDerivWithin_univ, ← iteratedFDerivWithin_univ, ← fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) f x)
    (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)) :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
          ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
      (iteratedFDeriv 𝕜 n fun (y : E) ↦ fderiv 𝕜 f y : E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      x)
have H : ∀ (m : (i : Fin (n + 1)) → E),
  Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) m : F)
    ((comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)) :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                  ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
              (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
            (iteratedFDeriv 𝕜 n fun (y : E) ↦ fderiv 𝕜 f y :
              E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            x :
          (a : (i : Fin (n + 1)) → E) → F)
        m :
      F)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : (i : Fin (n + 1)) → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) m : F)
    ((comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)) :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                  ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
              (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
            (iteratedFDeriv 𝕜 n fun (y : E) ↦ fderiv 𝕜 f y :
              E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            x :
          (a : (i : Fin (n + 1)) → E) → F)
        m :
      F)
have H : Eq.{uF + 1} (α := F)
  ((((iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin n) → E) → E →L[𝕜] F)
            (init (α := fun (i : Fin (n + 1)) ↦ E) m) :
          E →L[𝕜] F) :
        (a : E) → F)
      (m (last n)) :
    F)
  ((comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
          ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)) :
              (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
            (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
          (iteratedFDeriv 𝕜 n fun (y : E) ↦ fderiv 𝕜 f y :
            E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
          x :
        (a : (i : Fin (n + 1)) → E) → F)
      m :
    F)
Tactic: rw [iteratedFDeriv_succ_apply_right, comp_apply, continuousMultilinearCurryRightEquiv_symm_apply']