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
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
rw :
  ⟨p.proj (E := TangentSpace I),
      (ContinuousLinearMap.id 𝕜 (TangentSpace I (p.proj (E := TangentSpace I))) :
          (a : TangentSpace I p.proj) → TangentSpace I p.proj)
        (p.snd (E := TangentSpace I))⟩ =
    p
rw₁ : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
⊢ ⟨p.proj (E := TangentSpace I),
      (mfderivWithin I I id s (p.proj (E := TangentSpace I)) : (a : TangentSpace I p.proj) → TangentSpace I p.proj)
        (p.snd (E := TangentSpace I))⟩ =
    p

Tactic:
rw [mfderivWithin_id]

Premises used: mfderivWithin_id
-- 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
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
rcases :
  ∀ (proj : M) (snd : TangentSpace I proj)
    (hs : UniqueMDiffWithinAt I s (TotalSpace.proj (F := E) (E := TangentSpace I) ⟨proj, snd⟩)),
    Eq (α := TangentBundle I M)
      ⟨TotalSpace.proj (F := E) (E := TangentSpace I) ⟨proj, snd⟩,
        (ContinuousLinearMap.id 𝕜 (TangentSpace I (TotalSpace.proj (F := E) (E := TangentSpace I) ⟨proj, snd⟩)) :
            (a : TangentSpace I ⟨proj, snd⟩.proj) → TangentSpace I ⟨proj, snd⟩.proj)
          (TotalSpace.snd (E := TangentSpace I) ⟨proj, snd⟩)⟩
      ⟨proj, snd⟩
⊢ ⟨p.proj (E := TangentSpace I),
      (ContinuousLinearMap.id 𝕜 (TangentSpace I (p.proj (E := TangentSpace I))) :
          (a : TangentSpace I p.proj) → TangentSpace I p.proj)
        (p.snd (E := TangentSpace I))⟩ =
    p

Tactic:
rcases p with ⟨⟩
-- 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
s : Set M
proj : M
snd : TangentSpace I proj
hs : UniqueMDiffWithinAt I s (TotalSpace.proj (F := E) (E := TangentSpace I) ⟨proj, snd⟩)
⊢ Eq (α := TangentBundle I M)
    ⟨TotalSpace.proj (F := E) (E := TangentSpace I) ⟨proj, snd⟩,
      (ContinuousLinearMap.id 𝕜 (TangentSpace I (TotalSpace.proj (F := E) (E := TangentSpace I) ⟨proj, snd⟩)) :
          (a : TangentSpace I ⟨proj, snd⟩.proj) → TangentSpace I ⟨proj, snd⟩.proj)
        (TotalSpace.snd (E := TangentSpace I) ⟨proj, snd⟩)⟩
    ⟨proj, snd⟩

Tactic:
rfl
-- 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
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
⊢ UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))

Tactic:
hs
-- 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
s : Set M
p : TangentBundle I M
hs : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
⊢ UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))

