awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
⊢ DifferentiableWithinAt 𝕜 (F := E')
    (fun (x : E × E') ↦
      (↑I' : H' → E')
        ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
          ((↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H (p.1.proj (E := TangentSpace I)))).prod
                      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (p.2.proj (E := TangentSpace I'))))).symm :
                ModelProd H H' → M × M')
              ((↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H') x)).2))
    (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
      (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))

Tactic:
exact D _
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
φ' : (x : E) → E :=
  fun (x : E) ↦
    (↑I : H → E)
      ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H (p.1.proj (E := TangentSpace I)))) : H → M) ((↑I.symm : E → H) x)))
apply :
  ContDiffWithinAt 𝕜 1 φ' (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))))
⊢ DifferentiableWithinAt 𝕜 φ' (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))))

Tactic:
apply ContDiffWithinAt.differentiableWithinAt _ one_ne_zero

Premises used: one_ne_zero, ContDiffWithinAt.differentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
φ' : (x : E) → E :=
  fun (x : E) ↦
    (↑I : H → E)
      ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H (p.1.proj (E := TangentSpace I)))) : H → M) ((↑I.symm : E → H) x)))
hy :
  (↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))) ∈
    ((extChartAt I (p.1.proj (E := TangentSpace I))).symm ≫ extChartAt I (a.proj (E := TangentSpace I))).source
⊢ ContDiffWithinAt 𝕜 1 φ' (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))))

Tactic:
apply contDiffWithinAt_ext_coord_change

Premises used: contDiffWithinAt_ext_coord_change
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
φ' : (x : E) → E :=
  fun (x : E) ↦
    (↑I : H → E)
      ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H (p.1.proj (E := TangentSpace I)))) : H → M) ((↑I.symm : E → H) x)))
⊢ (↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))) ∈
    ((extChartAt I (p.1.proj (E := TangentSpace I))).symm ≫ extChartAt I (a.proj (E := TangentSpace I))).source

Tactic:
simp [hp.1]

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
φ' : (x : E) → E :=
  fun (x : E) ↦
    (↑I : H → E)
      ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H (p.1.proj (E := TangentSpace I)))) : H → M) ((↑I.symm : E → H) x)))
⊢ DifferentiableWithinAt 𝕜 φ' (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))))

Tactic:
have D0' : DifferentiableWithinAt 𝕜 φ' (Set.range I)
          (I ((chartAt H p.1.proj) p.1.proj)) := by
        apply ContDiffWithinAt.differentiableWithinAt _ one_ne_zero
        apply contDiffWithinAt_ext_coord_change
        simp [hp.1]
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
φ' : (x : E) → E :=
  fun (x : E) ↦
    (↑I : H → E)
      ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H (p.1.proj (E := TangentSpace I)))) : H → M) ((↑I.symm : E → H) x)))
D0' :
  DifferentiableWithinAt 𝕜 φ' (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))))
⊢ DifferentiableWithinAt 𝕜 φ' (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
        (↑I' : H' → E')
          ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I')))).1

Tactic:
D0'

Premises used: ModelWithCorners.toFun'
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
φ' : (x : E) → E :=
  fun (x : E) ↦
    (↑I : H → E)
      ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H (p.1.proj (E := TangentSpace I)))) : H → M) ((↑I.symm : E → H) x)))
D0' :
  DifferentiableWithinAt 𝕜 φ' (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))))
⊢ DifferentiableWithinAt 𝕜 φ' (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
        (↑I' : H' → E')
          ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I')))).1

Tactic:
exact D0'
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
φ' : (x : E) → E :=
  fun (x : E) ↦
    (↑I : H → E)
      ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H (p.1.proj (E := TangentSpace I)))) : H → M) ((↑I.symm : E → H) x)))
D0' :
  DifferentiableWithinAt 𝕜 φ' (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))))
⊢ MapsTo Prod.fst (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) (range (↑I : H → E))

Tactic:
simp [mapsTo_fst_prod]

Premises used: Set.mapsTo_fst_prod
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E') → E' :=
  fun (x : E') ↦
    (↑I' : H' → E')
      ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
        ((↑(OpenPartialHomeomorph.symm (chartAt H' (p.2.proj (E := TangentSpace I')))) : H' → M')
          ((↑I'.symm : E' → H') x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (w.proj (E := TangentSpace I))) : M → H) (w.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))
φ' : (x : E) → E :=
  fun (x : E) ↦
    (↑I : H → E)
      ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H (p.1.proj (E := TangentSpace I)))) : H → M) ((↑I.symm : E → H) x)))
D0' :
  DifferentiableWithinAt 𝕜 φ' (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))))
⊢ DifferentiableWithinAt 𝕜 (φ' ∘ Prod.fst) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
      (↑I' : H' → E') ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))

Tactic:
have D' : DifferentiableWithinAt 𝕜 (φ' ∘ Prod.fst) (Set.range (Prod.map I I'))
          (I ((chartAt H p.1.proj) p.1.proj), I' ((chartAt H' p.2.proj) p.2.proj)) :=
        DifferentiableWithinAt.comp (t := Set.range I) _ (by exact D0')
          differentiableWithinAt_fst (by simp [mapsTo_fst_prod])