awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 := (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:
AnalyticOn.pi (fun i ↦ (h'p i m).mono (iInter_subset _ _))

Premises used: AnalyticOn.pi, Set.iInter_subset, AnalyticOn.mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 := (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:
exact AnalyticOn.pi (fun i ↦ (h'p i m).mono (iInter_subset _ _))

Premises used: AnalyticOn.pi, Set.iInter_subset, AnalyticOn.mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
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
⊢ ∃ 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
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : (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:
⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _⟩

Premises used: Iff.mpr, Set.iInter, HasFTaylorSeriesUpToOn.mono, Filter.iInter_mem, And.intro, Exists.intro, Set.iInter_subset, hasFTaylorSeriesUpToOn_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : (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:
exact ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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')
h : ∀ (i : ι), ContDiffWithinAt.{u_1, uE, u_5} 𝕜 (F := F' i) n (fun (x : E) ↦ Φ x i) s x
⊢ ContDiffWithinAt 𝕜 n Φ s x

Tactic:
match n with
  | ω =>
    choose u hux p hp h'p using h
    refine ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _, fun m ↦ ?_⟩
    set L : (∀ i, E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] ∀ i, F' i :=
      ContinuousMultilinearMap.piₗᵢ _ _
    change AnalyticOn 𝕜 (fun x ↦ L (fun i ↦ p i x m)) (⋂ i, u i)
    apply (L.analyticOnNhd univ).comp_analyticOn ?_ (mapsTo_univ _ _)
    exact AnalyticOn.pi (fun i ↦ (h'p i m).mono (iInter_subset _ _))
  | (n : ℕ∞) =>
    intro m hm
    choose u hux p hp using fun i => h i m hm
    exact ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set 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
⊢ ContDiffOn 𝕜 n Φ s ↔ ∀ (i : ι), ContDiffOn.{u_1, uE, u_5} 𝕜 (F := F' i) n (fun (x : E) ↦ Φ x i) s

Tactic:
⟨fun h _ x hx => contDiffWithinAt_pi.1 (h x hx) _, fun h x hx =>
    contDiffWithinAt_pi.2 fun i => h i x hx⟩

Premises used: Iff.mpr, Iff.intro, contDiffWithinAt_pi, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 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
⊢ ContDiffAt 𝕜 n Φ x ↔ ∀ (i : ι), ContDiffAt.{u_1, uE, u_5} 𝕜 (F := F' i) n (fun (x : E) ↦ Φ x i) x

Tactic:
contDiffWithinAt_pi

Premises used: ContDiffAt, contDiffWithinAt_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 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
⊢ ContDiff 𝕜 n Φ ↔ ∀ (i : ι), ContDiff.{u_1, uE, u_5} 𝕜 (F := F' i) n fun (x : E) ↦ Φ x i

Tactic:
simp only [← contDiffOn_univ, contDiffOn_pi]

Premises used: contDiffOn_pi, contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 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
hΦ : ∀ (i : ι), ContDiff.{u_1, uE, u_5} 𝕜 (F := F' i) n fun (x : E) ↦ Φ x i
⊢ ContDiff 𝕜 n Φ

Tactic:
contDiff_pi.2 hΦ

Premises used: Iff.mpr, contDiff_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set 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
hΦ : ∀ (i : ι), ContDiffOn.{u_1, uE, u_5} 𝕜 (F := F' i) n (fun (x : E) ↦ Φ x i) s
⊢ ContDiffOn 𝕜 n Φ s

Tactic:
contDiffOn_pi.2 hΦ

Premises used: Iff.mpr, contDiffOn_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 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
hΦ : ∀ (i : ι), ContDiffAt.{u_1, uE, u_5} 𝕜 (F := F' i) n (fun (x : E) ↦ Φ x i) x
⊢ ContDiffAt 𝕜 n Φ x

Tactic:
contDiffAt_pi.2 hΦ

Premises used: Iff.mpr, contDiffAt_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ι
rw : ∀ (i_1 : ι), ContDiff 𝕜 (F := F' i_1) k fun (x_1 : F' i) ↦ update (β := F') x i x_1 i_1
⊢ ContDiff 𝕜 k (update (β := F') x i)

Tactic:
rw [contDiff_pi]

Premises used: contDiff_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ι
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 ⋯ else x j
⊢ ContDiff 𝕜 (F := F' j) k fun (x_1 : F' i) ↦ update (β := F') x i x_1 j

Tactic:
dsimp [Function.update]

Premises used: Function.update
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 ⋯
neg : ∀ (h : ¬j = i), ContDiff 𝕜 (F := F' j) k fun (x_1 : F' i) ↦ x 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

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
pos : ContDiff 𝕜 (F := F' j) k fun (x : F' j) ↦ Eq.rec (motive := fun (x : ι) (x_1 : j = x) ↦ F' x) x ⋯
⊢ ContDiff 𝕜 (F := F' j) k fun (x : F' i) ↦ Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ F' x) x ⋯

Tactic:
subst h
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
j : ι
⊢ ContDiff 𝕜 (F := F' j) k fun (x : F' j) ↦ Eq.rec (motive := fun (x : ι) (x_1 : j = x) ↦ F' x) x ⋯

Tactic:
contDiff_id

Premises used: contDiff_id
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
j : ι
⊢ ContDiff 𝕜 (F := F' j) k fun (x : F' j) ↦ Eq.rec (motive := fun (x : ι) (x_1 : j = x) ↦ F' x) x ⋯

Tactic:
exact contDiff_id

Premises used: contDiff_id
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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_1 : F' i) ↦ x j

Tactic:
contDiff_const

Premises used: contDiff_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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_1 : F' i) ↦ x j

Tactic:
exact contDiff_const

Premises used: contDiff_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ℕ∞ω
i : ι
⊢ ContDiff 𝕜 (E := F' i) k (Pi.single (M := F') i)

Tactic:
contDiff_update k 0 i

Premises used: contDiff_update, Pi.single, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
i : ι
⊢ ContDiff 𝕜 (F := E) n fun (f : ι → E) ↦ f i

Tactic:
contDiff_pi.mp contDiff_id i

Premises used: contDiff_id, Iff.mp, contDiff_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
i : ι
f : ι → E
⊢ ContDiffAt 𝕜 (F := E) n (fun (f : ι → E) ↦ f i) f

Tactic:
(contDiff_apply 𝕜 E i).contDiffAt

Premises used: contDiff_apply, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
ι : Type u_3
inst_3 : Fintype ι
i : ι
s : Set (ι → E)
⊢ ContDiffOn 𝕜 (F := E) n (fun (f : ι → E) ↦ f i) s

Tactic:
(contDiff_apply 𝕜 E i).contDiffOn

Premises used: ContDiff.contDiffOn, contDiff_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
ι : Type u_3
ι' : Type u_4
inst_3 : Fintype ι
inst_4 : Fintype ι'
i : ι
j : ι'
⊢ ContDiff 𝕜 (F := E) n fun (f : ι → ι' → E) ↦ f i j

Tactic:
contDiff_pi.mp (contDiff_apply 𝕜 (ι' → E) i) j

Premises used: contDiff_apply, Iff.mp, contDiff_pi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
q : E → FormalMultilinearSeries 𝕜 E F
g : E → F
hf : HasFTaylorSeriesUpToOn n f p s
hg : HasFTaylorSeriesUpToOn n g q s
⊢ HasFTaylorSeriesUpToOn n (f + g) (p + q) s

Tactic:
HasFTaylorSeriesUpToOn.continuousLinearMap_comp
    (ContinuousLinearMap.fst 𝕜 F F + .snd 𝕜 F F) (hf.prodMk hg)

Premises used: ContinuousLinearMap.compContinuousMultilinearMap, HasFTaylorSeriesUpToOn.continuousLinearMap_comp, HasFTaylorSeriesUpToOn.prodMk, HAdd.hAdd, ContinuousLinearMap.fst, LinearMap.compMultilinearMap
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
q : E → FormalMultilinearSeries 𝕜 E F
g : E → F
hf : HasFTaylorSeriesUpToOn n f p s
hg : HasFTaylorSeriesUpToOn n g q s
⊢ HasFTaylorSeriesUpToOn n (f + g) (p + q) s

Tactic:
exact HasFTaylorSeriesUpToOn.continuousLinearMap_comp
    (ContinuousLinearMap.fst 𝕜 F F + .snd 𝕜 F F) (hf.prodMk hg)

Premises used: HasFTaylorSeriesUpToOn.continuousLinearMap_comp, HasFTaylorSeriesUpToOn.prodMk, HAdd.hAdd, ContinuousLinearMap.fst
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
⊢ ContDiff 𝕜 (F := F) n fun (p : F × F) ↦ p.1 + p.2

Tactic:
(IsBoundedLinearMap.fst.add IsBoundedLinearMap.snd).contDiff

Premises used: IsBoundedLinearMap.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ℕ∞ω
s : Set E
f g : E → F
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f x + g x) s x

Tactic:
contDiff_add.contDiffWithinAt.comp x (hf.prodMk hg) subset_preimage_univ

Premises used: ContDiffWithinAt.comp, Set.subset_preimage_univ, contDiff_add, ContDiff.contDiffWithinAt, ContDiffWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
⊢ ContDiffWithinAt 𝕜 n f univ x

Tactic:
rw [← contDiffWithinAt_univ] at *

Premises used: contDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
⊢ ContDiffWithinAt 𝕜 n g univ x

Tactic:
rw [← contDiffWithinAt_univ] at *

Premises used: contDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f x + g x) univ x

Tactic:
hf.add hg

Premises used: ContDiffWithinAt.add
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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 : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f x + g x) univ x

Tactic:
exact hf.add hg

Premises used: ContDiffWithinAt.add
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
f g : E → F
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
⊢ ContDiff.{u_1, uE, uF} 𝕜 (F := F) n fun (x : E) ↦ f x + g x

Tactic:
contDiff_add.comp (hf.prodMk hg)

Premises used: ContDiff.prodMk, contDiff_add, ContDiff.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
s : Set E
f g : E → F
hf : ContDiffOn 𝕜 n f s
hg : ContDiffOn 𝕜 n g s
⊢ ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f x + g x) s

Tactic:
fun x hx =>
  (hf x hx).add (hg x hx)

Premises used: ContDiffWithinAt.add, ContDiffOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
⊢ Ne (α := ℕ∞ω) (↑i : ℕ∞ω) ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
⊢ ∀ᶠ (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))
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
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)
⊢ 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

Premises used: mem_nhdsWithin, Iff.mp