awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
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 f₁ : M → M'
n : ℕ∞ω
h : ContMDiffOn I I' n f univ
h₁ : ∀ (y : M), f₁ y = f y
⊢ ContMDiffOn I I' n f₁ univ

Tactic:
exact (contMDiffOn_congr fun y _ ↦ h₁ y).mpr h

Premises used: Iff.mpr, contMDiffOn_congr
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
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 f₁ : M → M'
n : ℕ∞ω
h₁ : ∀ (y : M), f₁ y = f y
simp_rw : ContMDiffOn I I' n f₁ univ ↔ ContMDiffOn I I' n f univ
⊢ ContMDiff I I' n f₁ ↔ ContMDiff I I' n f

Tactic:
simp_rw [← contMDiffOn_univ]

Premises used: contMDiffOn_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
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 f₁ : M → M'
n : ℕ∞ω
h₁ : ∀ (y : M), f₁ y = f y
⊢ ContMDiffOn I I' n f₁ univ ↔ ContMDiffOn I I' n f univ

Tactic:
contMDiffOn_congr fun y _ ↦ h₁ y

Premises used: contMDiffOn_congr
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
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 f₁ : M → M'
n : ℕ∞ω
h₁ : ∀ (y : M), f₁ y = f y
⊢ ContMDiffOn I I' n f₁ univ ↔ ContMDiffOn I I' n f univ

Tactic:
exact contMDiffOn_congr fun y _ ↦ h₁ y

Premises used: contMDiffOn_congr
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
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 : M → M'
s : Set M
n : ℕ∞ω
h : ∀ x ∈ s, ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' n f (s ∩ u)
⊢ ContMDiffOn I I' n f s

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropOn_of_locally_liftPropOn h

Premises used: ContMDiffWithinAt, ChartedSpace.LiftPropOn, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropOn_of_locally_liftPropOn, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
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 : M → M'
n : ℕ∞ω
h : ∀ (x : M), ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' n f u
⊢ ContMDiff I I' n f

Tactic:
(contDiffWithinAt_localInvariantProp n).liftProp_of_locally_liftPropOn h

Premises used: ChartedSpace.LiftProp, ContMDiffWithinAt, ContMDiff, StructureGroupoid.LocalInvariantProp.liftProp_of_locally_liftPropOn, contDiffWithinAt_localInvariantProp, ContMDiffAt, ChartedSpace.LiftPropAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
s : Set E
x : E
simp : ContDiffWithinAt 𝕜 n f s x → ContinuousWithinAt f s x
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
simp +contextual only [ContMDiffWithinAt, liftPropWithinAt_iff',
    ContDiffWithinAtProp, iff_def, mfld_simps]

Premises used: ContMDiffWithinAt, iff_def, ContDiffWithinAtProp, ChartedSpace.liftPropWithinAt_iff'
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
s : Set E
x : E
⊢ ContDiffWithinAt 𝕜 n f s x → ContinuousWithinAt f s x

Tactic:
ContDiffWithinAt.continuousWithinAt

Premises used: ContDiffWithinAt.continuousWithinAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
s : Set E
x : E
⊢ ContDiffWithinAt 𝕜 n f s x → ContinuousWithinAt f s x

Tactic:
exact ContDiffWithinAt.continuousWithinAt

Premises used: ContDiffWithinAt.continuousWithinAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
x : E
rw : ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f univ x ↔ ContDiffAt 𝕜 n f x
rw₁ : ContDiffWithinAt 𝕜 n f univ x ↔ ContDiffAt 𝕜 n f x
rw₂ rw₃ : ContDiffAt 𝕜 n f x ↔ ContDiffAt 𝕜 n f x
⊢ ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f x ↔ ContDiffAt 𝕜 n f x

Tactic:
rw [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_contDiffWithinAt, contDiffWithinAt_univ]

Premises used: contDiffWithinAt_univ, contMDiffWithinAt_iff_contDiffWithinAt, contMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
s : Set E
⊢ ∀ (a : E), a ∈ s → ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f s a ↔ a ∈ s → ContDiffWithinAt 𝕜 n f s a

Tactic:
simp [contMDiffWithinAt_iff_contDiffWithinAt]

Premises used: contMDiffWithinAt_iff_contDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
rw : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiffOn 𝕜 n f univ
rw₁ : ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E') n f univ ↔ ContDiffOn 𝕜 n f univ
rw₂ rw₃ : ContDiffOn 𝕜 n f univ ↔ ContDiffOn 𝕜 n f univ
⊢ ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiff 𝕜 n f

Tactic:
rw [← contDiffOn_univ, ← contMDiffOn_univ, contMDiffOn_iff_contDiffOn]

