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
p₀ : E × E'
hp₀ :
  p₀ ∈
    (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H p.1)).symm.prod
              (OpenPartialHomeomorph.toPartialEquiv (chartAt H' p.2)).symm) :
          ModelProd H H' → M × M') ∘
        (↑(I.symm.prod I'.symm) : E × E' → ModelProd H H') ⁻¹'
      s
hp₁₁ : p₀.1 ∈ range (↑I : H → E)
hp₁₂ : p₀.2 ∈ range (↑I' : H' → E')
⊢ p₀.1 ∈ range (↑I : H → E)

Tactic:
assumption
-- 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
p₀ : E × E'
hp₀ :
  p₀ ∈
    (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H p.1)).symm.prod
              (OpenPartialHomeomorph.toPartialEquiv (chartAt H' p.2)).symm) :
          ModelProd H H' → M × M') ∘
        (↑(I.symm.prod I'.symm) : E × E' → ModelProd H H') ⁻¹'
      s
hp₁₁ : p₀.1 ∈ range (↑I : H → E)
hp₁₂ : p₀.2 ∈ range (↑I' : H' → E')
simp_all :
  ∀
    (hp₀ :
      ((↑(OpenPartialHomeomorph.symm (chartAt H p.1)) : H → M) ((↑I.symm : E → H) p₀.1),
          (↑(OpenPartialHomeomorph.symm (chartAt H' p.2)) : H' → M') ((↑I'.symm : E' → H') p₀.2)) ∈
        s)
    (hp₁₁ : ∃ (y : H), (↑I : H → E) y = p₀.1) (hp₁₂ : ∃ (y : H'), (↑I' : H' → E') y = p₀.2),
    ∃ (a : M), (a, (↑(OpenPartialHomeomorph.symm (chartAt H' p.2)) : H' → M') ((↑I'.symm : E' → H') p₀.2)) ∈ s
⊢ p₀.2 ∈ (↑(OpenPartialHomeomorph.symm (chartAt H' p.2)) : H' → M') ∘ (↑I'.symm : E' → H') ⁻¹' Prod.snd '' s

Tactic:
simp_all
-- 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
p₀ : E × E'
hp₀ :
  ((↑(OpenPartialHomeomorph.symm (chartAt H p.1)) : H → M) ((↑I.symm : E → H) p₀.1),
      (↑(OpenPartialHomeomorph.symm (chartAt H' p.2)) : H' → M') ((↑I'.symm : E' → H') p₀.2)) ∈
    s
hp₁₁ : ∃ (y : H), (↑I : H → E) y = p₀.1
hp₁₂ : ∃ (y : H'), (↑I' : H' → E') y = p₀.2
⊢ ∃ (a : M), (a, (↑(OpenPartialHomeomorph.symm (chartAt H' p.2)) : H' → M') ((↑I'.symm : E' → H') p₀.2)) ∈ 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 × 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
p₀ : E × E'
hp₀ :
  p₀ ∈
    (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H p.1)).symm.prod
              (OpenPartialHomeomorph.toPartialEquiv (chartAt H' p.2)).symm) :
          ModelProd H H' → M × M') ∘
        (↑(I.symm.prod I'.symm) : E × E' → ModelProd H H') ⁻¹'
      s
hp₁₁ : p₀.1 ∈ range (↑I : H → E)
hp₁₂ : p₀.2 ∈ range (↑I' : H' → E')
⊢ p₀.2 ∈ range (↑I' : H' → E')

Tactic:
assumption
-- 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
p₀ : E × E'
hp₀ :
  p₀ ∈
    (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H p.1)).symm.prod
              (OpenPartialHomeomorph.toPartialEquiv (chartAt H' p.2)).symm) :
          ModelProd H H' → M × M') ∘
        (↑(I.symm.prod I'.symm) : E × E' → ModelProd H H') ⁻¹'
      s
hp₁₁ : p₀.1 ∈ range (↑I : H → E)
hp₁₂ : p₀.2 ∈ range (↑I' : H' → E')
⊢ p₀ ∈
    ((↑(OpenPartialHomeomorph.symm (chartAt H p.1)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' Prod.fst '' s ∩
        range (↑I : H → E)) ×ˢ
      ((↑(OpenPartialHomeomorph.symm (chartAt H' p.2)) : H' → M') ∘ (↑I'.symm : E' → H') ⁻¹' Prod.snd '' s ∩
        range (↑I' : H' → E'))

Tactic:
exact ⟨⟨by simp_all; grind, by assumption⟩, ⟨by simp_all; grind, by assumption⟩⟩
-- 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
⊢ (↑(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'))

Tactic:
have better : ((extChartAt (I.prod I') p).symm ⁻¹' s ∩ range ↑(I.prod I')) ⊆
      ((extChartAt I p.1).symm ⁻¹' (Prod.fst '' s) ∩ range I) ×ˢ
        ((extChartAt I' p.2).symm ⁻¹' (Prod.snd '' s) ∩ range I') := by
    simp only [mfld_simps]
    rw [range_prodMap, I.toPartialEquiv.prod_symm, (chartAt H p.1).toPartialEquiv.prod_symm]
    intro p₀ ⟨hp₀, ⟨hp₁₁, hp₁₂⟩⟩
    exact ⟨⟨by simp_all; grind, by assumption⟩, ⟨by simp_all; grind, by assumption⟩⟩
-- 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'))
rw :
  HasFDerivWithinAt (𝕜 := 𝕜) (Prod.map (writtenInExtChartAt I J p.1 f) (writtenInExtChartAt I' J' p.2 g))
    (df.prodMap dg)
    ((↑(extChartAt (I.prod I') p).symm : E × E' → M × M') ⁻¹' s ∩ range (↑(I.prod I') : ModelProd H H' → E × E'))
    ((↑(extChartAt (I.prod I') p) : M × M' → E × E') p)
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (writtenInExtChartAt (I.prod I') (J.prod J') p (Prod.map f g)) (df.prodMap dg)
    ((↑(extChartAt (I.prod I') p).symm : E × E' → M × M') ⁻¹' s ∩ range (↑(I.prod I') : ModelProd H H' → E × E'))
    ((↑(extChartAt (I.prod I') p) : M × M' → E × E') p)

Tactic:
rw [writtenInExtChartAt_prod]

Premises used: writtenInExtChartAt_prod
-- 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'))
apply :
  HasFDerivWithinAt (𝕜 := 𝕜) (Prod.map (writtenInExtChartAt I J p.1 f) (writtenInExtChartAt I' J' p.2 g))
    (df.prodMap dg)
    (((↑(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)
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (Prod.map (writtenInExtChartAt I J p.1 f) (writtenInExtChartAt I' J' p.2 g))
    (df.prodMap dg)
    ((↑(extChartAt (I.prod I') p).symm : E × E' → M × M') ⁻¹' s ∩ range (↑(I.prod I') : ModelProd H H' → E × E'))
    ((↑(extChartAt (I.prod I') p) : M × M' → E × E') p)

Tactic:
apply HasFDerivWithinAt.mono ?_ better

Premises used: 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'
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'))
hf₁ :
  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
hf₂ :
  HasFDerivWithinAt (writtenInExtChartAt I' J' p.2 g) dg
    (Prod.snd ''
      ((↑(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).2
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (Prod.map (writtenInExtChartAt I J p.1 f) (writtenInExtChartAt I' J' p.2 g))
    (df.prodMap dg)
    (((↑(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)

Tactic:
apply HasFDerivWithinAt.prodMap

Premises used: HasFDerivWithinAt.prodMap
-- 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:
hf.2.mono (fst_image_prod_subset ..)

Premises used: Set.fst_image_prod_subset, ModelWithCorners.toFun', instModuleTangentSpace._aux_1, And.right, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, HasFDerivWithinAt.mono, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4
-- 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.2 g) dg
    (Prod.snd ''
      ((↑(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).2

Tactic:
hg.2.mono (snd_image_prod_subset ..)

Premises used: Set.snd_image_prod_subset, ModelWithCorners.toFun', instModuleTangentSpace._aux_1, And.right, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, HasFDerivWithinAt.mono, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4