awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
u : (i : ι) → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun (x : E) ↦ Φ x i) (p i) (u i)
h'p :
  ∀ (i : ι) (i_1 : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin i_1) ↦ E) (F' i))
      (fun (x : E) ↦ p i x i_1) (u i)
⊢ ContDiffWithinAt 𝕜 ω Φ s x
have refine : ∀ (m : ℕ),
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
    (fun (x : E) ↦ ContinuousMultilinearMap.pi (M₁ := fun (i : Fin m) ↦ E) (M' := F') fun (i : ι) ↦ p i x m)
    (⋂ (i : ι), u i)
Tactic: refine ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _, fun m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
u : (i : ι) → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun (x : E) ↦ Φ x i) (p i) (u i)
h'p :
  ∀ (i : ι) (i_1 : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin i_1) ↦ E) (F' i))
      (fun (x : E) ↦ p i x i_1) (u i)
m : ℕ
L : ((i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i)) ≃ₗᵢ[𝕜]
  ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i) :=
  ContinuousMultilinearMap.piₗᵢ 𝕜 fun (i : Fin m) ↦ E (E' := F')
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
    (fun (x : E) ↦ ContinuousMultilinearMap.pi (M₁ := fun (i : Fin m) ↦ E) (M' := F') fun (i : ι) ↦ p i x m)
    (⋂ (i : ι), u i)
