awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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 : C^∞⟮I, M; I', M'⟯
⊢ Ne (α := ℕ∞ω) ∞ 0

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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 : C^∞⟮I, M; I', M'⟯
x : M
⊢ MDiffAt (⇑f : (a : M) → M') x

Tactic:
f.mdifferentiable x

Premises used: ContMDiffMap.mdifferentiable
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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'
simp :
  Eq (α := (a : TangentBundle (I.prod I') (M × M')) → TangentBundle I M × TangentBundle I' M')
    (⇑(equivTangentBundleProd I M I' M') :
      (a : TangentBundle (I.prod I') (M × M')) → TangentBundle I M × TangentBundle I' M')
    fun (p : TangentBundle (I.prod I') (M × M')) ↦
    (⟨p.proj (E := TangentSpace (I.prod I')).1, p.snd (E := TangentSpace (I.prod I')).1⟩,
      ⟨p.proj (E := TangentSpace (I.prod I')).2, p.snd (E := TangentSpace (I.prod I')).2⟩)
⊢ Eq (α := (a : TangentBundle (I.prod I') (M × M')) → TangentBundle I M × TangentBundle I' M')
    (⇑(equivTangentBundleProd I M I' M') :
      (a : TangentBundle (I.prod I') (M × M')) → TangentBundle I M × TangentBundle I' M')
    fun (p : TangentBundle (I.prod I') (M × M')) ↦
    (tangentMap (I.prod I') I Prod.fst p, tangentMap (I.prod I') I' Prod.snd p)

Tactic:
simp only [tangentMap_prodFst, tangentMap_prodSnd]

Premises used: tangentMap_prodSnd, tangentMap_prodFst
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
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'
⊢ Eq (α := (a : TangentBundle (I.prod I') (M × M')) → TangentBundle I M × TangentBundle I' M')
    (⇑(equivTangentBundleProd I M I' M') :
      (a : TangentBundle (I.prod I') (M × M')) → TangentBundle I M × TangentBundle I' M')
    fun (p : TangentBundle (I.prod I') (M × M')) ↦
    (⟨p.proj (E := TangentSpace (I.prod I')).1, p.snd (E := TangentSpace (I.prod I')).1⟩,
      ⟨p.proj (E := TangentSpace (I.prod I')).2, p.snd (E := TangentSpace (I.prod I')).2⟩)

Tactic:
rfl
-- 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'
rw :
  ContMDiff (I.prod I').tangent (I.tangent.prod I'.tangent) (M' := TangentBundle I M × TangentBundle I' M') n
    fun (p : TangentBundle (I.prod I') (M × M')) ↦
    (tangentMap (I.prod I') I Prod.fst p, tangentMap (I.prod I') I' Prod.snd p)
⊢ ContMDiff (I.prod I').tangent (M := TangentBundle (I.prod I') (M × M')) (I.tangent.prod I'.tangent) (M' :=
    TangentBundle I M × TangentBundle I' M') n
    (⇑(equivTangentBundleProd I M I' M') :
      (a : TangentBundle (I.prod I') (M × M')) → TangentBundle I M × TangentBundle I' M')

Tactic:
rw [equivTangentBundleProd_eq_tangentMap_prod_tangentMap]

Premises used: equivTangentBundleProd_eq_tangentMap_prod_tangentMap
-- 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'
⊢ ContMDiff (I.prod I').tangent (I.tangent.prod I'.tangent) (M' := TangentBundle I M × TangentBundle I' M') n
    fun (p : TangentBundle (I.prod I') (M × M')) ↦
    (tangentMap (I.prod I') I Prod.fst p, tangentMap (I.prod I') I' Prod.snd p)

Tactic:
(contMDiff_fst.contMDiff_tangentMap le_rfl).prodMk
    (contMDiff_snd.contMDiff_tangentMap le_rfl)

Premises used: le_rfl, ContMDiff.contMDiff_tangentMap, setOf, contMDiff_snd, TangentSpace, contMDiff_fst, ContMDiff.prodMk
-- 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'
⊢ ContMDiff (I.prod I').tangent (I.tangent.prod I'.tangent) (M' := TangentBundle I M × TangentBundle I' M') n
    fun (p : TangentBundle (I.prod I') (M × M')) ↦
    (tangentMap (I.prod I') I Prod.fst p, tangentMap (I.prod I') I' Prod.snd p)

Tactic:
exact (contMDiff_fst.contMDiff_tangentMap le_rfl).prodMk
    (contMDiff_snd.contMDiff_tangentMap le_rfl)

Premises used: le_rfl, ContMDiff.contMDiff_tangentMap, contMDiff_snd, contMDiff_fst, ContMDiff.prodMk
-- 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'
w : H
w' : H'
simp : UniqueDiffWithinAt 𝕜 (range (↑I : H → E) ×ˢ range (↑I' : H' → E')) ((↑I : H → E) w, (↑I' : H' → E') w')
⊢ UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')

Tactic:
simp only [range_prodMap]

Premises used: Set.range_prodMap
-- 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'
w : H
w' : H'
hs : UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑I : H → E) w)
ht : UniqueDiffWithinAt 𝕜 (range (↑I' : H' → E')) ((↑I' : H' → E') w')
⊢ UniqueDiffWithinAt 𝕜 (range (↑I : H → E) ×ˢ range (↑I' : H' → E')) ((↑I : H → E) w, (↑I' : H' → E') w')

Tactic:
apply UniqueDiffWithinAt.prod

Premises used: UniqueDiffWithinAt.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'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑I : H → E) w)

Tactic:
ModelWithCorners.uniqueDiffWithinAt_image I

Premises used: ModelWithCorners.uniqueDiffWithinAt_image
-- 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'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑I : H → E) w)

Tactic:
exact ModelWithCorners.uniqueDiffWithinAt_image I

Premises used: ModelWithCorners.uniqueDiffWithinAt_image
-- 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'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range (↑I' : H' → E')) ((↑I' : H' → E') w')

Tactic:
ModelWithCorners.uniqueDiffWithinAt_image I'

Premises used: ModelWithCorners.uniqueDiffWithinAt_image
-- 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'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range (↑I' : H' → E')) ((↑I' : H' → E') w')

Tactic:
exact ModelWithCorners.uniqueDiffWithinAt_image I'

Premises used: ModelWithCorners.uniqueDiffWithinAt_image
-- 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'
⊢ ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')

Tactic:
have U w w' : UniqueDiffWithinAt 𝕜 (Set.range (Prod.map I I')) (I w, I' w') := by
    simp only [range_prodMap]
    apply UniqueDiffWithinAt.prod
    · exact ModelWithCorners.uniqueDiffWithinAt_image I
    · exact ModelWithCorners.uniqueDiffWithinAt_image I'
-- 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')
rw :
  ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I') (M' := M × M') n
      (fun (x : TangentBundle I M × TangentBundle I' M') ↦
        TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I'))
          ((Equiv.symm (equivTangentBundleProd I M I' M') :
              (a : TangentBundle I M × TangentBundle I' M') → TangentBundle (I.prod I') (M × M'))
            x))
      (a, b) ∧
    ContMDiffAt (I.tangent.prod I'.tangent) (E' := E × E') 𝓘(𝕜, E × E') (M' := E × E') n
      (fun (x : TangentBundle I M × TangentBundle I' M') ↦
        ((↑(trivializationAt (E × E') (TangentSpace (I.prod I'))
                  (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I'))
                    ((Equiv.symm (equivTangentBundleProd I M I' M') :
                        (a : TangentBundle I M × TangentBundle I' M') → TangentBundle (I.prod I') (M × M'))
                      (a, b)))) :
              TotalSpace (E × E') (TangentSpace (I.prod I')) → (M × M') × E × E')
            ((Equiv.symm (equivTangentBundleProd I M I' M') :
                (a : TangentBundle I M × TangentBundle I' M') → TangentBundle (I.prod I') (M × M'))
              x)).2)
      (a, b)
⊢ ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I').tangent (M' := TangentBundle (I.prod I') (M × M')) n
    (⇑(Equiv.symm (equivTangentBundleProd I M I' M')) :
      (a : TangentBundle I M × TangentBundle I' M') → TangentBundle (I.prod I') (M × M'))
    (a, b)

Tactic:
rw [contMDiffAt_totalSpace]

Premises used: Bundle.contMDiffAt_totalSpace
-- 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')
⊢ ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I') (M' := M × M') n
      (fun (x : TangentBundle I M × TangentBundle I' M') ↦
        (x.1.proj (E := TangentSpace I), x.2.proj (E := TangentSpace I')))
      (a, b) ∧
    ContMDiffAt (I.tangent.prod I'.tangent) (E' := E × E') 𝓘(𝕜, E × E') (M' := E × E') n
      (fun (x : TangentBundle I M × TangentBundle I' M') ↦
        (fderivWithin 𝕜
              (((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) ∘ fun (p : M × M') ↦
                  ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H) p.1,
                    (↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H') p.2)) ∘
                (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H (x.1.proj (E := TangentSpace I)))).prod
                          (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (x.2.proj (E := TangentSpace I'))))).symm :
                    ModelProd H H' → M × M') ∘
                  (↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H'))
              (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
              ((↑I : H → E) ((↑(chartAt H (x.1.proj (E := TangentSpace I))) : M → H) (x.1.proj (E := TangentSpace I))),
                (↑I' : H' → E')
                  ((↑(chartAt H' (x.2.proj (E := TangentSpace I'))) : M' → H') (x.2.proj (E := TangentSpace I')))) :
            (a : E × E') → E × E')
          (x.1.snd (E := TangentSpace I), x.2.snd (E := TangentSpace I')))
      (a, b)

Tactic:
⟨?_, (contMDiffAt_prod_module_iff _).2 ⟨?_, ?_⟩⟩

Premises used: Iff.mpr, And.intro, contMDiffAt_prod_module_iff
-- 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')
⊢ ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I') (M' := M × M') n
    (fun (x : TangentBundle I M × TangentBundle I' M') ↦
      (x.1.proj (E := TangentSpace I), x.2.proj (E := TangentSpace I')))
    (a, b)

Tactic:
(contMDiffAt_proj (TangentSpace I)).prodMap (contMDiffAt_proj (TangentSpace I'))

Premises used: ContMDiffAt.prodMap, Prod.map, TangentSpace, Bundle.contMDiffAt_proj
-- 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')
⊢ ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I') (M' := M × M') n
    (fun (x : TangentBundle I M × TangentBundle I' M') ↦
      (x.1.proj (E := TangentSpace I), x.2.proj (E := TangentSpace I')))
    (a, b)

Tactic:
exact (contMDiffAt_proj (TangentSpace I)).prodMap (contMDiffAt_proj (TangentSpace I'))

Premises used: ContMDiffAt.prodMap, TangentSpace, Bundle.contMDiffAt_proj
-- 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')
⊢ ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)

Tactic:
have smooth_pM : CMDiffAt n (Prod.fst : TangentBundle I M × TangentBundle I' M' → _) (a, b) :=
      contMDiffAt_fst
-- 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.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p ∈
    PartialEquiv.source (β := ModelProd (ModelProd H E) (ModelProd H' E'))
      (OpenPartialHomeomorph.toPartialEquiv (chartAt (ModelProd (ModelProd H E) (ModelProd H' E')) (a, b)))
⊢ 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

Tactic:
simp only [prodChartedSpace_chartAt, OpenPartialHomeomorph.prod_toPartialEquiv,
      PartialEquiv.prod_source, Set.mem_prod, TangentBundle.mem_chart_source_iff] at hp

Premises used: PartialEquiv.prod_source, prodChartedSpace_chartAt, OpenPartialHomeomorph.prod_toPartialEquiv, Set.mem_prod, TangentBundle.mem_chart_source_iff