awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
i : ℕ
hi : (↑i : ℕ∞ω) ≤ n
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (iteratedFDerivWithin 𝕜 i (g ∘ f) s x)
    (FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g t (f x)) (ftaylorSeriesWithin 𝕜 f s x) i)

Tactic:
iteratedFDerivWithin_comp_of_eventually_mem hg hf ht hs hx (eventually_mem_nhdsWithin.mono hst) hi

Premises used: eventually_mem_nhdsWithin, Filter.Eventually.mono, iteratedFDerivWithin_comp_of_eventually_mem
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
g : F → G
x : E
n : ℕ∞ω
hg : ContDiffAt 𝕜 n g (f x)
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 ∘ f) univ x)
    (FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g univ (f x)) (ftaylorSeriesWithin 𝕜 f univ x) i)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) (iteratedFDeriv 𝕜 i (g ∘ f) x)
    (FormalMultilinearSeries.taylorComp (ftaylorSeries 𝕜 g (f x)) (ftaylorSeries 𝕜 f x) i)

Tactic:
simp only [← iteratedFDerivWithin_univ, ← ftaylorSeriesWithin_univ]

Premises used: ftaylorSeriesWithin_univ, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
g : F → G
x : E
n : ℕ∞ω
hg : ContDiffAt 𝕜 n g (f x)
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 ∘ f) univ x)
    (FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g univ (f x)) (ftaylorSeriesWithin 𝕜 f univ x) i)

Tactic:
iteratedFDerivWithin_comp hg.contDiffWithinAt hf.contDiffWithinAt
    uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _) (mapsTo_univ _ _) hi

Premises used: Set.mapsTo_univ, uniqueDiffOn_univ, iteratedFDerivWithin_comp, Set.mem_univ, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
g : F → G
x : E
n : ℕ∞ω
hg : ContDiffAt 𝕜 n g (f x)
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 ∘ f) univ x)
    (FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g univ (f x)) (ftaylorSeriesWithin 𝕜 f univ x) i)

Tactic:
exact iteratedFDerivWithin_comp hg.contDiffWithinAt hf.contDiffWithinAt
    uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _) (mapsTo_univ _ _) hi

Premises used: Set.mapsTo_univ, uniqueDiffOn_univ, iteratedFDerivWithin_comp, Set.mem_univ, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
⊢ ContDiff 𝕜 (E := E × F) n Prod.fst

Tactic:
IsBoundedLinearMap.contDiff IsBoundedLinearMap.fst

Premises used: IsBoundedLinearMap.contDiff, IsBoundedLinearMap.fst
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
hf : ContDiff 𝕜 n f
⊢ ContDiff.{u_1, u_2, u_3} 𝕜 (F := F) n fun (x : E) ↦ (f x).1

Tactic:
contDiff_fst.comp hf

Premises used: contDiff_fst, ContDiff.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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 → G
hf : ContDiff 𝕜 n f
⊢ ContDiff 𝕜 (F := G) n fun (x : E × F) ↦ f x.1

Tactic:
hf.comp contDiff_fst

Premises used: contDiff_fst, ContDiff.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
s : Set (E × F)
⊢ ContDiffOn 𝕜 n Prod.fst s

Tactic:
ContDiff.contDiffOn contDiff_fst

Premises used: contDiff_fst, ContDiff.contDiffOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
s : Set E
hf : ContDiffOn 𝕜 n f s
⊢ ContDiffOn.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ (f x).1) s

Tactic:
contDiff_fst.comp_contDiffOn hf

Premises used: contDiff_fst, ContDiff.comp_contDiffOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
p : E × F
⊢ ContDiffAt 𝕜 n Prod.fst p

Tactic:
contDiff_fst.contDiffAt

Premises used: contDiff_fst, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
x : E
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ (f x).1) x

Tactic:
contDiffAt_fst.comp x hf

Premises used: ContDiffAt.comp, contDiffAt_fst
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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 → G
x : E
y : F
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt 𝕜 (F := G) n (fun (x : E × F) ↦ f x.1) (x, y)

Tactic:
ContDiffAt.comp (x, y) hf contDiffAt_fst

Premises used: Prod.mk, ContDiffAt.comp, contDiffAt_fst
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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 → G
x : E × F
hf : ContDiffAt 𝕜 n f x.1
⊢ ContDiffAt 𝕜 (F := G) n (fun (x : E × F) ↦ f x.1) x

Tactic:
hf.comp x contDiffAt_fst

Premises used: ContDiffAt.comp, contDiffAt_fst
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
s : Set (E × F)
p : E × F
⊢ ContDiffWithinAt 𝕜 n Prod.fst s p

Tactic:
contDiff_fst.contDiffWithinAt

