awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀)
hg₁ : ContMDiffWithinAt J I m g univ x₀
⊢ m + 1 ≤ n

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 : ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt (J.prod I) I' n (uncurry f) (SProd.sprod (α := Set N) (β := Set M) univ univ) (x₀, g x₀)

Tactic:
rw [← univ_prod_univ] at hf

Premises used: Set.univ_prod_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 : ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
hf₁ : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (SProd.sprod (α := Set N) (β := Set M) univ univ) (x₀, g x₀)
⊢ ContMDiffWithinAt J I m g univ x₀

Tactic:
rw [← univ_prod_univ] at hf

Premises used: Set.univ_prod_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 : ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
hf₁ : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (SProd.sprod (α := Set N) (β := Set M) univ univ) (x₀, g x₀)
hg₁ : ContMDiffWithinAt J I m g univ x₀
⊢ m + 1 ≤ n

Tactic:
rw [← univ_prod_univ] at hf

Premises used: Set.univ_prod_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 : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (SProd.sprod (α := Set N) (β := Set M) univ univ) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
simp_rw :
  ContMDiffWithinAt J (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m
    (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) univ (g x)) x₀)
    univ x₀
⊢ ContMDiffWithinAt J (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m
    (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) ↦ mfderiv% (f x) (g x)) x₀)
    univ x₀

Tactic:
simp_rw [← mfderivWithin_univ]

Premises used: mfderivWithin_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 : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (SProd.sprod (α := Set N) (β := Set M) univ univ) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt J (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m
    (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) univ (g x)) x₀)
    univ x₀

Tactic:
ContMDiffWithinAt.mfderivWithin hf hg (mem_univ _) (mapsTo_univ _ _) hmn
    uniqueMDiffOn_univ

Premises used: Set.mapsTo_univ, uniqueMDiffOn_univ, ContMDiffWithinAt.mfderivWithin, Set.mem_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 : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (SProd.sprod (α := Set N) (β := Set M) univ univ) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt J (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m
    (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) univ (g x)) x₀)
    univ x₀

Tactic:
exact ContMDiffWithinAt.mfderivWithin hf hg (mem_univ _) (mapsTo_univ _ _) hmn
    uniqueMDiffOn_univ

Premises used: Set.mapsTo_univ, uniqueMDiffOn_univ, ContMDiffWithinAt.mfderivWithin, Set.mem_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'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : M
f : M → M'
hf : ContMDiffAt I I' n f x₀
hmn : m + 1 ≤ n
⊢ ContMDiffAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' id f (mfderiv% f) x₀) x₀

Tactic:
haveI : CMDiffAt n (fun x : M × M ↦ f x.2) (x₀, x₀) :=
    ContMDiffAt.comp (x₀, x₀) hf contMDiffAt_snd
  this.mfderiv (fun _ ↦ f) id contMDiffAt_id hmn

Premises used: id, Prod.mk, contMDiffAt_id, ContMDiffAt.mfderiv, ContMDiffAt.comp, contMDiffAt_snd
-- 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
hf : ContMDiffAt (J.prod I) I' n (uncurry f) (g₁ x₀, g (g₁ x₀))
hg : ContMDiffAt J I m g (g₁ x₀)
hg₁ : ContMDiffAt J' J m g₁ x₀
hg₂ : ContMDiffAt J' 𝓘(𝕜, E) m g₂ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffAt 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) ↦ mfderiv% (f x) (g x)) (g₁ x₀) (g₁ x) :
          (a : E) → E')
        (g₂ x))
    x₀

Tactic:
((hf.mfderiv f g hg hmn).comp_of_eq hg₁ rfl).clm_apply hg₂

