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'
x : M
f : M → M'
g : N → N'
y : N
hf : MDiffAt[univ] f x
hg : MDiffAt[univ] g y
⊢ MDiffAt[SProd.sprod (α := Set M) (β := Set N) univ univ] (Prod.map f g) (x, y)

Tactic:
hf.prodMap hg

Premises used: MDifferentiableWithinAt.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'
x : M
f : M → M'
g : N → N'
y : N
hf : MDiffAt[univ] f x
hg : MDiffAt[univ] g y
h : univ = SProd.sprod (α := Set M) (β := Set N) univ univ
⊢ MDiffAt[univ] (Prod.map f g) (x, y)

Tactic:
convert! hf.prodMap hg

Premises used: MDifferentiableWithinAt.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'
x : M
f : M → M'
g : N → N'
y : N
hf : MDiffAt[univ] f x
hg : MDiffAt[univ] g y
⊢ univ = SProd.sprod (α := Set M) (β := Set N) univ univ

Tactic:
univ_prod_univ.symm

Premises used: Set.univ_prod_univ, Eq.symm
-- 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'
x : M
f : M → M'
g : N → N'
y : N
hf : MDiffAt[univ] f x
hg : MDiffAt[univ] g y
⊢ univ = SProd.sprod (α := Set M) (β := Set N) univ univ

Tactic:
exact univ_prod_univ.symm

Premises used: Set.univ_prod_univ, Eq.symm
-- 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'
f : M → M'
g : N → N'
p : M × N
hf : MDiffAt f p.1
hg : MDiffAt g p.2
⊢ MDiffAt (Prod.map f g) p

Tactic:
hf.prodMap hg

Premises used: MDifferentiableAt.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
f : M → M'
g : N → N'
r : Set N
hf : MDiff[s] f
hg : MDiff[r] g
⊢ MDiff[s ×ˢ r] (Prod.map f g)

Tactic:
(hf.comp mdifferentiableOn_fst (prod_subset_preimage_fst _ _)).prodMk <|
    hg.comp mdifferentiableOn_snd (prod_subset_preimage_snd _ _)

Premises used: mdifferentiableOn_snd, MDifferentiableOn.prodMk, mdifferentiableOn_fst, Set.prod_subset_preimage_fst, MDifferentiableOn.comp, Prod.map, Set.prod_subset_preimage_snd
-- 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'
f : M → M'
g : N → N'
hf : MDiff f
hg : MDiff g
⊢ MDiff (Prod.map f g)

Tactic:
fun p ↦
  (hf p.1).prodMap' (hg p.2)

Premises used: MDifferentiableAt.prodMap', Prod.fst, MDifferentiable, Prod.snd
-- 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
⊢ s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' 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
refine :
  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)
⊢ HasMFDerivWithinAt (I.prod I') (J.prod J') (Prod.map f g) s p (df.prodMap dg)

Tactic:
refine ⟨hf.1.prodMap hg.1 |>.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 × 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
simp :
  (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H p.1)).prod
                  (OpenPartialHomeomorph.toPartialEquiv (chartAt H' p.2))).symm :
            ModelProd H H' → M × M') ∘
          (↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H') ⁻¹'
        s ∩
      range (Prod.map (↑I : H → E) (↑I' : H' → E')) ⊆
    ((↑(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'))
⊢ (↑(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:
simp only [mfld_simps]
-- 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
rw :
  (↑((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 ∩
      range (↑I : H → E) ×ˢ range (↑I' : H' → E') ⊆
    ((↑(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'))
⊢ (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H p.1)).prod
                  (OpenPartialHomeomorph.toPartialEquiv (chartAt H' p.2))).symm :
            ModelProd H H' → M × M') ∘
          (↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H') ⁻¹'
        s ∩
      range (Prod.map (↑I : H → E) (↑I' : H' → E')) ⊆
    ((↑(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:
rw [range_prodMap, I.toPartialEquiv.prod_symm, (chartAt H p.1).toPartialEquiv.prod_symm]

Premises used: chartAt, ModelWithCorners.toPartialEquiv, Prod.fst, Set.range_prodMap, PartialEquiv.prod_symm, OpenPartialHomeomorph.toPartialEquiv
-- 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'
this :
  ∀
    (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'))
⊢ 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 ∩
        range (↑I : H → E) ×ˢ 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:
⟨hp₀, ⟨hp₁₁, hp₁₂⟩⟩
-- 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),
    ∃ (x : M'), ((↑(OpenPartialHomeomorph.symm (chartAt H p.1)) : H → M) ((↑I.symm : E → H) p₀.1), x) ∈ s
⊢ p₀.1 ∈ (↑(OpenPartialHomeomorph.symm (chartAt H p.1)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' Prod.fst '' 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
⊢ ∃ (x : M'), ((↑(OpenPartialHomeomorph.symm (chartAt H p.1)) : H → M) ((↑I.symm : E → H) p₀.1), x) ∈ s

Tactic:
grind