Premises used: contDiff_fst, ContDiff.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
x : E
hf : ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) n (fun (x : E) ↦ (f x).1) s x

Tactic:
contDiffWithinAt_fst.comp x hf (mapsTo_image f s)

Premises used: contDiffWithinAt_fst, Set.mapsTo_image, ContDiffWithinAt.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
⊢ ContDiff 𝕜 (E := E × F) n Prod.snd

Tactic:
IsBoundedLinearMap.contDiff IsBoundedLinearMap.snd

Premises used: IsBoundedLinearMap.contDiff, IsBoundedLinearMap.snd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
hf : ContDiff 𝕜 n f
⊢ ContDiff.{u_1, u_2, u_4} 𝕜 (F := G) n fun (x : E) ↦ (f x).2

Tactic:
contDiff_snd.comp hf

Premises used: ContDiff.comp, contDiff_snd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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 : F → G
hf : ContDiff 𝕜 n f
⊢ ContDiff 𝕜 (F := G) n fun (x : E × F) ↦ f x.2

Tactic:
hf.comp contDiff_snd

Premises used: ContDiff.comp, contDiff_snd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
s : Set (E × F)
⊢ ContDiffOn 𝕜 n Prod.snd s

Tactic:
ContDiff.contDiffOn contDiff_snd

Premises used: ContDiff.contDiffOn, contDiff_snd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
s : Set E
hf : ContDiffOn 𝕜 n f s
⊢ ContDiffOn.{u_1, u_2, u_4} 𝕜 (F := G) n (fun (x : E) ↦ (f x).2) s

Tactic:
contDiff_snd.comp_contDiffOn hf

Premises used: ContDiff.comp_contDiffOn, contDiff_snd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
s : Set (E × F)
p : E × F
⊢ ContDiffWithinAt 𝕜 n Prod.snd s p

Tactic:
contDiff_snd.contDiffWithinAt

Premises used: ContDiff.contDiffWithinAt, contDiff_snd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
p : E × F
⊢ ContDiffAt 𝕜 n Prod.snd p

Tactic:
contDiff_snd.contDiffAt

Premises used: contDiff_snd, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
x : E
hf : ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) n (fun (x : E) ↦ (f x).2) s x

Tactic:
contDiffWithinAt_snd.comp x hf (mapsTo_image f s)

Premises used: Set.mapsTo_image, ContDiffWithinAt.comp, contDiffWithinAt_snd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
x : E
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt.{u_1, u_2, u_4} 𝕜 (F := G) n (fun (x : E) ↦ (f x).2) x

Tactic:
contDiffAt_snd.comp x hf

Premises used: contDiffAt_snd, ContDiffAt.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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 : F → G
x : E
y : F
hf : ContDiffAt 𝕜 n f y
⊢ ContDiffAt 𝕜 (F := G) n (fun (x : E × F) ↦ f x.2) (x, y)

Tactic:
ContDiffAt.comp (x, y) hf contDiffAt_snd

Premises used: contDiffAt_snd, Prod.mk, ContDiffAt.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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 : F → G
x : E × F
hf : ContDiffAt 𝕜 n f x.2
⊢ ContDiffAt 𝕜 (F := G) n (fun (x : E × F) ↦ f x.2) x

Tactic:
hf.comp x contDiffAt_snd

Premises used: contDiffAt_snd, ContDiffAt.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ContDiffWithinAt 𝕜 n (Prod.fst ∘ f) s x ∧ ContDiffWithinAt 𝕜 n (Prod.snd ∘ f) s x

Tactic:
⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩

Premises used: ContDiffWithinAt.snd, ContDiffWithinAt.fst, And.right, And.left, And.intro, Iff.intro, ContDiffWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
⊢ ContDiffAt 𝕜 n f x ↔ ContDiffAt 𝕜 n (Prod.fst ∘ f) x ∧ ContDiffAt 𝕜 n (Prod.snd ∘ f) x

Tactic:
⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩

Premises used: And.right, And.left, And.intro, Iff.intro, ContDiffAt.fst, ContDiffAt.prodMk, ContDiffAt.snd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
⊢ ContDiffOn 𝕜 n f s ↔ ContDiffOn 𝕜 n (Prod.fst ∘ f) s ∧ ContDiffOn 𝕜 n (Prod.snd ∘ f) s

Tactic:
⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩

Premises used: ContDiffOn.fst, And.right, And.left, And.intro, Iff.intro, ContDiffOn.prodMk, ContDiffOn.snd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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
⊢ ContDiff 𝕜 n f ↔ ContDiff 𝕜 n (Prod.fst ∘ f) ∧ ContDiff 𝕜 n (Prod.snd ∘ f)

