awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set (M × M')
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivWithinAt I J f (Prod.fst '' s) p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivWithinAt I' J' g (Prod.snd '' s) p.2 dg
better :
  (↑(extChartAt (I.prod I') p).symm : E × E' → M × M') ⁻¹' s ∩ range (↑(I.prod I') : ModelProd H H' → E × E') ⊆
    ((↑(extChartAt I p.1).symm : E → M) ⁻¹' Prod.fst '' s ∩ range (↑I : H → E)) ×ˢ
      ((↑(extChartAt I' p.2).symm : E' → M') ⁻¹' Prod.snd '' s ∩ range (↑I' : H' → E'))
⊢ HasFDerivWithinAt (writtenInExtChartAt I J p.1 f) df
    (Prod.fst ''
      ((↑(extChartAt I p.1).symm : E → M) ⁻¹' Prod.fst '' s ∩ range (↑I : H → E)) ×ˢ
        ((↑(extChartAt I' p.2).symm : E' → M') ⁻¹' Prod.snd '' s ∩ range (↑I' : H' → E')))
    ((↑(extChartAt (I.prod I') p) : M × M' → E × E') p).1

Tactic:
exacts [hf.2.mono (fst_image_prod_subset ..), hg.2.mono (snd_image_prod_subset ..)]

Premises used: Set.snd_image_prod_subset, Set.fst_image_prod_subset, And.right, HasFDerivWithinAt.mono
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivAt I J f p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivAt I' J' g p.2 dg
simp_rw :
  HasMFDerivWithinAt (I.prod I') (J.prod J') (Prod.map f g) (SProd.sprod (α := Set M) (β := Set M') univ univ) p
    (ContinuousLinearMap.prodMap (mfderivWithin I J f univ p.1) (mfderivWithin I' J' g univ p.2))
⊢ HasMFDerivAt (I.prod I') (J.prod J') (Prod.map f g) p (ContinuousLinearMap.prodMap (mfderiv% f p.1) (mfderiv% g p.2))

Tactic:
simp_rw [← hasMFDerivWithinAt_univ, ← mfderivWithin_univ, ← univ_prod_univ]

Premises used: mfderivWithin_univ, Set.univ_prod_univ, hasMFDerivWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivAt I J f p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivAt I' J' g p.2 dg
⊢ HasMFDerivWithinAt (I.prod I') (J.prod J') (Prod.map f g) (SProd.sprod (α := Set M) (β := Set M') univ univ) p
    (df.prodMap dg)

Tactic:
hf.hasMFDerivWithinAt.prodMap hg.hasMFDerivWithinAt

Premises used: HasMFDerivWithinAt.prodMap, HasMFDerivAt.hasMFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivAt I J f p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivAt I' J' g p.2 dg
h : mfderivWithin I J f univ p.1 = df
h₁ :
  TangentSpace I' p.2 = E' →
    HEq (α := TopologicalSpace (TangentSpace I' p.2)) (instTopologicalSpaceTangentSpace I' p.2) (β :=
        TopologicalSpace E') UniformSpace.toTopologicalSpace →
      HEq.{u_5 + 1} (α := AddCommMonoid (TangentSpace I' p.2)) AddCommGroup.toAddCommMonoid (β := AddCommMonoid E')
          AddCommGroup.toAddCommMonoid →
        HEq (α := Module.{u_1, u_5} 𝕜 (TangentSpace I' p.2)) (instModuleTangentSpace I' p.2) (β := Module 𝕜 E')
            (NormedSpace.toModule : Module 𝕜 E') →
          TangentSpace J' (g p.2) = F' →
            HEq (α := TopologicalSpace (TangentSpace J' (g p.2))) (instTopologicalSpaceTangentSpace J' (g p.2)) (β :=
                TopologicalSpace F') UniformSpace.toTopologicalSpace →
              HEq.{u_14 + 1} (α := AddCommMonoid (TangentSpace J' (g p.2))) AddCommGroup.toAddCommMonoid (β :=
                  AddCommMonoid F') AddCommGroup.toAddCommMonoid →
                HEq (α := Module.{u_1, u_14} 𝕜 (TangentSpace J' (g p.2))) (instModuleTangentSpace J' (g p.2)) (β :=
                    Module 𝕜 F') (NormedSpace.toModule : Module 𝕜 F') →
                  mfderivWithin I' J' g univ p.2 = dg
⊢ HasMFDerivWithinAt (I.prod I') (J.prod J') (Prod.map f g) (SProd.sprod (α := Set M) (β := Set M') univ univ) p
    (ContinuousLinearMap.prodMap (mfderivWithin I J f univ p.1) (mfderivWithin I' J' g univ p.2))

Tactic:
convert! hf.hasMFDerivWithinAt.prodMap hg.hasMFDerivWithinAt

Premises used: HasMFDerivWithinAt.prodMap, HasMFDerivAt.hasMFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivAt I J f p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivAt I' J' g p.2 dg
h : mfderiv% f p.1 = df
⊢ mfderivWithin I J f univ p.1 = df

Tactic:
rw [mfderivWithin_univ]

Premises used: mfderivWithin_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivAt I J f p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivAt I' J' g p.2 dg
⊢ mfderiv% f p.1 = df

Tactic:
hf.mfderiv

Premises used: HasMFDerivAt.mfderiv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivAt I J f p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivAt I' J' g p.2 dg
⊢ mfderiv% f p.1 = df

Tactic:
exact hf.mfderiv

Premises used: HasMFDerivAt.mfderiv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivAt I J f p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivAt I' J' g p.2 dg
e_11 : TangentSpace I' p.2 = E'
e_12 :
  HEq (α := TopologicalSpace (TangentSpace I' p.2)) (instTopologicalSpaceTangentSpace I' p.2) (β := TopologicalSpace E')
    UniformSpace.toTopologicalSpace
e_13 :
  HEq.{u_5 + 1} (α := AddCommMonoid (TangentSpace I' p.2)) AddCommGroup.toAddCommMonoid (β := AddCommMonoid E')
    AddCommGroup.toAddCommMonoid
e_14 :
  HEq (α := Module.{u_1, u_5} 𝕜 (TangentSpace I' p.2)) (instModuleTangentSpace I' p.2) (β := Module 𝕜 E')
    (NormedSpace.toModule : Module 𝕜 E')
e_15 : TangentSpace J' (g p.2) = F'
e_16 :
  HEq (α := TopologicalSpace (TangentSpace J' (g p.2))) (instTopologicalSpaceTangentSpace J' (g p.2)) (β :=
    TopologicalSpace F') UniformSpace.toTopologicalSpace
e_17 :
  HEq.{u_14 + 1} (α := AddCommMonoid (TangentSpace J' (g p.2))) AddCommGroup.toAddCommMonoid (β := AddCommMonoid F')
    AddCommGroup.toAddCommMonoid
e_18 :
  HEq (α := Module.{u_1, u_14} 𝕜 (TangentSpace J' (g p.2))) (instModuleTangentSpace J' (g p.2)) (β := Module 𝕜 F')
    (NormedSpace.toModule : Module 𝕜 F')
h : mfderiv% g p.2 = dg
⊢ mfderivWithin I' J' g univ p.2 = dg

Tactic:
rw [mfderivWithin_univ]

Premises used: mfderivWithin_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivAt I J f p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivAt I' J' g p.2 dg
e_11 : TangentSpace I' p.2 = E'
e_12 :
  HEq (α := TopologicalSpace (TangentSpace I' p.2)) (instTopologicalSpaceTangentSpace I' p.2) (β := TopologicalSpace E')
    UniformSpace.toTopologicalSpace
e_13 :
  HEq.{u_5 + 1} (α := AddCommMonoid (TangentSpace I' p.2)) AddCommGroup.toAddCommMonoid (β := AddCommMonoid E')
    AddCommGroup.toAddCommMonoid
e_14 :
  HEq (α := Module.{u_1, u_5} 𝕜 (TangentSpace I' p.2)) (instModuleTangentSpace I' p.2) (β := Module 𝕜 E')
    (NormedSpace.toModule : Module 𝕜 E')
e_15 : TangentSpace J' (g p.2) = F'
e_16 :
  HEq (α := TopologicalSpace (TangentSpace J' (g p.2))) (instTopologicalSpaceTangentSpace J' (g p.2)) (β :=
    TopologicalSpace F') UniformSpace.toTopologicalSpace
e_17 :
  HEq.{u_14 + 1} (α := AddCommMonoid (TangentSpace J' (g p.2))) AddCommGroup.toAddCommMonoid (β := AddCommMonoid F')
    AddCommGroup.toAddCommMonoid
e_18 :
  HEq (α := Module.{u_1, u_14} 𝕜 (TangentSpace J' (g p.2))) (instModuleTangentSpace J' (g p.2)) (β := Module 𝕜 F')
    (NormedSpace.toModule : Module 𝕜 F')
⊢ mfderiv% g p.2 = dg

Tactic:
hg.mfderiv

Premises used: HasMFDerivAt.mfderiv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivAt I J f p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivAt I' J' g p.2 dg
e_11 : TangentSpace I' p.2 = E'
e_12 :
  HEq (α := TopologicalSpace (TangentSpace I' p.2)) (instTopologicalSpaceTangentSpace I' p.2) (β := TopologicalSpace E')
    UniformSpace.toTopologicalSpace
e_13 :
  HEq.{u_5 + 1} (α := AddCommMonoid (TangentSpace I' p.2)) AddCommGroup.toAddCommMonoid (β := AddCommMonoid E')
    AddCommGroup.toAddCommMonoid
e_14 :
  HEq (α := Module.{u_1, u_5} 𝕜 (TangentSpace I' p.2)) (instModuleTangentSpace I' p.2) (β := Module 𝕜 E')
    (NormedSpace.toModule : Module 𝕜 E')
e_15 : TangentSpace J' (g p.2) = F'
e_16 :
  HEq (α := TopologicalSpace (TangentSpace J' (g p.2))) (instTopologicalSpaceTangentSpace J' (g p.2)) (β :=
    TopologicalSpace F') UniformSpace.toTopologicalSpace
e_17 :
  HEq.{u_14 + 1} (α := AddCommMonoid (TangentSpace J' (g p.2))) AddCommGroup.toAddCommMonoid (β := AddCommMonoid F')
    AddCommGroup.toAddCommMonoid
e_18 :
  HEq (α := Module.{u_1, u_14} 𝕜 (TangentSpace J' (g p.2))) (instModuleTangentSpace J' (g p.2)) (β := Module 𝕜 F')
    (NormedSpace.toModule : Module 𝕜 F')
⊢ mfderiv% g p.2 = dg

Tactic:
exact hg.mfderiv

Premises used: HasMFDerivAt.mfderiv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set M
p : M × M'
t : Set M'
f : M → N
g : M' → N'
hf : MDiffAt[s] f p.1
hg : MDiffAt[t] g p.2
hs : UniqueMDiffWithinAt I s p.1
ht : UniqueMDiffWithinAt I' t p.2
⊢ Prod.fst '' s ×ˢ t ⊆ s

Tactic:
grind
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set M
p : M × M'
t : Set M'
f : M → N
g : M' → N'
hf : MDiffAt[s] f p.1
hg : MDiffAt[t] g p.2
hs : UniqueMDiffWithinAt I s p.1
ht : UniqueMDiffWithinAt I' t p.2
⊢ HasMFDerivWithinAt I J f (Prod.fst '' s ×ˢ t) p.1 (mfderivWithin I J f s p.1)

Tactic:
have hf' : HasMFDerivAt[Prod.fst '' s ×ˢ t] f p.1 (mfderiv[s] f p.1) :=
    hf.hasMFDerivWithinAt.mono (by grind)
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
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 : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set M
p : M × M'
t : Set M'
f : M → N
g : M' → N'
hf : MDiffAt[s] f p.1
hg : MDiffAt[t] g p.2
hs : UniqueMDiffWithinAt I s p.1
ht : UniqueMDiffWithinAt I' t p.2
hf' : HasMFDerivWithinAt I J f (Prod.fst '' s ×ˢ t) p.1 (mfderivWithin I J f s p.1)
⊢ Prod.snd '' s ×ˢ t ⊆ t

Tactic:
grind