awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n : ℕ∞ω
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
simp :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f univ x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDeriv 𝕜 i ((⇑g : (a : F) → G) ∘ f) x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i f x)

Tactic:
simp only [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n : ℕ∞ω
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f univ x)

Tactic:
g.norm_iteratedFDerivWithin_comp_left hf.contDiffWithinAt uniqueDiffOn_univ (mem_univ x) hi

Premises used: uniqueDiffOn_univ, LinearIsometry.norm_iteratedFDerivWithin_comp_left, Set.mem_univ, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n : ℕ∞ω
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f univ x)

Tactic:
exact g.norm_iteratedFDerivWithin_comp_left hf.contDiffWithinAt uniqueDiffOn_univ (mem_univ x) hi

Premises used: uniqueDiffOn_univ, LinearIsometry.norm_iteratedFDerivWithin_comp_left, Set.mem_univ, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
g : F ≃ₗᵢ[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
    ((↑(↑g : F ≃L[𝕜] G) : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s x))

Tactic:
have :
    iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
      (g : F →L[𝕜] G).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x) :=
    g.toContinuousLinearEquiv.iteratedFDerivWithin_comp_left f hs hx i
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
g : F ≃ₗᵢ[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
    ((↑(↑g : F ≃L[𝕜] G) : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s x))
rw :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      ((↑(↑g : F ≃L[𝕜] G) : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E)
        (iteratedFDerivWithin 𝕜 i f s x)) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
g : F ≃ₗᵢ[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
    ((↑(↑g : F ≃L[𝕜] G) : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s x))
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      ((↑(↑g : F ≃L[𝕜] G) : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E)
        (iteratedFDerivWithin 𝕜 i f s x)) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i f s x)

Tactic:
apply LinearIsometry.norm_compContinuousMultilinearMap g.toLinearIsometry

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.norm_compContinuousMultilinearMap
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F ≃ₗᵢ[𝕜] G
f : E → F
x : E
i : ℕ
rw :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f univ x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDeriv 𝕜 i ((⇑g : (a : F) → G) ∘ f) x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i f x)

Tactic:
rw [← iteratedFDerivWithin_univ, ← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F ≃ₗᵢ[𝕜] G
f : E → F
x : E
i : ℕ
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
      (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f univ x)

Tactic:
apply g.norm_iteratedFDerivWithin_comp_left f uniqueDiffOn_univ (mem_univ x) i

Premises used: LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
x : E
n : ℕ∞ω
e : F ≃L[𝕜] G
H : ContDiffWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) n ((⇑e : (a : F) → G) ∘ f) s x
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
simpa only [Function.comp_def, e.symm.coe_coe, e.symm_apply_apply] using
      H.continuousLinearMap_comp (e.symm : G →L[𝕜] F)

Premises used: ContinuousLinearEquiv.symm, ContDiffWithinAt.continuousLinearMap_comp, Function.comp_def, ContinuousLinearEquiv.symm_apply_apply, ContinuousLinearEquiv.coe_coe, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
x : E
n : ℕ∞ω
e : F ≃L[𝕜] G
⊢ ContDiffAt.{u_1, u_2, u_4} 𝕜 (F := G) n ((⇑e : (a : F) → G) ∘ f) x ↔ ContDiffAt 𝕜 n f x

Tactic:
simp only [← contDiffWithinAt_univ, e.comp_contDiffWithinAt_iff]

Premises used: contDiffWithinAt_univ, ContinuousLinearEquiv.comp_contDiffWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
n : ℕ∞ω
e : F ≃L[𝕜] G
⊢ ContDiffOn.{u_1, u_2, u_4} 𝕜 (F := G) n ((⇑e : (a : F) → G) ∘ f) s ↔ ContDiffOn 𝕜 n f s

Tactic:
simp [ContDiffOn, e.comp_contDiffWithinAt_iff]

Premises used: ContDiffOn, ContinuousLinearEquiv.comp_contDiffWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
n : ℕ∞ω
e : F ≃L[𝕜] G
⊢ ContDiff.{u_1, u_2, u_4} 𝕜 (F := G) n ((⇑e : (a : F) → G) ∘ f) ↔ ContDiff 𝕜 n f

Tactic:
simp only [← contDiffOn_univ, e.comp_contDiffOn_iff]

Premises used: ContinuousLinearEquiv.comp_contDiffOn_iff, contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
⊢ ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)

Tactic:
have hA : ∀ m, IsBoundedLinearMap 𝕜 (A m) := fun m =>
    isBoundedLinearMap_continuousMultilinearMap_comp_linear g.contLinear
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
zero_eq :
  ∀ (x : G),
    Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x →
      ContinuousMultilinearMap.curry0.{u_1, u_4, u_3} (G := G)
          (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
            (p ((g : (a : G) → E) x) 0) fun (x : Fin 0) ↦ g.contLinear) =
        (f ∘ (⇑g : (a : G) → E)) x