have change : AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
  (fun (x : E) ↦
    (L :
        (a : (i : ι) → ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (F' i)) →
          ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
      fun (i : ι) ↦ p i x m)
  (⋂ (i : ι), u i)
Tactic: change AnalyticOn 𝕜 (fun x ↦ L (fun i ↦ p i x m)) (⋂ i, u i)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
u : (i : ι) → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun (x : E) ↦ Φ x i) (p i) (u i)
h'p :
  ∀ (i : ι) (i_1 : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin i_1) ↦ E) (F' i))
      (fun (x : E) ↦ p i x i_1) (u i)
m : ℕ
L : ((i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i)) ≃ₗᵢ[𝕜]
  ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i) :=
  ContinuousMultilinearMap.piₗᵢ 𝕜 fun (i : Fin m) ↦ E (E' := F')
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
    (fun (x : E) ↦
      (L :
          (a : (i : ι) → ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) (F' i)) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) ((i : ι) → F' i))
        fun (i : ι) ↦ p i x m)
    (⋂ (i : ι), u i)
have apply : AnalyticOn 𝕜 (F := (i : ι) → ContinuousMultilinearMap.{u_1, 0, uE, u_5} 𝕜 (fun (i : Fin m) ↦ E) (F' i))
  (fun (x : E) (i : ι) ↦ p i x m) (⋂ (i : ι), u i)
Tactic: apply (L.analyticOnNhd univ).comp_analyticOn ?_ (mapsTo_univ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n_1 : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
F' : ι → Type u_5
inst_4 : (i : ι) → NormedAddCommGroup (F' i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj (φ := F')
n : ℕ∞
h : ∀ (i : ι), ContDiffWithinAt.{u_1, uE, u_5} 𝕜 (F := F' i) (↑n : ℕ∞ω) (fun (x : E) ↦ Φ x i) s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
⊢ ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) Φ p u
have choose : ∀ (u : (i : ι) → Set E) (hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x)
  (p : (i : ι) → E → FormalMultilinearSeries.{u_1, uE, u_5} 𝕜 E (F' i))
  (hp : ∀ (i : ι), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) (fun (x : E) ↦ Φ x i) (p i) (u i)),
  ∃ u ∈ 𝓝[insert x s] x,
    ∃ (p : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) Φ p u
Tactic: choose u hux p hp using fun i => h i m hm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
inst_1 : Fintype ι
F' : ι → Type u_5
inst_2 : (i : ι) → NormedAddCommGroup (F' i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
inst_4 : DecidableEq ι
k : ℕ∞ω
x : (i : ι) → F' i
i : ι
⊢ ContDiff 𝕜 k (update (β := F') x i)
have rw : ∀ (i_1 : ι), ContDiff 𝕜 (F := F' i_1) k fun (x_1 : F' i) ↦ update (β := F') x i x_1 i_1
Tactic: rw [contDiff_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
inst_1 : Fintype ι
F' : ι → Type u_5
inst_2 : (i : ι) → NormedAddCommGroup (F' i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
inst_4 : DecidableEq ι
k : ℕ∞ω
x : (i : ι) → F' i
i j : ι
⊢ ContDiff 𝕜 (F := F' j) k fun (x_1 : F' i) ↦ update (β := F') x i x_1 j
have dsimp : ContDiff 𝕜 (F := F' j) k fun (x_1 : F' i) ↦
  if h : j = i then Eq.rec (motive := fun (x : ι) (x_2 : i = x) ↦ F' x) x_1 sorry else x j
Tactic: dsimp [Function.update]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
inst_1 : Fintype ι
F' : ι → Type u_5
inst_2 : (i : ι) → NormedAddCommGroup (F' i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
inst_4 : DecidableEq ι
k : ℕ∞ω
x : (i : ι) → F' i
i j : ι
⊢ ContDiff 𝕜 (F := F' j) k fun (x_1 : F' i) ↦
    if h : j = i then Eq.rec (motive := fun (x : ι) (x_2 : i = x) ↦ F' x) x_1 ⋯ else x j
have pos : ∀ (h : j = i), ContDiff 𝕜 (F := F' j) k fun (x : F' i) ↦ Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ F' x) x sorry
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
inst_1 : Fintype ι
F' : ι → Type u_5
inst_2 : (i : ι) → NormedAddCommGroup (F' i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
inst_4 : DecidableEq ι
k : ℕ∞ω
x : (i : ι) → F' i
i j : ι
pos : ∀ (h : j = i), ContDiff 𝕜 (F := F' j) k fun (x : F' i) ↦ Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ F' x) x ⋯
⊢ ContDiff 𝕜 (F := F' j) k fun (x_1 : F' i) ↦
    if h : j = i then Eq.rec (motive := fun (x : ι) (x_2 : i = x) ↦ F' x) x_1 ⋯ else x j
have neg : ∀ (h : ¬j = i), ContDiff 𝕜 (F := F' j) k fun (x_1 : F' i) ↦ x j
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_3
inst_1 : Fintype ι
F' : ι → Type u_5
inst_2 : (i : ι) → NormedAddCommGroup (F' i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (F' i)
inst_4 : DecidableEq ι
k : ℕ∞ω
x : (i : ι) → F' i
i j : ι
h : j = i
⊢ ContDiff 𝕜 (F := F' j) k fun (x : F' i) ↦ Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ F' x) x ⋯
have pos : ContDiff 𝕜 (F := F' j) k fun (x : F' j) ↦ Eq.rec (motive := fun (x : ι) (x_1 : j = x) ↦ F' x) x sorry
Tactic: subst h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
f g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f x + g x) x
have hf₁ : ContDiffWithinAt 𝕜 n f univ x
Tactic: rw [← contDiffWithinAt_univ] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
f g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
hf₁ : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f x + g x) x
have hg₁ : ContDiffWithinAt 𝕜 n g univ x
Tactic: rw [← contDiffWithinAt_univ] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
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
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s x) (iteratedFDerivWithin 𝕜 i g s x)
have this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
Tactic: have := (hf.eventually (by simp)).and (hg.eventually (by simp))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s x) (iteratedFDerivWithin 𝕜 i g s x)
have obtain : ∀ (t : Set E) (ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) (hxt : x ∈ t)
  (h :
    t ∩ insert x s ⊆
      {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}),
  iteratedFDerivWithin 𝕜 i (f + g) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s x) (iteratedFDerivWithin 𝕜 i g s x)
Tactic: obtain ⟨t, ht, hxt, h⟩ := mem_nhdsWithin.mp this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
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
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s x) (iteratedFDerivWithin 𝕜 i g s x)
have hft : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)
Tactic: have hft : ContDiffOn 𝕜 i f (s ∩ t) := fun a ha ↦ (h (by simp_all)).1.mono inter_subset_left
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
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
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
hft : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s x) (iteratedFDerivWithin 𝕜 i g s x)
have hgt : ContDiffOn 𝕜 (↑i : ℕ∞ω) g (s ∩ t)
Tactic: have hgt : ContDiffOn 𝕜 i g (s ∩ t) := fun a ha ↦ (h (by simp_all)).2.mono inter_subset_left
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
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
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
hft : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i : ℕ∞ω) g (s ∩ t)
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s x) (iteratedFDerivWithin 𝕜 i g s x)
have hut : UniqueDiffOn 𝕜 (s ∩ t)
Tactic: have hut : UniqueDiffOn 𝕜 (s ∩ t) := hu.inter ht
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
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
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
hft : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i : ℕ∞ω) g (s ∩ t)
hut : UniqueDiffOn 𝕜 (s ∩ t)
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s x) (iteratedFDerivWithin 𝕜 i g s x)
have H : s ∩ t =ᶠ[𝓝 x] s
Tactic: have H : ↑(s ∩ t) =ᶠ[𝓝 x] s :=
    inter_eventuallyEq_left.mpr (eventually_of_mem (ht.mem_nhds hxt) (fun _ h _ ↦ h))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
hft : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i : ℕ∞ω) g (s ∩ t)
hut : UniqueDiffOn 𝕜 (s ∩ t)
H : s ∩ t =ᶠ[𝓝 x] s
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s x) (iteratedFDerivWithin 𝕜 i g s x)
have rw : iteratedFDerivWithin 𝕜 i (f + g) (s ∩ t) x =
  HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i f (s ∩ t) x) (iteratedFDerivWithin 𝕜 i g (s ∩ t) x)
Tactic: rw [← iteratedFDerivWithin_congr_set H, ← iteratedFDerivWithin_congr_set H,
    ← iteratedFDerivWithin_congr_set H]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
i : ℕ
f g : E → F
hf : ContDiffAt 𝕜 (↑i : ℕ∞ω) f x
hg : ContDiffAt 𝕜 (↑i : ℕ∞ω) g x
⊢ iteratedFDeriv 𝕜 i (f + g) x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i f x)
      (iteratedFDeriv 𝕜 i g x)
have simp_rw : iteratedFDerivWithin 𝕜 i (f + g) univ x =
  HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i f univ x) (iteratedFDerivWithin 𝕜 i g univ x)
Tactic: simp_rw [← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
f : E → F
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ -f x) x
have hf₁ : ContDiffWithinAt 𝕜 n f univ x
Tactic: rw [← contDiffWithinAt_univ] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
hu : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 (-f) s x)
    (-iteratedFDerivWithin 𝕜 0 f s x)
have zero : ∀ (h : (i : Fin 0) → E),
  Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 0 (-f) s x : (a : (i : Fin 0) → E) → F) h : F)
    ((-iteratedFDerivWithin 𝕜 0 f s x : (a : (i : Fin 0) → E) → F) h : F)
Tactic: ext h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
      (-iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (i + 1) (-f) s x) (-iteratedFDerivWithin 𝕜 (i + 1) f s x)
have succ : ∀ (h : (i : Fin (i + 1)) → E),
  Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (i + 1) (-f) s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
    ((-iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
Tactic: ext h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
      (-iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
h : (i : Fin (i + 1)) → E
⊢ Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    ((((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
have rw : Eq.{uF + 1} (α := F)
  ((((fderivWithin 𝕜 (fun (x : E) ↦ -iteratedFDerivWithin 𝕜 i f s x) s x :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
            (h 0) :
          ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
  ((((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x : (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
            (h 0) :
          ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
Tactic: rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]