Tactic:
⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩

Premises used: ContDiff.fst, ContDiff.prodMk, And.right, And.left, And.intro, Iff.intro, ContDiff.snd
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
n : ℕ∞ω
E₁ : Type u_6
E₂ : Type u_7
inst_5 : NormedAddCommGroup E₁
inst_6 : NormedAddCommGroup E₂
inst_7 : NormedSpace 𝕜 E₁
inst_8 : NormedSpace 𝕜 E₂
g : E₁ × E₂ → G
f₁ : F → E₁
f₂ : F → E₂
hg : ContDiff 𝕜 n g
hf₁ : ContDiff 𝕜 n f₁
hf₂ : ContDiff 𝕜 n f₂
⊢ ContDiff.{u_1, u_3, u_4} 𝕜 (F := G) n fun (x : F) ↦ g (f₁ x, f₂ x)

Tactic:
hg.comp <| hf₁.prodMk hf₂

Premises used: ContDiff.prodMk, ContDiff.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
n : ℕ∞ω
E₁ : Type u_6
E₂ : Type u_7
inst_5 : NormedAddCommGroup E₁
inst_6 : NormedAddCommGroup E₂
inst_7 : NormedSpace 𝕜 E₁
inst_8 : NormedSpace 𝕜 E₂
g : E₁ × E₂ → G
f₁ : F → E₁
f₂ : F → E₂
x : F
hg : ContDiffAt 𝕜 n g (f₁ x, f₂ x)
hf₁ : ContDiffAt 𝕜 n f₁ x
hf₂ : ContDiffAt 𝕜 n f₂ x
⊢ ContDiffAt.{u_1, u_3, u_4} 𝕜 (F := G) n (fun (x : F) ↦ g (f₁ x, f₂ x)) x

Tactic:
hg.comp x (hf₁.prodMk hf₂)

Premises used: ContDiffAt.comp, ContDiffAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
n : ℕ∞ω
E₁ : Type u_6
E₂ : Type u_7
inst_5 : NormedAddCommGroup E₁
inst_6 : NormedAddCommGroup E₂
inst_7 : NormedSpace 𝕜 E₁
inst_8 : NormedSpace 𝕜 E₂
g : E₁ × E₂ → G
f₁ : F → E₁
f₂ : F → E₂
s : Set F
x : F
hg : ContDiffAt 𝕜 n g (f₁ x, f₂ x)
hf₁ : ContDiffWithinAt 𝕜 n f₁ s x
hf₂ : ContDiffWithinAt 𝕜 n f₂ s x
⊢ ContDiffWithinAt.{u_1, u_3, u_4} 𝕜 (F := G) n (fun (x : F) ↦ g (f₁ x, f₂ x)) s x

Tactic:
hg.comp_contDiffWithinAt x (hf₁.prodMk hf₂)

Premises used: ContDiffAt.comp_contDiffWithinAt, ContDiffWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
n : ℕ∞ω
E₁ : Type u_6
E₂ : Type u_7
inst_5 : NormedAddCommGroup E₁
inst_6 : NormedAddCommGroup E₂
inst_7 : NormedSpace 𝕜 E₁
inst_8 : NormedSpace 𝕜 E₂
g : E₁ × E₂ → G
f₁ : F → E₁
f₂ : F → E₂
x : F
hg : ContDiff 𝕜 n g
hf₁ : ContDiffAt 𝕜 n f₁ x
hf₂ : ContDiffAt 𝕜 n f₂ x
⊢ ContDiffAt.{u_1, u_3, u_4} 𝕜 (F := G) n (fun (x : F) ↦ g (f₁ x, f₂ x)) x

Tactic:
hg.contDiffAt.comp₂ hf₁ hf₂

Premises used: ContDiffAt.comp₂, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
n : ℕ∞ω
E₁ : Type u_6
E₂ : Type u_7
inst_5 : NormedAddCommGroup E₁
inst_6 : NormedAddCommGroup E₂
inst_7 : NormedSpace 𝕜 E₁
inst_8 : NormedSpace 𝕜 E₂
g : E₁ × E₂ → G
f₁ : F → E₁
f₂ : F → E₂
s : Set F
x : F
hg : ContDiff 𝕜 n g
hf₁ : ContDiffWithinAt 𝕜 n f₁ s x
hf₂ : ContDiffWithinAt 𝕜 n f₂ s x
⊢ ContDiffWithinAt.{u_1, u_3, u_4} 𝕜 (F := G) n (fun (x : F) ↦ g (f₁ x, f₂ x)) s x

Tactic:
hg.contDiffAt.comp_contDiffWithinAt x (hf₁.prodMk hf₂)

