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
f : E → F
n_1 : ℕ∞ω
x : G
g : G →L[𝕜] E
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s ((g : (a : G) → E) x)
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ MapsTo (α := G) (⇑g : (a : G) → E) (insert x ((⇑g : (a : G) → E) ⁻¹' s)) (insert (α := E) ((g : (a : G) → E) x : E) s)

Tactic:
(mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)

Premises used: Iff.mpr, Set.mem_singleton, Set.insert, Set.Mem, setOf, Set.mapsTo_preimage, Set.singleton, Set.MapsTo.union_union, Set.mapsTo_singleton
-- 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_1 : ℕ∞ω
x : G
g : G →L[𝕜] E
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s ((g : (a : G) → E) x)
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝[insert (α := E) ((g : (a : G) → E) x : E) s] (g : (a : G) → E) x : Filter E) u
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ MapsTo (α := G) (⇑g : (a : G) → E) (insert x ((⇑g : (a : G) → E) ⁻¹' s)) (insert (α := E) ((g : (a : G) → E) x : E) s)

Tactic:
exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)

Premises used: Iff.mpr, Set.mem_singleton, Set.mapsTo_preimage, Set.MapsTo.union_union, Set.mapsTo_singleton
-- 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 : ℕ∞ω
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 n f s ((g : (a : G) → E) x)
⊢ ContDiffWithinAt 𝕜 n (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x

Tactic:
match n with
  | ω =>
    obtain ⟨u, hu, p, hp, h'p⟩ := hf
    refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g, ?_⟩
    · refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu
      exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)
    · intro i
      change AnalyticOn 𝕜 (fun x ↦
        ContinuousMultilinearMap.compContinuousLinearMapL (fun _ ↦ g) (p (g x) i)) (⇑g ⁻¹' u)
      apply AnalyticOn.comp _ _ (Set.mapsTo_univ _ _)
      · exact ContinuousLinearMap.analyticOn _ _
      · exact (h'p i).comp (g.analyticOn _) (mapsTo_preimage _ _)
  | (n : ℕ∞) =>
    intro m hm
    rcases hf m hm with ⟨u, hu, p, hp⟩
    refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g⟩
    refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu
    exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)
-- 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 : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
g : G →L[𝕜] E
⊢ ContDiffOn.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s)

Tactic:
fun x hx => (hf (g x) hx).comp_continuousLinearMap g

Premises used: ContDiffOn, ContDiffWithinAt.comp_continuousLinearMap, 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
n : ℕ∞ω
f : E → F
g : G →L[𝕜] E
hf : ContDiff 𝕜 n f
⊢ ContDiff.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑g : (a : G) → E))

Tactic:
contDiffOn_univ.1 <| ContDiffOn.comp_continuousLinearMap (contDiffOn_univ.2 hf) _

Premises used: Iff.mpr, Iff.mp, ContDiffOn.comp_continuousLinearMap, 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
n : ℕ∞ω
f : E → F
g : G →L[𝕜] E
hf : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
h's : UniqueDiffOn.{u_1, u_4} 𝕜 (E := G) ((⇑g : (a : G) → E) ⁻¹' s)
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (x : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ g)

Tactic:
((((hf.of_le hi).ftaylorSeriesWithin hs).compContinuousLinearMap
    g).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl h's hx).symm

Premises used: le_rfl, ftaylorSeriesWithin, HasFTaylorSeriesUpToOn.compContinuousLinearMap, ContDiffOn.of_le, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn, Eq.symm, 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
s : Set E
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
zero :
  ∀ (m : (i : Fin 0) → G),
    Eq.{u_3 + 1} (α := F)
      ((iteratedFDerivWithin 𝕜 0 (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x : (a : (i : Fin 0) → G) → F) m :
        F)
      ((ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
              (iteratedFDerivWithin 𝕜 0 f s ((g : (a : G) → E) x)) fun (x : Fin 0) ↦ (↑g : G →L[𝕜] E) :
            (a : (i : Fin 0) → G) → F)
          m :
        F)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin 0) ↦ G) F)
    (iteratedFDerivWithin 𝕜 0 (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
      (iteratedFDerivWithin 𝕜 0 f s ((g : (a : G) → E) x)) fun (x : Fin 0) ↦ (↑g : G →L[𝕜] E))

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 : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
m : (i : Fin 0) → G
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 0 (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x : (a : (i : Fin 0) → G) → F) m : F)
    ((ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
            (iteratedFDerivWithin 𝕜 0 f s ((g : (a : G) → E) x)) fun (x : Fin 0) ↦ (↑g : G →L[𝕜] E) :
          (a : (i : Fin 0) → G) → F)
        m :
      F)