Premises used: ContMDiffAt.comp_of_eq, ContMDiffAt.mfderiv, ContMDiffAt.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 : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
x₀ : TangentBundle I M
hx₀ : Membership.mem (γ := Set (TangentBundle I M)) (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
s' : Set (TangentBundle I M) := TotalSpace.proj (E := TangentSpace I) ⁻¹' s
b₁ : TangentBundle I M → M := fun (p : TangentBundle I M) ↦ p.proj (E := TangentSpace I)
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun (y : TangentBundle I M) ↦ y.snd (E := TangentSpace I)
⊢ ContMDiffWithinAt I.tangent I.tangent (M' := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) m
    (fun (y : TangentBundle I M) ↦ ⟨b₁ y, v y⟩) s' x₀

Tactic:
have hv : ContMDiffWithinAt I.tangent I.tangent m (fun y ↦ (v y : TangentBundle I M)) s' x₀ :=
    contMDiffWithinAt_id
-- 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 : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
x₀ : TangentBundle I M
hx₀ : Membership.mem (γ := Set (TangentBundle I M)) (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
s' : Set (TangentBundle I M) := TotalSpace.proj (E := TangentSpace I) ⁻¹' s
b₁ : TangentBundle I M → M := fun (p : TangentBundle I M) ↦ p.proj (E := TangentSpace I)
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun (y : TangentBundle I M) ↦ y.snd (E := TangentSpace I)
hv :
  ContMDiffWithinAt I.tangent I.tangent (M' := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) m
    (fun (y : TangentBundle I M) ↦ ⟨b₁ y, v y⟩) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
⊢ ContMDiffWithinAt I.tangent I' m b₂ s' x₀

Tactic:
have hb₂ : CMDiffAt[s'] m b₂ x₀ :=
    ((hf (b₁ x₀) hx₀).of_le (le_self_add.trans hmn)).comp _
      (contMDiffWithinAt_proj (TangentSpace I)) (fun x h ↦ h)
-- 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 : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
x₀ : TangentBundle I M
hx₀ : Membership.mem (γ := Set (TangentBundle I M)) (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
s' : Set (TangentBundle I M) := TotalSpace.proj (E := TangentSpace I) ⁻¹' s
b₁ : TangentBundle I M → M := fun (p : TangentBundle I M) ↦ p.proj (E := TangentSpace I)
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun (y : TangentBundle I M) ↦ y.snd (E := TangentSpace I)
hv :
  ContMDiffWithinAt I.tangent I.tangent (M' := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) m
    (fun (y : TangentBundle I M) ↦ ⟨b₁ y, v y⟩) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀
ϕ : (y : TangentBundle I M) →
  ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (b₁ y)) (TangentSpace I' (b₂ y)) :=
  fun (y : TangentBundle I M) ↦ mfderivWithin I I' f s (b₁ y)
⊢ ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (y : M) ↦
      ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) y (b₂ x₀) (f y)
        (mfderivWithin I I' f s y))
    s (b₁ x₀)

Tactic:
have A : CMDiffAt[s] m (fun y ↦ ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E'
        (TangentSpace I' (M := M')) (b₁ x₀) y (b₂ x₀) (f y) (mfderiv[s] f y)) (b₁ x₀) :=
      .mfderivWithin_const (hf _ hx₀) hmn hx₀ hs
-- 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 : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
x₀ : TangentBundle I M
hx₀ : Membership.mem (γ := Set (TangentBundle I M)) (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
s' : Set (TangentBundle I M) := TotalSpace.proj (E := TangentSpace I) ⁻¹' s
b₁ : TangentBundle I M → M := fun (p : TangentBundle I M) ↦ p.proj (E := TangentSpace I)
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun (y : TangentBundle I M) ↦ y.snd (E := TangentSpace I)
hv :
  ContMDiffWithinAt I.tangent I.tangent (M' := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) m
    (fun (y : TangentBundle I M) ↦ ⟨b₁ y, v y⟩) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀
ϕ : (y : TangentBundle I M) →
  ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (b₁ y)) (TangentSpace I' (b₂ y)) :=
  fun (y : TangentBundle I M) ↦ mfderivWithin I I' f s (b₁ y)
A :
  ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (y : M) ↦
      ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) y (b₂ x₀) (f y)
        (mfderivWithin I I' f s y))
    s (b₁ x₀)
⊢ ContMDiffWithinAt I.tangent (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (y : TangentBundle I M) ↦
      ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y))
    s' x₀

Tactic:
A.comp _ (contMDiffWithinAt_proj (TangentSpace I)) (fun x h ↦ h)

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.inCoordinates, Bundle.contMDiffWithinAt_proj, TangentSpace, ContMDiffWithinAt.comp
-- 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 : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
x₀ : TangentBundle I M
hx₀ : Membership.mem (γ := Set (TangentBundle I M)) (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
s' : Set (TangentBundle I M) := TotalSpace.proj (E := TangentSpace I) ⁻¹' s
b₁ : TangentBundle I M → M := fun (p : TangentBundle I M) ↦ p.proj (E := TangentSpace I)
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun (y : TangentBundle I M) ↦ y.snd (E := TangentSpace I)
hv :
  ContMDiffWithinAt I.tangent I.tangent (M' := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) m
    (fun (y : TangentBundle I M) ↦ ⟨b₁ y, v y⟩) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀
ϕ : (y : TangentBundle I M) →
  ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (b₁ y)) (TangentSpace I' (b₂ y)) :=
  fun (y : TangentBundle I M) ↦ mfderivWithin I I' f s (b₁ y)
A :
  ContMDiffWithinAt I (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (y : M) ↦
      ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) y (b₂ x₀) (f y)
        (mfderivWithin I I' f s y))
    s (b₁ x₀)
⊢ ContMDiffWithinAt I.tangent (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (y : TangentBundle I M) ↦
      ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y))
    s' x₀

Tactic:
exact A.comp _ (contMDiffWithinAt_proj (TangentSpace I)) (fun x h ↦ h)

Premises used: Bundle.contMDiffWithinAt_proj, TangentSpace, ContMDiffWithinAt.comp
-- 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 : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
x₀ : TangentBundle I M
hx₀ : Membership.mem (γ := Set (TangentBundle I M)) (TotalSpace.proj (E := TangentSpace I) ⁻¹' s) x₀
s' : Set (TangentBundle I M) := TotalSpace.proj (E := TangentSpace I) ⁻¹' s
b₁ : TangentBundle I M → M := fun (p : TangentBundle I M) ↦ p.proj (E := TangentSpace I)
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun (y : TangentBundle I M) ↦ y.snd (E := TangentSpace I)
hv :
  ContMDiffWithinAt I.tangent I.tangent (M' := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) m
    (fun (y : TangentBundle I M) ↦ ⟨b₁ y, v y⟩) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀
ϕ : (y : TangentBundle I M) →
  ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (b₁ y)) (TangentSpace I' (b₂ y)) :=
  fun (y : TangentBundle I M) ↦ mfderivWithin I I' f s (b₁ y)
⊢ ContMDiffWithinAt I.tangent (E' := E →L[𝕜] E') 𝓘(𝕜, E →L[𝕜] E') (M' := E →L[𝕜] E') m
    (fun (y : TangentBundle I M) ↦
      ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y))
    s' x₀

Tactic:
have hϕ : CMDiffAt[s'] m (fun y ↦ ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E'
      (TangentSpace I' (M := M')) (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y)) x₀ := by
    have A : CMDiffAt[s] m (fun y ↦ ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E'
        (TangentSpace I' (M := M')) (b₁ x₀) y (b₂ x₀) (f y) (mfderiv[s] f y)) (b₁ x₀) :=
      .mfderivWithin_const (hf _ hx₀) hmn hx₀ hs
    exact A.comp _ (contMDiffWithinAt_proj (TangentSpace I)) (fun x h ↦ h)