Premises used: ContDiffAt.comp_contDiffWithinAt, ContDiffWithinAt.prodMk, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
n : ℕ∞ω
E₁ : Type u_6
E₂ : Type u_7
inst_5 : NormedAddCommGroup E₁
inst_6 : NormedAddCommGroup E₂
inst_7 : NormedSpace 𝕜 E₁
inst_8 : NormedSpace 𝕜 E₂
g : E₁ × E₂ → G
f₁ : F → E₁
f₂ : F → E₂
s : Set F
hg : ContDiff 𝕜 n g
hf₁ : ContDiffOn 𝕜 n f₁ s
hf₂ : ContDiffOn 𝕜 n f₂ s
⊢ ContDiffOn.{u_1, u_3, u_4} 𝕜 (F := G) n (fun (x : F) ↦ g (f₁ x, f₂ x)) s

Tactic:
hg.comp_contDiffOn <| hf₁.prodMk hf₂

Premises used: ContDiff.comp_contDiffOn, ContDiffOn.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
n : ℕ∞ω
E₁ : Type u_6
E₂ : Type u_7
E₃ : Type u_8
inst_5 : NormedAddCommGroup E₁
inst_6 : NormedAddCommGroup E₂
inst_7 : NormedAddCommGroup E₃
inst_8 : NormedSpace 𝕜 E₁
inst_9 : NormedSpace 𝕜 E₂
inst_10 : NormedSpace 𝕜 E₃
g : E₁ × E₂ × E₃ → G
f₁ : F → E₁
f₂ : F → E₂
f₃ : F → E₃
hg : ContDiff 𝕜 n g
hf₁ : ContDiff 𝕜 n f₁
hf₂ : ContDiff 𝕜 n f₂
hf₃ : ContDiff 𝕜 n f₃
⊢ ContDiff.{u_1, u_3, u_4} 𝕜 (F := G) n fun (x : F) ↦ g (f₁ x, f₂ x, f₃ x)

Tactic:
hg.comp₂ hf₁ <| hf₂.prodMk hf₃

Premises used: ContDiff.prodMk, ContDiff.comp₂
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
n : ℕ∞ω
E₁ : Type u_6
E₂ : Type u_7
E₃ : Type u_8
inst_5 : NormedAddCommGroup E₁
inst_6 : NormedAddCommGroup E₂
inst_7 : NormedAddCommGroup E₃
inst_8 : NormedSpace 𝕜 E₁
inst_9 : NormedSpace 𝕜 E₂
inst_10 : NormedSpace 𝕜 E₃
g : E₁ × E₂ × E₃ → G
f₁ : F → E₁
f₂ : F → E₂
f₃ : F → E₃
s : Set F
hg : ContDiff 𝕜 n g
hf₁ : ContDiffOn 𝕜 n f₁ s
hf₂ : ContDiffOn 𝕜 n f₂ s
hf₃ : ContDiffOn 𝕜 n f₃ s
⊢ ContDiffOn.{u_1, u_3, u_4} 𝕜 (F := G) n (fun (x : F) ↦ g (f₁ x, f₂ x, f₃ x)) s

Tactic:
hg.comp₂_contDiffOn hf₁ <| hf₂.prodMk hf₃

Premises used: ContDiff.comp₂_contDiffOn, ContDiffOn.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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 : Type u_5
inst_7 : NormedAddCommGroup X
inst_8 : NormedSpace 𝕜 X
n : ℕ∞ω
g : X → F →L[𝕜] G
f : X → E →L[𝕜] F
hg : ContDiff 𝕜 n g
hf : ContDiff 𝕜 n f
⊢ ContDiff 𝕜 (F := E →L[𝕜] G) n fun (x : X) ↦ g x ∘SL f x

Tactic:
isBoundedBilinearMap_comp.contDiff.comp₂ (g := fun p => p.1.comp p.2) hg hf

Premises used: IsBoundedBilinearMap.contDiff, ContDiff.comp₂
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
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 : Type u_5
inst_7 : NormedAddCommGroup X
inst_8 : NormedSpace 𝕜 X
n : ℕ∞ω
g : X → F →L[𝕜] G
f : X → E →L[𝕜] F
s : Set X
hg : ContDiffOn 𝕜 n g s
hf : ContDiffOn 𝕜 n f s
⊢ ContDiffOn 𝕜 (F := E →L[𝕜] G) n (fun (x : X) ↦ g x ∘SL f x) s

Tactic:
(isBoundedBilinearMap_comp (E := E) (F := F) (G := G)).contDiff.comp₂_contDiffOn hg hf

Premises used: IsBoundedBilinearMap.contDiff, ContDiff.comp₂_contDiffOn