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
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : F →L[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hxU : x ∈ U
hfU : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ U)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) (s ∩ U) x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f (s ∩ U) x))

Tactic:
exact .symm <| (hfU.ftaylorSeriesWithin (hs.inter hU)).continuousLinearMap_comp g
    |>.eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter hU) ⟨hx, hxU⟩

Premises used: le_rfl, HasFTaylorSeriesUpToOn.continuousLinearMap_comp, And.intro, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn, UniqueDiffOn.inter, ContDiffOn.ftaylorSeriesWithin
-- 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 →L[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
simp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f univ x))
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDeriv 𝕜 i ((⇑g : (a : F) → G) ∘ f) x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (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 →L[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f univ x))

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

Premises used: ContinuousLinearMap.iteratedFDerivWithin_comp_left, uniqueDiffOn_univ, 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 →L[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f univ x))

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

Premises used: ContinuousLinearMap.iteratedFDerivWithin_comp_left, uniqueDiffOn_univ, 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
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
zero :
  ∀ (m : (i : Fin 0) → E),
    Eq.{u_4 + 1} (α := G) ((iteratedFDerivWithin 𝕜 0 ((⇑g : (a : F) → G) ∘ f) s x : (a : (i : Fin 0) → E) → G) m : G)
      (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin 0) ↦ E) (iteratedFDerivWithin 𝕜 0 f s x) :
            (a : (i : Fin 0) → E) → G)
          m :
        G)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin 0) ↦ E) G)
    (iteratedFDerivWithin 𝕜 0 ((⇑g : (a : F) → G) ∘ f) s x)
    ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin 0) ↦ E) (iteratedFDerivWithin 𝕜 0 f s x))

Tactic:
ext1 m
-- 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
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
m : (i : Fin 0) → E
⊢ Eq.{u_4 + 1} (α := G) ((iteratedFDerivWithin 𝕜 0 ((⇑g : (a : F) → G) ∘ f) s x : (a : (i : Fin 0) → E) → G) m : G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin 0) ↦ E) (iteratedFDerivWithin 𝕜 0 f s x) :
          (a : (i : Fin 0) → E) → G)
        m :
      G)

Tactic:
simp only [iteratedFDerivWithin_zero_apply, comp_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, coe_coe]

Premises used: ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply, ContinuousLinearEquiv.coe_coe, iteratedFDerivWithin_zero_apply
-- 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
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E} (hx : x ∈ s),
    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).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
x : E
hx : x ∈ s
succ :
  ∀ (m : (i : Fin (i + 1)) → E),
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 (i + 1) ((⇑g : (a : F) → G) ∘ f) s x : (a : (i : Fin (i + 1)) → E) → G) m : G)
      (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
              (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
            (a : (i : Fin (i + 1)) → E) → G)
          m :
        G)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin (i + 1)) ↦ E) G)
    (iteratedFDerivWithin 𝕜 (i + 1) ((⇑g : (a : F) → G) ∘ f) s x)
    ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
      (iteratedFDerivWithin 𝕜 (i + 1) f s x))

Tactic:
ext1 m
-- 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
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E} (hx : x ∈ s),
    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).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
x : E
hx : x ∈ s
m : (i : Fin (i + 1)) → E
succ :
  Eq.{u_4 + 1} (α := G)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)
⊢ Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 (i + 1) ((⇑g : (a : F) → G) ∘ f) s x : (a : (i : Fin (i + 1)) → E) → G) m : G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)

Tactic:
rw [iteratedFDerivWithin_succ_apply_left]

Premises used: iteratedFDerivWithin_succ_apply_left
-- 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
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E} (hx : x ∈ s),
    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).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
x : E
hx : x ∈ s
m : (i : Fin (i + 1)) → E
⊢ Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x)
    (fderivWithin 𝕜
      (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
        (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
        (iteratedFDerivWithin 𝕜 i f s))
      s x)

Tactic:
have Z : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (g ∘ f) s) s x =
        fderivWithin 𝕜 (g.continuousMultilinearMapCongrRight (fun _ : Fin i => E) ∘
          iteratedFDerivWithin 𝕜 i f s) s x :=
      fderivWithin_congr' (@IH) hx
-- 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
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E} (hx : x ∈ s),
    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).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
x : E
hx : x ∈ s
m : (i : Fin (i + 1)) → E
Z :
  Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x)
    (fderivWithin 𝕜
      (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
        (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
        (iteratedFDerivWithin 𝕜 i f s))
      s x)
succ :
  Eq.{u_4 + 1} (α := G)
    ((((fderivWithin 𝕜
                  (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
                    (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
                      (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) →
                        ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
                    (iteratedFDerivWithin 𝕜 i f s))
                  s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)
⊢ Eq.{u_4 + 1} (α := G)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)

Tactic:
simp_rw [Z]
-- 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
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E} (hx : x ∈ s),
    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).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
x : E
hx : x ∈ s
m : (i : Fin (i + 1)) → E
Z :
  Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x)
    (fderivWithin 𝕜
      (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
        (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
        (iteratedFDerivWithin 𝕜 i f s))
      s x)
succ :
  Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      F)
    ((iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) m : F)
⊢ Eq.{u_4 + 1} (α := G)
    (((((↑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
                    ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F →L[𝕜]
                      ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G) ∘SL
                  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
            (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
          (a : (i : Fin (i + 1)) → E) → G)
        m :
      G)

Tactic:
simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
      ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, EmbeddingLike.apply_eq_iff_eq]

Premises used: ContinuousLinearMap.coe_comp', EmbeddingLike.apply_eq_iff_eq, ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply, ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply, ContinuousLinearEquiv.coe_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
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E} (hx : x ∈ s),
    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).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))
x : E
hx : x ∈ s
m : (i : Fin (i + 1)) → E
Z :
  Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s) s x)
    (fderivWithin 𝕜
      (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F)
        (⇑(continuousMultilinearMapCongrRight (fun (x : Fin i) ↦ E) g) :
          (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) G)
        (iteratedFDerivWithin 𝕜 i f s))
      s x)
succ succ₁ :
  Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      F)
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : Fin i) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      F)
    ((iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) m : F)

Tactic:
rw [iteratedFDerivWithin_succ_apply_left]

Premises used: iteratedFDerivWithin_succ_apply_left
-- 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
g : F ≃L[𝕜] G
i : ℕ
simp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x)
    ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f univ x))
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDeriv 𝕜 i ((⇑g : (a : F) → G) ∘ f) x)
    ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (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
f : E → F
x : E
g : F ≃L[𝕜] G
i : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) univ x)
    ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f univ x))

Tactic:
apply g.iteratedFDerivWithin_comp_left f uniqueDiffOn_univ trivial

Premises used: trivial, uniqueDiffOn_univ, ContinuousLinearEquiv.iteratedFDerivWithin_comp_left
-- 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
n : ℕ∞ω
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ 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.toContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))

Tactic:
have :
    iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
      g.toContinuousLinearMap.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x) :=
    g.toContinuousLinearMap.iteratedFDerivWithin_comp_left hf hs hx hi
-- 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
n : ℕ∞ω
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
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.toContinuousLinearMap.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.toContinuousLinearMap.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
n : ℕ∞ω
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
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.toContinuousLinearMap.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.toContinuousLinearMap.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

Premises used: LinearIsometry.norm_compContinuousMultilinearMap