awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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'
⊢ 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'))
have 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'))
Tactic: ⟨hp₀, ⟨hp₁₁, hp₁₂⟩⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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 ∈ (↑(OpenPartialHomeomorph.symm (chartAt H p.1)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' Prod.fst '' s
have 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
Tactic: simp_all
Cleared hypotheses: hp₀, hp₁₁, hp₁₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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 ∈ (↑(OpenPartialHomeomorph.symm (chartAt H' p.2)) : H' → M') ∘ (↑I'.symm : E' → H') ⁻¹' Prod.snd '' s
have 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
Tactic: simp_all
Cleared hypotheses: hp₀, hp₁₁, hp₁₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (hypothesis)
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
⊢ 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)
have 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'))
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⟩⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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.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)
have 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)
Tactic: rw [writtenInExtChartAt_prod]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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 (𝕜 := 𝕜) (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)
have 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)
Tactic: apply HasFDerivWithinAt.mono ?_ better
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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 (𝕜 := 𝕜) (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)
have 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
Tactic: apply HasFDerivWithinAt.prodMap
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
⊢ 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)
have 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
Tactic: apply HasFDerivWithinAt.prodMap
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
⊢ HasMFDerivAt (I.prod I') (J.prod J') (Prod.map f g) p (ContinuousLinearMap.prodMap (mfderiv% f p.1) (mfderiv% g p.2))
have 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))
Tactic: simp_rw [← hasMFDerivWithinAt_univ, ← mfderivWithin_univ, ← univ_prod_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
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
    (ContinuousLinearMap.prodMap (mfderivWithin I J f univ p.1) (mfderivWithin I' J' g univ p.2))
have h : mfderivWithin I J f univ p.1 = df
Tactic: convert! hf.hasMFDerivWithinAt.prodMap hg.hasMFDerivWithinAt