Premises used: contMDiffOn_iff_contDiffOn, contMDiffOn_univ, contDiffOn_univ
-- 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_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
F' : Type u_7
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
n : WithTop ℕ∞
g : F → F'
f : M → F
s : Set M
t : Set F
x : M
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContMDiffWithinAt I 𝓘(𝕜, F) n f s x
h : s ⊆ f ⁻¹' t
⊢ ContMDiffWithinAt I 𝓘(𝕜, F') n (g ∘ f) s x

Tactic:
hg.contMDiffWithinAt.comp x hf h

Premises used: ContDiffWithinAt.contMDiffWithinAt, ContMDiffWithinAt.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_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
F' : Type u_7
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
n : WithTop ℕ∞
g : F → F'
f : M → F
s : Set M
x : M
hg : ContDiffAt 𝕜 n g (f x)
hf : ContMDiffWithinAt I 𝓘(𝕜, F) n f s x
⊢ ContMDiffWithinAt I 𝓘(𝕜, F') n (g ∘ f) s x

Tactic:
hg.contMDiffAt.comp_contMDiffWithinAt x hf

Premises used: ContDiffAt.contMDiffAt, ContMDiffAt.comp_contMDiffWithinAt
-- 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_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
F' : Type u_7
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
n : WithTop ℕ∞
g : F → F'
f : M → F
x : M
hg : ContDiffAt 𝕜 n g (f x)
hf : ContMDiffAt I 𝓘(𝕜, F) n f x
⊢ ContMDiffAt I 𝓘(𝕜, F') n (g ∘ f) x

Tactic:
hg.comp_contMDiffWithinAt hf

Premises used: ContDiffAt.comp_contMDiffWithinAt, ContMDiffAt
-- 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_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
F' : Type u_7
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
n : ℕ∞ω
g : F → F'
f : M → F
s : Set M
x : M
hg : ContDiff 𝕜 n g
hf : ContMDiffWithinAt I 𝓘(𝕜, F) n f s x
⊢ ContMDiffWithinAt I 𝓘(𝕜, F') n (g ∘ f) s x

Tactic:
hg.contDiffAt.comp_contMDiffWithinAt hf

Premises used: ContDiffAt.comp_contMDiffWithinAt, 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_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
F' : Type u_7
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
n : ℕ∞ω
g : F → F'
f : M → F
x : M
hg : ContDiff 𝕜 n g
hf : ContMDiffAt I 𝓘(𝕜, F) n f x
⊢ ContMDiffAt I 𝓘(𝕜, F') n (g ∘ f) x

Tactic:
hg.comp_contMDiffWithinAt hf

Premises used: ContDiff.comp_contMDiffWithinAt, ContMDiffAt
-- 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_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
F' : Type u_7
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
n : ℕ∞ω
g : F → F'
f : M → F
hg : ContDiff 𝕜 n g
hf : ContMDiff I 𝓘(𝕜, F) n f
⊢ ContMDiff I 𝓘(𝕜, F') n (g ∘ f)

Tactic:
fun x =>
  hg.contDiffAt.comp_contMDiffAt (hf x)

Premises used: ContMDiff, ContDiffAt.comp_contMDiffAt, 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
F : Type u_6
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : WithTop ℕ∞
L : E →L[𝕜] F
⊢ ContMDiff 𝓘(𝕜, E) (M := E) 𝓘(𝕜, F) (M' := F) n (⇑L : (a : E) → F)

Tactic:
L.contDiff.contMDiff

Premises used: ContDiff.contMDiff, ContinuousLinearMap.contDiff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_6
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : WithTop ℕ∞
L : E →L[𝕜] F
x : E
⊢ ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, F) (M' := F) n (⇑L : (a : E) → F) x

Tactic:
L.contMDiff _

Premises used: ContinuousLinearMap.contMDiff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_6
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : WithTop ℕ∞
L : E →L[𝕜] F
s : Set E
x : E
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) (M' := F) n (⇑L : (a : E) → F) s x

Tactic:
L.contMDiffAt.contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, ContinuousLinearMap.contMDiffAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_6
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : WithTop ℕ∞
L : E →L[𝕜] F
s : Set E
⊢ ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, F) (M' := F) n (⇑L : (a : E) → F) s

Tactic:
L.contMDiff.contMDiffOn

Premises used: ContinuousLinearMap.contMDiff, ContMDiff.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 ℕ∞
f : M → F₁ →L[𝕜] F₂
s : Set M
x : M
hf : ContMDiffWithinAt I (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) n 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) ↦ ContinuousLinearMap.precomp F₃ (f y)) s x

Tactic:
ContDiff.comp_contMDiffWithinAt (g := (ContinuousLinearMap.compL 𝕜 F₁ F₂ F₃).flip)
    (ContinuousLinearMap.contDiff _) hf

Premises used: ContinuousLinearMap.comp, LinearMap.mkContinuousOfExistsBound, ContinuousLinearMap.precomp, ContDiff.comp_contMDiffWithinAt, ContinuousLinearMap.contDiff
-- 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 ℕ∞
f : M → F₁ →L[𝕜] F₂
x : M
hf : ContMDiffAt I (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) n 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) ↦ ContinuousLinearMap.precomp F₃ (f y)) x

Tactic:
hf.clm_precomp

Premises used: ContMDiffAt, ContMDiffWithinAt.clm_precomp
-- 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 ℕ∞
f : M → F₁ →L[𝕜] F₂
s : Set M
hf : ContMDiffOn I (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) n 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) ↦ ContinuousLinearMap.precomp F₃ (f y)) s

Tactic:
fun x hx ↦
  (hf x hx).clm_precomp

Premises used: ContMDiffWithinAt.clm_precomp, 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 ℕ∞
f : M → F₁ →L[𝕜] F₂
hf : ContMDiff I (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) n 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) ↦ ContinuousLinearMap.precomp F₃ (f y)