fderivWithin :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) < n →
      ∀ (x : G),
        Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x →
          HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
            (fun (x : G) ↦
              (p ((g : (a : G) → E) x) m).compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦
                E) fun (x : Fin m) ↦ g.contLinear)
            (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ G)
              (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin m.succ) ↦ G) (M₁' :=
                fun (i : Fin m.succ) ↦ E) (p ((g : (a : G) → E) x) m.succ) fun (x : Fin m.succ) ↦ g.contLinear))
            ((⇑g : (a : G) → E) ⁻¹' s) x
cont :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
        (fun (x : G) ↦
          (p ((g : (a : G) → E) x) m).compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E)
            fun (x : Fin m) ↦ g.contLinear)
        ((⇑g : (a : G) → E) ⁻¹' s)
⊢ HasFTaylorSeriesUpToOn.{u_1, u_4, u_3} (𝕜 := 𝕜) n (f ∘ (⇑g : (a : G) → E))
    (fun (x : G) (k : ℕ) ↦
      (p ((g : (a : G) → E) x) k).compContinuousLinearMap (M₁ := fun (i : Fin k) ↦ G) (M₁' := fun (i : Fin k) ↦ E)
        fun (x : Fin k) ↦ g.contLinear)
    ((⇑g : (a : G) → E) ⁻¹' s)

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
x : G
hx : Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x
zero_eq :
  ContinuousMultilinearMap.curry0.{u_1, u_4, u_3} (G := G)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
        (p ((g : (a : G) → E) x) 0) fun (x : Fin 0) ↦ g.contLinear) =
    ContinuousMultilinearMap.curry0 (p ((g : (a : G) → E) x) 0)
⊢ ContinuousMultilinearMap.curry0.{u_1, u_4, u_3} (G := G)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
        (p ((g : (a : G) → E) x) 0) fun (x : Fin 0) ↦ g.contLinear) =
    (f ∘ (⇑g : (a : G) → E)) x

Tactic:
simp only [(hf.zero_eq (g x) hx).symm, Function.comp_apply]

Premises used: HasFTaylorSeriesUpToOn.zero_eq, Function.comp_apply, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
x : G
hx : Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x
zero_eq :
  Eq.{u_3 + 1} (α := F)
    ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ (g.contLinear : (a : G) → E) 0 : F)
    ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) 0 : F)
⊢ ContinuousMultilinearMap.curry0.{u_1, u_4, u_3} (G := G)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
        (p ((g : (a : G) → E) x) 0) fun (x : Fin 0) ↦ g.contLinear) =
    ContinuousMultilinearMap.curry0 (p ((g : (a : G) → E) x) 0)

Tactic:
change (p (g x) 0 fun _ : Fin 0 => g.contLinear 0) = p (g x) 0 0

Premises used: ContinuousAffineMap.contLinear, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
x : G
hx : Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x
zero_eq :
  Eq.{u_3 + 1} (α := F) ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)
    ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) 0 : F)
⊢ Eq.{u_3 + 1} (α := F)
    ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ (g.contLinear : (a : G) → E) 0 : F)
    ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) 0 : F)

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
x : G
hx : Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x
⊢ Eq.{u_3 + 1} (α := F) ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ 0 : F)
    ((p ((g : (a : G) → E) x) 0 : (a : (i : Fin 0) → E) → F) 0 : F)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : G
hx : Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x
⊢ HasFDerivWithinAt (A m ∘ (fun (x : E) ↦ p x m) ∘ (⇑g : (a : G) → E))
    (IsBoundedLinearMap.toContinuousLinearMap (A m) ⋯ ∘SL
      ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p ((g : (a : G) → E) x) m.succ) ∘SL
        g.contLinear)
    (fun (x : G) ↦ s ((g : (a : G) → E) x)) x

Tactic:
(hA m).hasFDerivAt.comp_hasFDerivWithinAt x
        ((hf.fderivWithin m hm (g x) hx).comp x g.hasFDerivWithinAt (Subset.refl _))

Premises used: Set.Subset.refl, HasFDerivAt.comp_hasFDerivWithinAt, HasFTaylorSeriesUpToOn.fderivWithin, HasFDerivWithinAt.comp, ContinuousAffineMap.hasFDerivWithinAt, IsBoundedLinearMap.hasFDerivAt, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : G
hx : Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F))
    (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin m) ↦ G)) NormedAddCommGroup.toAddCommGroup
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F))
    (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin m) ↦ G)) (β :=
    Module 𝕜 (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)) NormedSpace.toModule
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F))
    (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin m) ↦ G)) UniformSpace.toTopologicalSpace
y : G
v : (i : Fin m) → G
h h₁ :
  Eq.{u_3 + 1} (α := F)
    ((p ((g : (a : G) → E) x) m.succ : (a : (i : Fin m.succ) → E) → F)
        (cons (α := fun (i : Fin (m + 1)) ↦ E) ((g.contLinear : (a : G) → E) y) ((⇑g.contLinear : (a : G) → E) ∘ v)) :
      F)
    ((p ((g : (a : G) → E) x) m.succ : (a : (i : Fin m.succ) → E) → F)
        (cons (α := fun (i : Fin m.succ) ↦ E) ((g.contLinear : (a : G) → E) y) ((⇑g.contLinear : (a : G) → E) ∘ v)) :
      F)
⊢ Eq.{u_3 + 1} (α := F)
    ((p ((g : (a : G) → E) x) m.succ : (a : (i : Fin m.succ) → E) → F)
        (comp.{1, u_4 + 1, u_2 + 1} (β := G) (⇑g.contLinear : (a : G) → E) (cons (α := fun (a : Fin m.succ) ↦ G) y v)) :
      F)
    ((p ((g : (a : G) → E) x) m.succ : (a : (i : Fin m.succ) → E) → F)
        (cons (α := fun (i : Fin m.succ) ↦ E) ((g.contLinear : (a : G) → E) y) ((⇑g.contLinear : (a : G) → E) ∘ v)) :
      F)

Tactic:
rw [comp_cons]

Premises used: Fin.comp_cons