Tactic:
exact hs
-- 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'
c : M'
x : M
⊢ ContinuousAt.{u_4, u_7} (Y := M') (fun (x : M) ↦ c) x

Tactic:
fun_prop
-- 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'
c : M'
x : M
⊢ HasFDerivWithinAt.{u_1, u_2, u_5} (𝕜 := 𝕜)
    (writtenInExtChartAt.{u_1, u_2, u_4, u_3, u_5, u_7, u_6} (M' := M') I I' x fun (x : M) ↦ c) 0 (range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)

Tactic:
simp [Function.comp_def, hasFDerivWithinAt_const]

Premises used: hasFDerivWithinAt_const, Function.comp_def
-- 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'
c : M'
s : Set M
x : M
⊢ HasMFDerivWithinAt.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} I I' (M' := M') (fun (x : M) ↦ c) s x 0

Tactic:
(hasMFDerivAt_const c x).hasMFDerivWithinAt

Premises used: hasMFDerivAt_const, HasMFDerivAt.hasMFDerivWithinAt
-- 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'
x : M
c : M'
⊢ (MDiffAt fun (x : M) ↦ c) x

Tactic:
(hasMFDerivAt_const c x).mdifferentiableAt

Premises used: hasMFDerivAt_const, HasMFDerivAt.mdifferentiableAt
-- 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'
s : Set M
x : M
c : M'
⊢ (MDiffAt[s] fun (x : M) ↦ c) x

Tactic:
mdifferentiableAt_const.mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, mdifferentiableAt_const
-- 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'
c : M'
⊢ MDiff fun (x : M) ↦ c

Tactic:
fun _ ↦ mdifferentiableAt_const

Premises used: mdifferentiableAt_const, MDifferentiable
-- 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'
s : Set M
c : M'
⊢ MDiff[s] fun (x : M) ↦ c

Tactic:
mdifferentiable_const.mdifferentiableOn

Premises used: mdifferentiable_const, MDifferentiable.mdifferentiableOn
-- 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'
x : M
c : M'
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' c))
    ((mfderiv% fun (x : M) ↦ c) x :
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' c))
    (0 : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' c))

Tactic:
(hasMFDerivAt_const c x).mfderiv

Premises used: HasMFDerivAt.mfderiv, hasMFDerivAt_const
-- 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'
s : Set M
x : M
c : M'
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' c))
    (mfderivWithin.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} I I' (M' := M') (fun (x : M) ↦ c) s x :
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' c))
    (0 : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' c))

Tactic:
(hasMFDerivWithinAt_const _ _ _).mfderivWithin_eq_zero

Premises used: hasMFDerivWithinAt_const, HasMFDerivWithinAt.mfderivWithin_eq_zero
-- 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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
s : Set M
x : M
f : M → M'
g : M → M''
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
⊢ (MDiffAt[s] fun (x : M) ↦ (f x, g x)) x

Tactic:
⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩

Premises used: ChartedSpace.LiftPropWithinAt.prop, ChartedSpace.LiftPropWithinAt.continuousWithinAt, DifferentiableWithinAt.prodMk, ContinuousWithinAt.prodMk, MDifferentiableWithinAt, ChartedSpace.LiftPropWithinAt.mk
-- 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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
s : Set M
x : M
f : M → M'
g : M → M''
df : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
hf : HasMFDerivWithinAt I I' f s x df
dg : ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' (g x))
hg : HasMFDerivWithinAt I I'' g s x dg
⊢ HasMFDerivWithinAt I (I'.prod I'') (M' := M' × M'') (fun (y : M) ↦ (f y, g y)) s x (df.prod dg)

Tactic:
⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩

Premises used: HasFDerivWithinAt.prodMk, And.right, And.left, And.intro, ContinuousWithinAt.prodMk, HasMFDerivWithinAt
-- 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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
s : Set M
x : M
f : M → M'
g : M → M''
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
hs : UniqueMDiffWithinAt I s x
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
    (mfderivWithin I (I'.prod I'') (M' := M' × M'') (fun (x : M) ↦ (f x, g x)) s x :
      TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
    (ContinuousLinearMap.prod (mfderivWithin I I' f s x) (mfderivWithin I I'' g s x) :
      TangentSpace I x →L[𝕜] Prod.{u_5, u_8} (TangentSpace I' (f x)) (TangentSpace I'' (g x)))

Tactic:
(hf.hasMFDerivWithinAt.prodMk hg.hasMFDerivWithinAt).mfderivWithin hs

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.prodMk, HasMFDerivWithinAt.mfderivWithin
-- 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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
x : M
f : M → M'
g : M → M''
hf : MDiffAt f x
hg : MDiffAt g x
simp_rw :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
    (mfderivWithin I (I'.prod I'') (M' := M' × M'') (fun (x : M) ↦ (f x, g x)) univ x :
      TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
    (ContinuousLinearMap.prod (mfderivWithin I I' f univ x) (mfderivWithin I I'' g univ x) :
      TangentSpace I x →L[𝕜] Prod.{u_5, u_8} (TangentSpace I' (f x)) (TangentSpace I'' (g x)))
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
    ((mfderiv% fun (x : M) ↦ (f x, g x)) x : TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
    (ContinuousLinearMap.prod (mfderiv% f x) (mfderiv% g x) :
      TangentSpace I x →L[𝕜] Prod.{u_5, u_8} (TangentSpace I' (f x)) (TangentSpace I'' (g x)))

Tactic:
simp_rw [← mfderivWithin_univ]

Premises used: mfderivWithin_univ
-- 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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
x : M
f : M → M'
g : M → M''
hf : MDiffAt f x
hg : MDiffAt g x
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
    (mfderivWithin I (I'.prod I'') (M' := M' × M'') (fun (x : M) ↦ (f x, g x)) univ x :
      TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
    (ContinuousLinearMap.prod (mfderivWithin I I' f univ x) (mfderivWithin I I'' g univ x) :
      TangentSpace I x →L[𝕜] Prod.{u_5, u_8} (TangentSpace I' (f x)) (TangentSpace I'' (g x)))

Tactic:
mfderivWithin_prodMk hf.mdifferentiableWithinAt hg.mdifferentiableWithinAt
    (uniqueMDiffWithinAt_univ I)

Premises used: MDifferentiableAt.mdifferentiableWithinAt, uniqueMDiffWithinAt_univ, mfderivWithin_prodMk
-- 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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
x : M
f : M → M'
g : M → M''
hf : MDiffAt f x
hg : MDiffAt g x
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
    (mfderivWithin I (I'.prod I'') (M' := M' × M'') (fun (x : M) ↦ (f x, g x)) univ x :
      TangentSpace I x →L[𝕜] TangentSpace (I'.prod I'') (f x, g x))
    (ContinuousLinearMap.prod (mfderivWithin I I' f univ x) (mfderivWithin I I'' g univ x) :
      TangentSpace I x →L[𝕜] Prod.{u_5, u_8} (TangentSpace I' (f x)) (TangentSpace I'' (g x)))

Tactic:
exact mfderivWithin_prodMk hf.mdifferentiableWithinAt hg.mdifferentiableWithinAt
    (uniqueMDiffWithinAt_univ I)

Premises used: MDifferentiableAt.mdifferentiableWithinAt, uniqueMDiffWithinAt_univ, mfderivWithin_prodMk
-- 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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
x : M
f : M → M'
g : M → M''
hf : MDiffAt f x
hg : MDiffAt g x
⊢ (MDiffAt fun (x : M) ↦ (f x, g x)) x

Tactic:
⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩

Premises used: ChartedSpace.LiftPropWithinAt.prop, ChartedSpace.LiftPropWithinAt.continuousWithinAt, DifferentiableWithinAt.prodMk, MDifferentiableAt, ContinuousWithinAt.prodMk, ChartedSpace.LiftPropAt, ChartedSpace.LiftPropWithinAt.mk
-- 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'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
x : M
f : M → M'
g : M → M''
df : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
hf : HasMFDerivAt I I' f x df
dg : ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' (g x))
hg : HasMFDerivAt I I'' g x dg
⊢ HasMFDerivAt I (I'.prod I'') (M' := M' × M'') (fun (y : M) ↦ (f y, g y)) x (df.prod dg)

Tactic:
⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩

Premises used: HasMFDerivAt, HasFDerivWithinAt.prodMk, And.right, And.left, And.intro, ContinuousAt.prodMk
-- 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'
E'' : Type u_8
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
s : Set M
x : M
f : M → E'
g : M → E''
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
⊢ (MDiffAt[s] fun (x : M) ↦ (f x, g x)) x

Tactic:
⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩

Premises used: ChartedSpace.LiftPropWithinAt.prop, ChartedSpace.LiftPropWithinAt.continuousWithinAt, DifferentiableWithinAt.prodMk, ContinuousWithinAt.prodMk, MDifferentiableWithinAt, ChartedSpace.LiftPropWithinAt.mk
-- 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'
E'' : Type u_8
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
x : M
f : M → E'
g : M → E''
hf : MDiffAt f x
hg : MDiffAt g x
⊢ (MDiffAt fun (x : M) ↦ (f x, g x)) x

Tactic:
⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩

Premises used: ChartedSpace.LiftPropWithinAt.prop, ChartedSpace.LiftPropWithinAt.continuousWithinAt, DifferentiableWithinAt.prodMk, MDifferentiableAt, ContinuousWithinAt.prodMk, ChartedSpace.LiftPropAt, ChartedSpace.LiftPropWithinAt.mk