awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_10
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₁
s : Set M
hg : ContMDiffOn I (E' := F₁ →L[𝕜] F₃) 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s
hf : ContMDiffOn I (E' := F₂ →L[𝕜] F₁) 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s
⊢ ContMDiffOn I (E' := F₂ →L[𝕜] F₃) 𝓘(𝕜, F₂ →L[𝕜] F₃) (M' := F₂ →L[𝕜] F₃) n (fun (x : M) ↦ g x ∘SL f x) s

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

Premises used: ContMDiffWithinAt.clm_comp, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_10
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₁
hg : ContMDiff I (E' := F₁ →L[𝕜] F₃) 𝓘(𝕜, F₁ →L[𝕜] F₃) n g
hf : ContMDiff I (E' := F₂ →L[𝕜] F₁) 𝓘(𝕜, F₂ →L[𝕜] F₁) n f
⊢ ContMDiff I (E' := F₂ →L[𝕜] F₃) 𝓘(𝕜, F₂ →L[𝕜] F₃) (M' := F₂ →L[𝕜] F₃) n fun (x : M) ↦ g x ∘SL f x

Tactic:
fun x => (hg x).clm_comp (hf x)

Premises used: ContMDiff, ContMDiffAt.clm_comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : ContMDiffWithinAt I (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x
hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x
h : ContDiff 𝕜 (F := F₂) n fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2
⊢ ContDiffWithinAt 𝕜 (F := F₂) n (fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2) univ (g x, f x)

Tactic:
apply ContDiff.contDiffAt

Premises used: ContDiff.contDiffAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : ContMDiffWithinAt I (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x
hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x
⊢ ContDiff 𝕜 (F := F₂) n fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2

Tactic:
contDiff_fst.clm_apply contDiff_snd

Premises used: contDiff_fst, ContDiff.clm_apply, contDiff_snd
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : ContMDiffWithinAt I (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x
hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x
⊢ ContDiff 𝕜 (F := F₂) n fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2

Tactic:
exact contDiff_fst.clm_apply contDiff_snd

Premises used: contDiff_fst, ContDiff.clm_apply, contDiff_snd
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₂
f : M → F₁
x : M
hg : ContMDiffAt I (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) n g x
hf : ContMDiffAt I 𝓘(𝕜, F₁) n f x
⊢ ContMDiffAt I 𝓘(𝕜, F₂) (M' := F₂) n (fun (x : M) ↦ (g x : (a : F₁) → F₂) (f x)) x

Tactic:
hg.clm_apply hf

Premises used: ContMDiffAt, ContMDiffWithinAt.clm_apply
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
hg : ContMDiffOn I (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s
hf : ContMDiffOn I 𝓘(𝕜, F₁) n f s
⊢ ContMDiffOn I 𝓘(𝕜, F₂) (M' := F₂) n (fun (x : M) ↦ (g x : (a : F₁) → F₂) (f x)) s

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

Premises used: ContMDiffWithinAt.clm_apply, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₂
f : M → F₁
hg : ContMDiff I (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) n g
hf : ContMDiff I 𝓘(𝕜, F₁) n f
⊢ ContMDiff I 𝓘(𝕜, F₂) (M' := F₂) n fun (x : M) ↦ (g x : (a : F₁) → F₂) (f x)

Tactic:
fun x => (hg x).clm_apply (hf x)

Premises used: ContMDiff, ContMDiffAt.clm_apply
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_10
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_11
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
n : WithTop ℕ∞
f : M → F₁ ≃L[𝕜] F₂
g : M → F₃ ≃L[𝕜] F₄
s : Set M
x : M
hf :
  ContMDiffWithinAt I (E' := F₂ →L[𝕜] F₁) 𝓘(𝕜, F₂ →L[𝕜] F₁) (M' := F₂ →L[𝕜] F₁) n
    (fun (x : M) ↦ (↑(f x).symm : F₂ →L[𝕜] F₁)) s x
hg :
  ContMDiffWithinAt I (E' := F₃ →L[𝕜] F₄) 𝓘(𝕜, F₃ →L[𝕜] F₄) (M' := F₃ →L[𝕜] F₄) n (fun (x : M) ↦ (↑(g x) : F₃ →L[𝕜] F₄))
    s x
⊢ ContMDiffWithinAt I (E' := (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) (M' :=
    (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) n (fun (y : M) ↦ (↑((f y).arrowCongr (g y)) : (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) s x

Tactic:
show ContMDiffWithinAt I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) n
    (fun y ↦ (((f y).symm : F₂ →L[𝕜] F₁).precomp F₄).comp ((g y : F₃ →L[𝕜] F₄).postcomp F₁)) s x
  from hf.clm_precomp (F₃ := F₄) |>.clm_comp <| hg.clm_postcomp (F₁ := F₁)

Premises used: ContinuousLinearMap.comp, ContMDiffWithinAt.clm_postcomp, ContMDiffWithinAt.clm_precomp, ContMDiffWithinAt.clm_comp, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_10
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_11
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
n : WithTop ℕ∞
f : M → F₁ ≃L[𝕜] F₂
g : M → F₃ ≃L[𝕜] F₄
x : M
hf :
  ContMDiffAt I (E' := F₂ →L[𝕜] F₁) 𝓘(𝕜, F₂ →L[𝕜] F₁) (M' := F₂ →L[𝕜] F₁) n (fun (x : M) ↦ (↑(f x).symm : F₂ →L[𝕜] F₁))
    x
hg : ContMDiffAt I (E' := F₃ →L[𝕜] F₄) 𝓘(𝕜, F₃ →L[𝕜] F₄) (M' := F₃ →L[𝕜] F₄) n (fun (x : M) ↦ (↑(g x) : F₃ →L[𝕜] F₄)) x
⊢ ContMDiffAt I (E' := (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) (M' :=
    (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) n (fun (y : M) ↦ (↑((f y).arrowCongr (g y)) : (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) x

Tactic:
hf.cle_arrowCongr hg

Premises used: ContMDiffAt, ContMDiffWithinAt.cle_arrowCongr
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_10
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_11
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
n : WithTop ℕ∞
f : M → F₁ ≃L[𝕜] F₂
g : M → F₃ ≃L[𝕜] F₄
s : Set M
hf :
  ContMDiffOn I (E' := F₂ →L[𝕜] F₁) 𝓘(𝕜, F₂ →L[𝕜] F₁) (M' := F₂ →L[𝕜] F₁) n (fun (x : M) ↦ (↑(f x).symm : F₂ →L[𝕜] F₁))
    s
hg : ContMDiffOn I (E' := F₃ →L[𝕜] F₄) 𝓘(𝕜, F₃ →L[𝕜] F₄) (M' := F₃ →L[𝕜] F₄) n (fun (x : M) ↦ (↑(g x) : F₃ →L[𝕜] F₄)) s
⊢ ContMDiffOn I (E' := (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) (M' :=
    (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) n (fun (y : M) ↦ (↑((f y).arrowCongr (g y)) : (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) s

Tactic:
fun x hx ↦
  (hf x hx).cle_arrowCongr (hg x hx)

Premises used: ContMDiffWithinAt.cle_arrowCongr, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_10
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_11
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
n : WithTop ℕ∞
f : M → F₁ ≃L[𝕜] F₂
g : M → F₃ ≃L[𝕜] F₄
hf : ContMDiff I (E' := F₂ →L[𝕜] F₁) 𝓘(𝕜, F₂ →L[𝕜] F₁) (M' := F₂ →L[𝕜] F₁) n fun (x : M) ↦ (↑(f x).symm : F₂ →L[𝕜] F₁)
hg : ContMDiff I (E' := F₃ →L[𝕜] F₄) 𝓘(𝕜, F₃ →L[𝕜] F₄) (M' := F₃ →L[𝕜] F₄) n fun (x : M) ↦ (↑(g x) : F₃ →L[𝕜] F₄)
⊢ ContMDiff I (E' := (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) (M' :=
    (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) n fun (y : M) ↦ (↑((f y).arrowCongr (g y)) : (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)

Tactic:
fun x ↦
  (hf x).cle_arrowCongr (hg x)

Premises used: ContMDiff, ContMDiffAt.cle_arrowCongr
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_10
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_11
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₄
s : Set M
x : M
hg : ContMDiffWithinAt I (E' := F₁ →L[𝕜] F₃) 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s x
hf : ContMDiffWithinAt I (E' := F₂ →L[𝕜] F₄) 𝓘(𝕜, F₂ →L[𝕜] F₄) n f s x
⊢ ContMDiffWithinAt I (E' := F₁ × F₂ →L[𝕜] F₃ × F₄) 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) (M' := F₁ × F₂ →L[𝕜] F₃ × F₄) n
    (fun (x : M) ↦ (g x).prodMap (f x)) s x

Tactic:
ContDiff.comp_contMDiffWithinAt (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₄) => x.1.prodMap x.2)
    (f := fun x => (g x, f x)) (ContinuousLinearMap.prodMapL 𝕜 F₁ F₃ F₂ F₄).contDiff
    (hg.prodMk_space hf)

Premises used: setOf, ContMDiffWithinAt.prodMk_space, ContinuousLinearMap.prodMap, ContDiff.comp_contMDiffWithinAt, ContinuousLinearMap.prod, ContinuousLinearMap.contDiff, ContinuousLinearMap.prodMapL
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_10
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_11
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₄
x : M
hg : ContMDiffAt I (E' := F₁ →L[𝕜] F₃) 𝓘(𝕜, F₁ →L[𝕜] F₃) n g x
hf : ContMDiffAt I (E' := F₂ →L[𝕜] F₄) 𝓘(𝕜, F₂ →L[𝕜] F₄) n f x
⊢ ContMDiffAt I (E' := F₁ × F₂ →L[𝕜] F₃ × F₄) 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) (M' := F₁ × F₂ →L[𝕜] F₃ × F₄) n
    (fun (x : M) ↦ (g x).prodMap (f x)) x

Tactic:
hg.clm_prodMap hf

Premises used: ContMDiffAt, ContMDiffWithinAt.clm_prodMap
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_10
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_11
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₄
s : Set M
hg : ContMDiffOn I (E' := F₁ →L[𝕜] F₃) 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s
hf : ContMDiffOn I (E' := F₂ →L[𝕜] F₄) 𝓘(𝕜, F₂ →L[𝕜] F₄) n f s
⊢ ContMDiffOn I (E' := F₁ × F₂ →L[𝕜] F₃ × F₄) 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) (M' := F₁ × F₂ →L[𝕜] F₃ × F₄) n
    (fun (x : M) ↦ (g x).prodMap (f x)) s

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

Premises used: ContMDiffWithinAt.clm_prodMap, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_8
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_10
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
F₄ : Type u_11
inst_12 : NormedAddCommGroup F₄
inst_13 : NormedSpace 𝕜 F₄
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₄
hg : ContMDiff I (E' := F₁ →L[𝕜] F₃) 𝓘(𝕜, F₁ →L[𝕜] F₃) n g
hf : ContMDiff I (E' := F₂ →L[𝕜] F₄) 𝓘(𝕜, F₂ →L[𝕜] F₄) n f
⊢ ContMDiff I (E' := F₁ × F₂ →L[𝕜] F₃ × F₄) 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) (M' := F₁ × F₂ →L[𝕜] F₃ × F₄) n fun (x : M) ↦
    (g x).prodMap (f x)

Tactic:
fun x =>
  (hg x).clm_prodMap (hf x)

Premises used: ContMDiff, ContMDiffAt.clm_prodMap
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : M
f : M → M'
hf : ContMDiffWithinAt I I' n f s x₀
hmn : m + 1 ≤ n
hx : x₀ ∈ s
hs : UniqueMDiffOn I s
⊢ ContMDiffWithinAt.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} (I.prod I) I' (M' := M') n (fun (x : M × M) ↦ f x.2) (s ×ˢ s)
    (x₀, x₀)

Tactic:
have : CMDiffAt[s ×ˢ s] n (fun x : M × M ↦ f x.2) (x₀, x₀) :=
    hf.comp (x₀, x₀) contMDiffWithinAt_snd mapsTo_snd_prod
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : M
f : M → M'
hf : ContMDiffWithinAt I I' n f s x₀
hmn : m + 1 ≤ n
hx : x₀ ∈ s
hs : UniqueMDiffOn I s
this :
  ContMDiffWithinAt.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} (I.prod I) I' (M' := M') n (fun (x : M × M) ↦ f x.2) (s ×ˢ s)
    (x₀, x₀)
⊢ ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' id f (mfderivWithin I I' f s) x₀)
    s x₀

Tactic:
this.mfderivWithin contMDiffWithinAt_id hx (mapsTo_id _) hmn hs

Premises used: Set.mapsTo_id, contMDiffWithinAt_id, ContMDiffWithinAt.mfderivWithin
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : M
f : M → M'
hf : ContMDiffWithinAt I I' n f s x₀
hmn : m + 1 ≤ n
hx : x₀ ∈ s
hs : UniqueMDiffOn I s
this :
  ContMDiffWithinAt.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} (I.prod I) I' (M' := M') n (fun (x : M × M) ↦ f x.2) (s ×ˢ s)
    (x₀, x₀)
⊢ ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' id f (mfderivWithin I I' f s) x₀)
    s x₀

Tactic:
exact this.mfderivWithin contMDiffWithinAt_id hx (mapsTo_id _) hmn hs

Premises used: Set.mapsTo_id, contMDiffWithinAt_id, ContMDiffWithinAt.mfderivWithin
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
Js : IsManifold J 1 N
F' : Type u_11
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_12
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N'
f : N → M → M'
g : N → M
g₁ : N' → N
g₂ : N' → E
t : Set N
u : Set M
v : Set N'
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (g₁ x₀, g (g₁ x₀))
hg : ContMDiffWithinAt J I m g t (g₁ x₀)
hg₁ : ContMDiffWithinAt J' J m g₁ v x₀
hg₂ : ContMDiffWithinAt J' 𝓘(𝕜, E) m g₂ v x₀
hmn : m + 1 ≤ n
h'g₁ : MapsTo g₁ v t
hg₁x₀ : g₁ x₀ ∈ t
h'g : MapsTo g t u
hu : UniqueMDiffOn I u
⊢ ContMDiffWithinAt J' 𝓘(𝕜, E') (M' := E') m
    (fun (x : N') ↦
      (inTangentCoordinates.{u_1, u_2, u_5, u_3, u_6, u_4, u_7, u_10} I I' (M' := M') g (fun (x : N) ↦ f x (g x))
            (fun (x : N) ↦ mfderivWithin I I' (f x) u (g x)) (g₁ x₀) (g₁ x) :
          (a : E) → E')
        (g₂ x))
    v x₀

Tactic:
((hf.mfderivWithin hg hg₁x₀ h'g hmn hu).comp_of_eq hg₁ h'g₁ rfl).clm_apply hg₂

Premises used: ContMDiffWithinAt.comp_of_eq, ContMDiffWithinAt.mfderivWithin, ContMDiffWithinAt.clm_apply, rfl
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)
hg : ContMDiffAt J I m g x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)

Tactic:
rw [← contMDiffWithinAt_univ] at hf hg ⊢

Premises used: contMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_9
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)
hg : ContMDiffAt J I m g x₀
hmn : m + 1 ≤ n
hf₁ : ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)
⊢ ContMDiffWithinAt J I m g univ x₀

Tactic:
rw [← contMDiffWithinAt_univ] at hf hg ⊢

Premises used: contMDiffWithinAt_univ