Tactic:
fun x ↦
  (hf x).clm_precomp

Premises used: ContMDiff, ContMDiffAt.clm_precomp
-- 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 ℕ∞
f : M → F₂ →L[𝕜] F₃
s : Set M
x : M
hf : ContMDiffWithinAt I (E' := F₂ →L[𝕜] F₃) 𝓘(𝕜, F₂ →L[𝕜] F₃) n 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) ↦ ContinuousLinearMap.postcomp F₁ (f y)) s x

Tactic:
ContDiff.comp_contMDiffWithinAt (F' := (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃))
    (g := ContinuousLinearMap.compL 𝕜 F₁ F₂ F₃) (ContinuousLinearMap.contDiff _) hf

Premises used: LinearMap.mkContinuousOfExistsBound, ContinuousLinearMap.postcomp, ContDiff.comp_contMDiffWithinAt, ContinuousLinearMap.contDiff
-- 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 ℕ∞
f : M → F₂ →L[𝕜] F₃
x : M
hf : ContMDiffAt I (E' := F₂ →L[𝕜] F₃) 𝓘(𝕜, F₂ →L[𝕜] F₃) n 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) ↦ ContinuousLinearMap.postcomp F₁ (f y)) x

Tactic:
hf.clm_postcomp

Premises used: ContMDiffWithinAt.clm_postcomp, ContMDiffAt
-- 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 ℕ∞
f : M → F₂ →L[𝕜] F₃
s : Set M
hf : ContMDiffOn I (E' := F₂ →L[𝕜] F₃) 𝓘(𝕜, F₂ →L[𝕜] F₃) n 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) ↦ ContinuousLinearMap.postcomp F₁ (f y)) s

Tactic:
fun x hx ↦
  (hf x hx).clm_postcomp

Premises used: ContMDiffWithinAt.clm_postcomp, 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 ℕ∞
f : M → F₂ →L[𝕜] F₃
hf : ContMDiff I (E' := F₂ →L[𝕜] F₃) 𝓘(𝕜, F₂ →L[𝕜] F₃) n 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) ↦ ContinuousLinearMap.postcomp F₁ (f y)

Tactic:
fun x ↦
  (hf x).clm_postcomp

Premises used: ContMDiffAt.clm_postcomp, ContMDiff
-- 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
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₂ →L[𝕜] F₃) 𝓘(𝕜, F₂ →L[𝕜] F₃) (M' := F₂ →L[𝕜] F₃) n (fun (x : M) ↦ g x ∘SL f x) s x

Tactic:
ContDiff.comp_contMDiffWithinAt (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₁) => x.1.comp x.2)
    (f := fun x => (g x, f x)) (contDiff_fst.clm_comp contDiff_snd) (hg.prodMk_space hf)

Premises used: ContinuousLinearMap.comp, contDiff_fst, ContMDiffWithinAt.prodMk_space, ContDiff.comp_contMDiffWithinAt, ContDiff.clm_comp, 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₂
F₃ : Type u_10
inst_10 : NormedAddCommGroup F₃
inst_11 : 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₂ →L[𝕜] F₃) 𝓘(𝕜, F₂ →L[𝕜] F₃) (M' := F₂ →L[𝕜] F₃) n (fun (x : M) ↦ g x ∘SL f x) x

Tactic:
(hg.contMDiffWithinAt.clm_comp hf.contMDiffWithinAt).contMDiffAt Filter.univ_mem

Premises used: ContMDiffAt.contMDiffWithinAt, ContMDiffWithinAt.contMDiffAt, Filter.univ_mem, ContMDiffWithinAt.clm_comp