Tactic:
simp only [iteratedFDerivWithin_zero_apply, comp_apply,
      ContinuousMultilinearMap.compContinuousLinearMap_apply]

Premises used: ContinuousMultilinearMap.compContinuousLinearMap_apply, Function.comp_apply, 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 : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G} (hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
        (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑g : G →L[𝕜] E))
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
succ :
  ∀ (m : (i : Fin (i + 1)) → G),
    Eq.{u_3 + 1} (α := F)
      ((iteratedFDerivWithin 𝕜 (i + 1) (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x :
            (a : (i : Fin (i + 1)) → G) → F)
          m :
        F)
      ((ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin (i + 1)) ↦ G) (M₁' :=
              fun (i : Fin (i + 1)) ↦ E) (iteratedFDerivWithin 𝕜 (i + 1) f s ((g : (a : G) → E) x))
              fun (x : Fin (i + 1)) ↦ (↑g : G →L[𝕜] E) :
            (a : (i : Fin (i + 1)) → G) → F)
          m :
        F)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin (i + 1)) ↦ G) F)
    (iteratedFDerivWithin 𝕜 (i + 1) (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin (i + 1)) ↦ G) (M₁' := fun (i : Fin (i + 1)) ↦
      E) (iteratedFDerivWithin 𝕜 (i + 1) f s ((g : (a : G) → E) x)) fun (x : Fin (i + 1)) ↦ (↑g : G →L[𝕜] E))

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

Tactic:
simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply,
      ContinuousLinearEquiv.coe_coe, iteratedFDerivWithin_succ_apply_left]

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

Tactic:
have : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s)) (g ⁻¹' s) x =
        fderivWithin 𝕜
          (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft _ (fun _x : Fin i => g) ∘
            (iteratedFDerivWithin 𝕜 i f s ∘ g)) (g ⁻¹' 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
n : ℕ∞ω
g : G →L[𝕜] E
f : E → F
hf : ContDiff 𝕜 n f
x : G
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
simp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) univ x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (x : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f univ ((g : (a : G) → E) x)) fun (x : Fin i) ↦ g)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (iteratedFDeriv 𝕜 i (f ∘ (⇑g : (a : G) → E)) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (x : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
      (iteratedFDeriv 𝕜 i f ((g : (a : G) → E) x)) fun (x : Fin i) ↦ g)

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

Tactic:
g.iteratedFDerivWithin_comp_right hf.contDiffOn uniqueDiffOn_univ uniqueDiffOn_univ
      (mem_univ _) hi

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

Tactic:
exact g.iteratedFDerivWithin_comp_right hf.contDiffOn uniqueDiffOn_univ uniqueDiffOn_univ
      (mem_univ _) hi

Premises used: ContDiff.contDiffOn, ContinuousLinearMap.iteratedFDerivWithin_comp_right, 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
g : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
i : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑(↑g : G ≃L[𝕜] E) : G →L[𝕜] E))

Tactic:
have : iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s) x =
      (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun _ => g :=
    g.toContinuousLinearEquiv.iteratedFDerivWithin_comp_right 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
g : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
i : ℕ
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑(↑g : G ≃L[𝕜] E) : G →L[𝕜] E))
rw :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
        (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑(↑g : G ≃L[𝕜] E) : G →L[𝕜] E)) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x))
rw₁ rw₂ :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x))
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x))

Tactic:
rw [this, ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv]

Premises used: ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv
-- 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 : G ≃ₗᵢ[𝕜] E
f : E → F
x : G
i : ℕ
simp :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) univ x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f univ ((g : (a : G) → E) x))
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDeriv 𝕜 i (f ∘ (⇑g : (a : G) → E)) x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv 𝕜 i f ((g : (a : G) → E) 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
g : G ≃ₗᵢ[𝕜] E
f : E → F
x : G
i : ℕ
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) univ x) =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f univ ((g : (a : G) → E) x))

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

Premises used: uniqueDiffOn_univ, LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right, Set.mem_univ, 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
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
mp :
  ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((⇑e : (a : G) → E) ⁻¹' s : Set G)
      ((e.symm : (a : E) → G) x : G) →
    ContDiffWithinAt 𝕜 n f s x
mpr :
  ContDiffWithinAt 𝕜 n f s x →
    ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((⇑e : (a : G) → E) ⁻¹' s : Set G)
      ((e.symm : (a : E) → G) x : G)
⊢ ContDiffWithinAt.{u_1, u_4, u_3} 𝕜 (E := G) n (f ∘ (⇑e : (a : G) → E) : G → F) ((⇑e : (a : G) → E) ⁻¹' s : Set G)
      ((e.symm : (a : E) → G) x : G) ↔
    ContDiffWithinAt 𝕜 n f s x

Tactic:
constructor