Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁶ : TopologicalSpace M
inst✝¹⁵ : ChartedSpace H M
E' : Type u_5
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝¹² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹¹ : TopologicalSpace M'
inst✝¹⁰ : ChartedSpace H' M'
F : Type u_11
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_12
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
s : Set (M × M')
p : M × M'
f : M → N
g : M' → N'
df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)
hf : HasMFDerivAt[Prod.fst '' s] f p.1 df
dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)
hg : HasMFDerivAt[Prod.snd '' s] g p.2 dg
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')
⊢ HasFDerivWithinAt (Prod.map (writtenInExtChartAt I J p.1 f) (writtenInExtChartAt I' J' p.2 g)) (df.prodMap dg)
    ((↑(extChartAt I p.1).symm ⁻¹' Prod.fst '' s ∩ range ↑I) ×ˢ
      (↑(extChartAt I' p.2).symm ⁻¹' Prod.snd '' s ∩ range ↑I'))
    (↑(extChartAt (I.prod I') p) p)

Tactic:
apply HasFDerivWithinAt.prodMap

Goal state after:
case hf
𝕜 : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁶ : TopologicalSpace M
inst✝¹⁵ : ChartedSpace H M
E' : Type u_5
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝¹² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹¹ : TopologicalSpace M'
inst✝¹⁰ : ChartedSpace H' M'
F : Type u_11
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_12
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
s : Set (M × M')
p : M × M'
f : M → N
g : M' → N'
df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)
hf : HasMFDerivAt[Prod.fst '' s] f p.1 df
dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)
hg : HasMFDerivAt[Prod.snd '' s] g p.2 dg
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')
⊢ HasFDerivWithinAt (writtenInExtChartAt I J p.1 f) df
    (Prod.fst ''
      (↑(extChartAt I p.1).symm ⁻¹' Prod.fst '' s ∩ range ↑I) ×ˢ
        (↑(extChartAt I' p.2).symm ⁻¹' Prod.snd '' s ∩ range ↑I'))
    (↑(extChartAt (I.prod I') p) p).1

case hf₂
𝕜 : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁶ : TopologicalSpace M
inst✝¹⁵ : ChartedSpace H M
E' : Type u_5
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝¹² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹¹ : TopologicalSpace M'
inst✝¹⁰ : ChartedSpace H' M'
F : Type u_11
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_12
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
s : Set (M × M')
p : M × M'
f : M → N
g : M' → N'
df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)
hf : HasMFDerivAt[Prod.fst '' s] f p.1 df
dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)
hg : HasMFDerivAt[Prod.snd '' s] g p.2 dg
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')
⊢ HasFDerivWithinAt (writtenInExtChartAt I' J' p.2 g) dg
    (Prod.snd ''
      (↑(extChartAt I p.1).symm ⁻¹' Prod.fst '' s ∩ range ↑I) ×ˢ
        (↑(extChartAt I' p.2).symm ⁻¹' Prod.snd '' s ∩ range ↑I'))
    (↑(extChartAt (I.prod I') p) p).2