awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set M
p : M × M'
t : Set M'
f : M → N
g : M' → N'
hf : MDiffAt[s] f p.1
hg : MDiffAt[t] g p.2
hs : UniqueMDiffWithinAt I s p.1
ht : UniqueMDiffWithinAt I' t p.2
hf' : HasMFDerivWithinAt I J f (Prod.fst '' s ×ˢ t) p.1 (mfderivWithin I J f s p.1)
⊢ HasMFDerivWithinAt I' J' g (Prod.snd '' s ×ˢ t) p.2 (mfderivWithin I' J' g t p.2)

Tactic:
have hg' : HasMFDerivAt[Prod.snd '' s ×ˢ t] g p.2 (mfderiv[t] g p.2) :=
    hg.hasMFDerivWithinAt.mono (by grind)
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set M
p : M × M'
t : Set M'
f : M → N
g : M' → N'
hf : MDiffAt[s] f p.1
hg : MDiffAt[t] g p.2
hs : UniqueMDiffWithinAt I s p.1
ht : UniqueMDiffWithinAt I' t p.2
hf' : HasMFDerivWithinAt I J f (Prod.fst '' s ×ˢ t) p.1 (mfderivWithin I J f s p.1)
hg' : HasMFDerivWithinAt I' J' g (Prod.snd '' s ×ˢ t) p.2 (mfderivWithin I' J' g t p.2)
⊢ Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (J.prod J') (Prod.map f g p))
    (mfderivWithin (I.prod I') (J.prod J') (Prod.map f g) (s ×ˢ t) p)
    (ContinuousLinearMap.prodMap (mfderivWithin I J f s p.1) (mfderivWithin I' J' g t p.2))

Tactic:
(hf'.prodMap hg').mfderivWithin (hs.prod ht)

Premises used: HasMFDerivWithinAt.prodMap, HasMFDerivWithinAt.mfderivWithin, instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, UniqueMDiffWithinAt.prod, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set M
p : M × M'
t : Set M'
f : M → N
g : M' → N'
hf : MDiffAt[s] f p.1
hg : MDiffAt[t] g p.2
hs : UniqueMDiffWithinAt I s p.1
ht : UniqueMDiffWithinAt I' t p.2
hf' : HasMFDerivWithinAt I J f (Prod.fst '' s ×ˢ t) p.1 (mfderivWithin I J f s p.1)
hg' : HasMFDerivWithinAt I' J' g (Prod.snd '' s ×ˢ t) p.2 (mfderivWithin I' J' g t p.2)
⊢ Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (J.prod J') (Prod.map f g p))
    (mfderivWithin (I.prod I') (J.prod J') (Prod.map f g) (s ×ˢ t) p)
    (ContinuousLinearMap.prodMap (mfderivWithin I J f s p.1) (mfderivWithin I' J' g t p.2))

Tactic:
exact (hf'.prodMap hg').mfderivWithin (hs.prod ht)

Premises used: HasMFDerivWithinAt.prodMap, HasMFDerivWithinAt.mfderivWithin, UniqueMDiffWithinAt.prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
hf : MDiffAt f p.1
hg : MDiffAt g p.2
simp_rw :
  Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (J.prod J') (Prod.map f g p))
    (mfderivWithin (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))
⊢ Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (J.prod J') (Prod.map f g p)) (mfderiv% (Prod.map f g) p)
    (ContinuousLinearMap.prodMap (mfderiv% f p.1) (mfderiv% g p.2))

Tactic:
simp_rw [← mfderivWithin_univ, ← univ_prod_univ]

Premises used: mfderivWithin_univ, Set.univ_prod_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'
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'
hf : MDiffAt f p.1
hg : MDiffAt g p.2
⊢ Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (J.prod J') (Prod.map f g p))
    (mfderivWithin (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:
mfderivWithin_prodMap hf.mdifferentiableWithinAt hg.mdifferentiableWithinAt
    (uniqueMDiffWithinAt_univ I) (uniqueMDiffWithinAt_univ I')

Premises used: MDifferentiableAt.mdifferentiableWithinAt, uniqueMDiffWithinAt_univ, mfderivWithin_prodMap
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
hf : MDiffAt f p.1
hg : MDiffAt g p.2
⊢ Eq (α := TangentSpace (I.prod I') p →L[𝕜] TangentSpace (J.prod J') (Prod.map f g p))
    (mfderivWithin (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:
exact mfderivWithin_prodMap hf.mdifferentiableWithinAt hg.mdifferentiableWithinAt
    (uniqueMDiffWithinAt_univ I) (uniqueMDiffWithinAt_univ I')

Premises used: MDifferentiableAt.mdifferentiableWithinAt, uniqueMDiffWithinAt_univ, mfderivWithin_prodMap
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
p : TangentBundle (I.prod I') (M × M')
simp :
  ((ContinuousLinearMap.snd 𝕜 (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
            (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
          Prod.{u_2, u_5} (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
              (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) →L[𝕜]
            TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
        (a : TangentSpace (I.prod I') p.proj) → TangentSpace I' p.proj.2)
      (p.snd (E := TangentSpace (I.prod I'))) =
    p.snd (E := TangentSpace (I.prod I')).2
⊢ Eq (α := TangentBundle I' M') (tangentMap (I.prod I') I' Prod.snd p)
    ⟨p.proj (E := TangentSpace (I.prod I')).2, p.snd (E := TangentSpace (I.prod I')).2⟩

Tactic:
simp [tangentMap]

Premises used: tangentMap
-- 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'
p : TangentBundle (I.prod I') (M × M')
⊢ ((ContinuousLinearMap.snd 𝕜 (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
            (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
          Prod.{u_2, u_5} (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
              (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) →L[𝕜]
            TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
        (a : TangentSpace (I.prod I') p.proj) → TangentSpace I' p.proj.2)
      (p.snd (E := TangentSpace (I.prod I'))) =
    p.snd (E := TangentSpace (I.prod I')).2

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
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 × M')
p : TangentBundle (I.prod I') (M × M')
hs : UniqueMDiffWithinAt (I.prod I') s (p.proj (E := TangentSpace (I.prod I')))
rw :
  Eq (α := TangentBundle I' M')
    ⟨p.proj (E := TangentSpace (I.prod I')).2,
      ((ContinuousLinearMap.snd 𝕜 (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
              (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
            Prod.{u_2, u_5} (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
                (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) →L[𝕜]
              TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
          (a : TangentSpace (I.prod I') p.proj) → TangentSpace I' p.proj.2)
        (p.snd (E := TangentSpace (I.prod I')))⟩
    ⟨p.proj (E := TangentSpace (I.prod I')).2, p.snd (E := TangentSpace (I.prod I')).2⟩
⊢ Eq (α := TangentBundle I' M')
    ⟨p.proj (E := TangentSpace (I.prod I')).2,
      (mfderivWithin (I.prod I') I' Prod.snd s (p.proj (E := TangentSpace (I.prod I'))) :
          (a : TangentSpace (I.prod I') p.proj) → TangentSpace I' p.proj.2)
        (p.snd (E := TangentSpace (I.prod I')))⟩
    ⟨p.proj (E := TangentSpace (I.prod I')).2, p.snd (E := TangentSpace (I.prod I')).2⟩

Tactic:
rw [mfderivWithin_snd hs]

Premises used: mfderivWithin_snd
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set (M × M')
p : TangentBundle (I.prod I') (M × M')
hs : UniqueMDiffWithinAt (I.prod I') s (p.proj (E := TangentSpace (I.prod I')))
rcases :
  ∀ (proj : M × M') (snd : TangentSpace (I.prod I') proj)
    (hs :
      UniqueMDiffWithinAt (I.prod I') s (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩)),
    Eq (α := TangentBundle I' M')
      ⟨(TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2,
        ((ContinuousLinearMap.snd 𝕜
                (TangentSpace I (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1)
                (TangentSpace I' (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2) :
              Prod.{u_2, u_5}
                  (TangentSpace I (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1)
                  (TangentSpace I' (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2) →L[𝕜]
                TangentSpace I' (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2) :
            (a : TangentSpace (I.prod I') ⟨proj, snd⟩.proj) → TangentSpace I' ⟨proj, snd⟩.proj.2)
          (TotalSpace.snd (E := TangentSpace (I.prod I')) ⟨proj, snd⟩)⟩
      ⟨(TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2,
        (TotalSpace.snd (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2⟩
⊢ Eq (α := TangentBundle I' M')
    ⟨p.proj (E := TangentSpace (I.prod I')).2,
      ((ContinuousLinearMap.snd 𝕜 (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
              (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
            Prod.{u_2, u_5} (TangentSpace I p.proj (E := TangentSpace (I.prod I')).1)
                (TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) →L[𝕜]
              TangentSpace I' p.proj (E := TangentSpace (I.prod I')).2) :
          (a : TangentSpace (I.prod I') p.proj) → TangentSpace I' p.proj.2)
        (p.snd (E := TangentSpace (I.prod I')))⟩
    ⟨p.proj (E := TangentSpace (I.prod I')).2, p.snd (E := TangentSpace (I.prod I')).2⟩

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
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 × M')
proj : M × M'
snd : TangentSpace (I.prod I') proj
hs : UniqueMDiffWithinAt (I.prod I') s (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩)
⊢ Eq (α := TangentBundle I' M')
    ⟨(TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2,
      ((ContinuousLinearMap.snd 𝕜
              (TangentSpace I (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1)
              (TangentSpace I' (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2) :
            Prod.{u_2, u_5}
                (TangentSpace I (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1)
                (TangentSpace I' (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2) →L[𝕜]
              TangentSpace I' (TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2) :
          (a : TangentSpace (I.prod I') ⟨proj, snd⟩.proj) → TangentSpace I' ⟨proj, snd⟩.proj.2)
        (TotalSpace.snd (E := TangentSpace (I.prod I')) ⟨proj, snd⟩)⟩
    ⟨(TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2,
      (TotalSpace.snd (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).2⟩

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
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
y₀ : M'
⊢ Eq (α := TangentSpace I x₀ →L[𝕜] TangentSpace (I.prod I') (x₀, y₀))
    ((mfderiv% fun (x : M) ↦ (x, y₀)) x₀ : TangentSpace I x₀ →L[𝕜] TangentSpace (I.prod I') (x₀, y₀))
    (ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) :
      TangentSpace I x₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' y₀))

Tactic:
(mdifferentiableAt_id.mfderiv_prod mdifferentiableAt_const).trans ?_

Premises used: MDifferentiableAt.mfderiv_prod, mdifferentiableAt_const, TangentSpace, mdifferentiableAt_id, Eq.trans
-- 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
y₀ : M'
refine :
  Eq (α := TangentSpace I x₀ →L[𝕜] TangentSpace (I.prod I') (id x₀, y₀))
    (ContinuousLinearMap.prod (mfderiv% id x₀) ((mfderiv% fun (x : M) ↦ y₀) x₀) :
      TangentSpace I x₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I (id x₀)) (TangentSpace I' y₀))
    (ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) :
      TangentSpace I x₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' y₀))
⊢ Eq (α := TangentSpace I x₀ →L[𝕜] TangentSpace (I.prod I') (x₀, y₀))
    ((mfderiv% fun (x : M) ↦ (x, y₀)) x₀ : TangentSpace I x₀ →L[𝕜] TangentSpace (I.prod I') (x₀, y₀))
    (ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) :
      TangentSpace I x₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' y₀))

Tactic:
refine (mdifferentiableAt_id.mfderiv_prod mdifferentiableAt_const).trans ?_

Premises used: MDifferentiableAt.mfderiv_prod, mdifferentiableAt_const, mdifferentiableAt_id, Eq.trans
-- 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
y₀ : M'
rw :
  Eq (α := TangentSpace I x₀ →L[𝕜] TangentSpace (I.prod I') (id x₀, y₀))
    (ContinuousLinearMap.prod (ContinuousLinearMap.id 𝕜 (TangentSpace I x₀)) ((mfderiv% fun (x : M) ↦ y₀) x₀) :
      TangentSpace I x₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I (id x₀)) (TangentSpace I' y₀))
    (ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) :
      TangentSpace I x₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' y₀))
rw₁ :
  Eq (α := TangentSpace I x₀ →L[𝕜] TangentSpace (I.prod I') (id x₀, y₀))
    (ContinuousLinearMap.prod (ContinuousLinearMap.id 𝕜 (TangentSpace I x₀)) 0 :
      TangentSpace I x₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I (id x₀)) (TangentSpace I' y₀))
    (ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀))
rw₂ rw₃ :
  Eq (α := TangentSpace I x₀ →L[𝕜] TangentSpace (I.prod I') (id x₀, y₀))
    (ContinuousLinearMap.prod (ContinuousLinearMap.id 𝕜 (TangentSpace I x₀)) 0 :
      TangentSpace I x₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I (id x₀)) (TangentSpace I' y₀))
    (ContinuousLinearMap.prod (ContinuousLinearMap.id 𝕜 (TangentSpace I x₀)) 0)
⊢ Eq (α := TangentSpace I x₀ →L[𝕜] TangentSpace (I.prod I') (id x₀, y₀))
    (ContinuousLinearMap.prod (mfderiv% id x₀) ((mfderiv% fun (x : M) ↦ y₀) x₀) :
      TangentSpace I x₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I (id x₀)) (TangentSpace I' y₀))
    (ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) :
      TangentSpace I x₀ →L[𝕜] Prod.{u_2, u_5} (TangentSpace I x₀) (TangentSpace I' y₀))

Tactic:
rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inl]

Premises used: mfderiv_const, ContinuousLinearMap.inl, mfderiv_id