awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivAt I J f p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivAt I' J' g p.2 dg
h : mfderivWithin I J f univ p.1 = df
⊢ HasMFDerivWithinAt (I.prod I') (J.prod J') (Prod.map f g) (SProd.sprod (α := Set M) (β := Set M') univ univ) p
    (ContinuousLinearMap.prodMap (mfderivWithin I J f univ p.1) (mfderivWithin I' J' g univ p.2))
have h₁ : TangentSpace I' p.2 = E' →
  HEq (α := TopologicalSpace (TangentSpace I' p.2)) (instTopologicalSpaceTangentSpace I' p.2) (β := TopologicalSpace E')
      UniformSpace.toTopologicalSpace →
    HEq.{u_5 + 1} (α := AddCommMonoid (TangentSpace I' p.2)) AddCommGroup.toAddCommMonoid (β := AddCommMonoid E')
        AddCommGroup.toAddCommMonoid →
      HEq (α := Module.{u_1, u_5} 𝕜 (TangentSpace I' p.2)) (instModuleTangentSpace I' p.2) (β := Module 𝕜 E')
          (NormedSpace.toModule : Module 𝕜 E') →
        TangentSpace J' (g p.2) = F' →
          HEq (α := TopologicalSpace (TangentSpace J' (g p.2))) (instTopologicalSpaceTangentSpace J' (g p.2)) (β :=
              TopologicalSpace F') UniformSpace.toTopologicalSpace →
            HEq.{u_14 + 1} (α := AddCommMonoid (TangentSpace J' (g p.2))) AddCommGroup.toAddCommMonoid (β :=
                AddCommMonoid F') AddCommGroup.toAddCommMonoid →
              HEq (α := Module.{u_1, u_14} 𝕜 (TangentSpace J' (g p.2))) (instModuleTangentSpace J' (g p.2)) (β :=
                  Module 𝕜 F') (NormedSpace.toModule : Module 𝕜 F') →
                mfderivWithin I' J' g univ p.2 = dg
Tactic: convert! hf.hasMFDerivWithinAt.prodMap hg.hasMFDerivWithinAt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivAt I J f p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivAt I' J' g p.2 dg
⊢ mfderivWithin I J f univ p.1 = df
have h : mfderiv% f p.1 = df
Tactic: rw [mfderivWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : ContinuousLinearMap.{u_1, u_1, u_2, u_11} (RingHom.id 𝕜) (TangentSpace I p.1) (TangentSpace J (f p.1))
hf : HasMFDerivAt I J f p.1 df
dg : ContinuousLinearMap.{u_1, u_1, u_5, u_14} (RingHom.id 𝕜) (TangentSpace I' p.2) (TangentSpace J' (g p.2))
hg : HasMFDerivAt I' J' g p.2 dg
e_11 : TangentSpace I' p.2 = E'
e_12 :
  HEq (α := TopologicalSpace (TangentSpace I' p.2)) (instTopologicalSpaceTangentSpace I' p.2) (β := TopologicalSpace E')
    UniformSpace.toTopologicalSpace
e_13 :
  HEq.{u_5 + 1} (α := AddCommMonoid (TangentSpace I' p.2)) AddCommGroup.toAddCommMonoid (β := AddCommMonoid E')
    AddCommGroup.toAddCommMonoid
e_14 :
  HEq (α := Module.{u_1, u_5} 𝕜 (TangentSpace I' p.2)) (instModuleTangentSpace I' p.2) (β := Module 𝕜 E')
    (NormedSpace.toModule : Module 𝕜 E')
e_15 : TangentSpace J' (g p.2) = F'
e_16 :
  HEq (α := TopologicalSpace (TangentSpace J' (g p.2))) (instTopologicalSpaceTangentSpace J' (g p.2)) (β :=
    TopologicalSpace F') UniformSpace.toTopologicalSpace
e_17 :
  HEq.{u_14 + 1} (α := AddCommMonoid (TangentSpace J' (g p.2))) AddCommGroup.toAddCommMonoid (β := AddCommMonoid F')
    AddCommGroup.toAddCommMonoid
e_18 :
  HEq (α := Module.{u_1, u_14} 𝕜 (TangentSpace J' (g p.2))) (instModuleTangentSpace J' (g p.2)) (β := Module 𝕜 F')
    (NormedSpace.toModule : Module 𝕜 F')
⊢ mfderivWithin I' J' g univ p.2 = dg
have h : mfderiv% g p.2 = dg
Tactic: rw [mfderivWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set M
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
⊢ 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))
have hf' : HasMFDerivWithinAt I J f (Prod.fst '' s ×ˢ t) p.1 (mfderivWithin I J f s p.1)
Tactic: have hf' : HasMFDerivAt[Prod.fst '' s ×ˢ t] f p.1 (mfderiv[s] f p.1) :=
    hf.hasMFDerivWithinAt.mono (by grind)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
s : Set M
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)
⊢ 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))
have hg' : 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)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
F : Type u_11
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
G : Type u_12
inst_13 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
F' : Type u_14
inst_16 : NormedAddCommGroup F'
inst_17 : NormedSpace 𝕜 F'
G' : Type u_15
inst_18 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
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)) (mfderiv% (Prod.map f g) p)
    (ContinuousLinearMap.prodMap (mfderiv% f p.1) (mfderiv% g p.2))
have 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))
Tactic: simp_rw [← mfderivWithin_univ, ← univ_prod_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
p : TangentBundle (I.prod I') (M × M')
⊢ 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⟩
have 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
Tactic: simp [tangentMap]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set (M × M')
p : TangentBundle (I.prod I') (M × M')
hs : UniqueMDiffWithinAt (I.prod I') s (p.proj (E := TangentSpace (I.prod I')))
⊢ 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⟩
have 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⟩
Tactic: rw [mfderivWithin_snd hs]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
s : Set (M × M')
p : TangentBundle (I.prod I') (M × M')
hs : UniqueMDiffWithinAt (I.prod I') s (p.proj (E := TangentSpace (I.prod I')))
⊢ 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⟩
have 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⟩
Tactic: rcases p with ⟨⟩
Cleared hypotheses: p, hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
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₀))
have 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₀))
Tactic: refine (mdifferentiableAt_id.mfderiv_prod mdifferentiableAt_const).trans ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
x₀ : M
y₀ : M'
⊢ 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₀))
have 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₀))
Tactic: rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inl]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
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₀))
⊢ 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₀))
have 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₀))
Tactic: rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inl]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
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₀))
⊢ 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₀))
have 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)
Tactic: rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inl]