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'
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')).1,
      ((ContinuousLinearMap.fst 𝕜 (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')).1) :
          (a : TangentSpace (I.prod I') p.proj) → TangentSpace I p.proj.1)
        (p.snd (E := TangentSpace (I.prod I')))⟩
    ⟨p.proj (E := TangentSpace (I.prod I')).1, p.snd (E := TangentSpace (I.prod I')).1⟩
rw₁ : UniqueMDiffWithinAt (I.prod I') s (p.proj (E := TangentSpace (I.prod I')))
⊢ Eq (α := TangentBundle I M)
    ⟨p.proj (E := TangentSpace (I.prod I')).1,
      (mfderivWithin (I.prod I') I Prod.fst s (p.proj (E := TangentSpace (I.prod I'))) :
          (a : TangentSpace (I.prod I') p.proj) → TangentSpace I p.proj.1)
        (p.snd (E := TangentSpace (I.prod I')))⟩
    ⟨p.proj (E := TangentSpace (I.prod I')).1, p.snd (E := TangentSpace (I.prod I')).1⟩

Tactic:
rw [mfderivWithin_fst]

Premises used: mfderivWithin_fst
-- 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⟩).1,
        ((ContinuousLinearMap.fst 𝕜
                (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⟩).1) :
            (a : TangentSpace (I.prod I') ⟨proj, snd⟩.proj) → TangentSpace I ⟨proj, snd⟩.proj.1)
          (TotalSpace.snd (E := TangentSpace (I.prod I')) ⟨proj, snd⟩)⟩
      ⟨(TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1,
        (TotalSpace.snd (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1⟩
⊢ Eq (α := TangentBundle I M)
    ⟨p.proj (E := TangentSpace (I.prod I')).1,
      ((ContinuousLinearMap.fst 𝕜 (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')).1) :
          (a : TangentSpace (I.prod I') p.proj) → TangentSpace I p.proj.1)
        (p.snd (E := TangentSpace (I.prod I')))⟩
    ⟨p.proj (E := TangentSpace (I.prod I')).1, p.snd (E := TangentSpace (I.prod I')).1⟩

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⟩).1,
      ((ContinuousLinearMap.fst 𝕜
              (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⟩).1) :
          (a : TangentSpace (I.prod I') ⟨proj, snd⟩.proj) → TangentSpace I ⟨proj, snd⟩.proj.1)
        (TotalSpace.snd (E := TangentSpace (I.prod I')) ⟨proj, snd⟩)⟩
    ⟨(TotalSpace.proj (F := E × E') (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1,
      (TotalSpace.snd (E := TangentSpace (I.prod I')) ⟨proj, snd⟩).1⟩

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')))
⊢ UniqueMDiffWithinAt (I.prod I') s (p.proj (E := TangentSpace (I.prod 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
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')))
⊢ UniqueMDiffWithinAt (I.prod I') s (p.proj (E := TangentSpace (I.prod 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'
x : M × M'
⊢ HasMFDerivAt (I.prod I') I' Prod.snd x (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
⟨continuous_snd.continuousAt, ?_⟩

Premises used: HasMFDerivAt, continuous_snd, Continuous.continuousAt, And.intro
-- 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 × M'
refine :
  HasFDerivWithinAt (𝕜 := 𝕜) (writtenInExtChartAt (I.prod I') I' x Prod.snd)
    (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
    (range (↑(I.prod I') : ModelProd H H' → E × E')) ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x)
⊢ HasMFDerivAt (I.prod I') I' Prod.snd x (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
refine ⟨continuous_snd.continuousAt, ?_⟩
-- 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 × M'
h :
  ∀ (y : E × E') (hy : y ∈ (extChartAt (I.prod I') x).target),
    ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2
⊢ ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2

Tactic:
filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy

Premises used: extChartAt_target_mem_nhdsWithin
-- 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 × M'
y : E × E'
hy : y ∈ ((extChartAt I x.1).prod (extChartAt I' x.2)).target
⊢ ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2

Tactic:
(extChartAt I' x.2).right_inv hy.2

Premises used: extChartAt, PartialEquiv.right_inv, And.right, Prod.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'
x : M × M'
y : E × E'
hy : y ∈ ((extChartAt I x.1).prod (extChartAt I' x.2)).target
⊢ ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2

Tactic:
exact (extChartAt I' x.2).right_inv hy.2

Premises used: extChartAt, PartialEquiv.right_inv, And.right, Prod.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'
x : M × M'
⊢ ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2

Tactic:
have :
    ∀ᶠ y in 𝓝[range (I.prod I')] extChartAt (I.prod I') x x,
      (extChartAt I' x.2 ∘ Prod.snd ∘ (extChartAt (I.prod I') x).symm) y = y.2 := by
    /- porting note: was
    apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin (I.prod I') x)
    mfld_set_tac
    -/
    filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
    rw [extChartAt_prod] at hy
    exact (extChartAt I' x.2).right_inv hy.2
-- 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 × M'
this :
  ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2
apply :
  ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M'))
      ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x) =
    ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x).2
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (writtenInExtChartAt (I.prod I') I' x Prod.snd)
    (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
    (range (↑(I.prod I') : ModelProd H H' → E × E')) ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x)

Tactic:
apply HasFDerivWithinAt.congr_of_eventuallyEq hasFDerivWithinAt_snd this

Premises used: HasFDerivWithinAt.congr_of_eventuallyEq, hasFDerivWithinAt_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'
x : M × M'
this :
  ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2
⊢ ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M'))
      ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x) =
    ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x).2

Tactic:
(extChartAt I' x.2).right_inv <| (extChartAt I' x.2).map_source (mem_extChartAt_source _)

Premises used: extChartAt, PartialEquiv.map_source, mem_extChartAt_source, PartialEquiv.right_inv, Prod.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'
x : M × M'
this :
  ∀ᶠ (y : E × E') in
    𝓝[range (↑(I.prod I') : ModelProd H H' → E × E')] (↑(extChartAt (I.prod I') x) : M × M' → E × E') x,
    ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M')) y = y.2
⊢ ((↑(extChartAt I' x.2) : M' → E') ∘ Prod.snd ∘ (↑(extChartAt (I.prod I') x).symm : E × E' → M × M'))
      ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x) =
    ((↑(extChartAt (I.prod I') x) : M × M' → E × E') x).2

Tactic:
exact (extChartAt I' x.2).right_inv <| (extChartAt I' x.2).map_source (mem_extChartAt_source _)

Premises used: extChartAt, PartialEquiv.map_source, mem_extChartAt_source, PartialEquiv.right_inv, Prod.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')
x : M × M'
⊢ HasMFDerivWithinAt (I.prod I') I' Prod.snd s x (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
(hasMFDerivAt_snd x).hasMFDerivWithinAt

Premises used: HasMFDerivAt.hasMFDerivWithinAt, hasMFDerivAt_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'
x : M × M'
⊢ MDiffAt Prod.snd x

Tactic:
(hasMFDerivAt_snd x).mdifferentiableAt

Premises used: HasMFDerivAt.mdifferentiableAt, hasMFDerivAt_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')
x : M × M'
⊢ MDiffAt[s] Prod.snd x

Tactic:
mdifferentiableAt_snd.mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, mdifferentiableAt_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'
⊢ MDiff Prod.snd

Tactic:
fun _ ↦ mdifferentiableAt_snd

Premises used: mdifferentiableAt_snd, 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 × M')
⊢ MDiff[s] Prod.snd

Tactic:
mdifferentiable_snd.mdifferentiableOn

Premises used: mdifferentiable_snd, 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 × M'
⊢ Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I' x.2) (mfderiv% Prod.snd x)
    (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
(hasMFDerivAt_snd x).mfderiv

Premises used: HasMFDerivAt.mfderiv, TangentSpace, hasMFDerivAt_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')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
rw :
  Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I' x.2) (mfderiv% Prod.snd x)
    (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
⊢ Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I' x.2) (mfderivWithin (I.prod I') I' Prod.snd s x)
    (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
rw [MDifferentiable.mfderivWithin mdifferentiableAt_snd hxs]

Premises used: mdifferentiableAt_snd, MDifferentiable.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'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
⊢ Eq (α := TangentSpace (I.prod I') x →L[𝕜] TangentSpace I' x.2) (mfderiv% Prod.snd x)
    (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
mfderiv_snd

Premises used: mfderiv_snd