awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
⊢ DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ x') ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
exact differentiableAt_fun_id

Premises used: differentiableAt_fun_id
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
⊢ DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
differentiableAt_const _

Premises used: differentiableAt_const
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
⊢ DifferentiableAt 𝕜 (F := E) (fun (x' : E) ↦ 0) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
exact differentiableAt_const _

Premises used: differentiableAt_const
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
⊢ UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
ModelWithCorners.uniqueDiffWithinAt_image I

Premises used: ModelWithCorners.uniqueDiffWithinAt_image
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
⊢ UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
exact ModelWithCorners.uniqueDiffWithinAt_image I

Premises used: ModelWithCorners.uniqueDiffWithinAt_image
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
⊢ DifferentiableAt 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
differentiableAt_id.prodMk (differentiableAt_const _)

Premises used: DifferentiableAt.prodMk, differentiableAt_const, differentiableAt_id
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
⊢ DifferentiableAt 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
exact differentiableAt_id.prodMk (differentiableAt_const _)

Premises used: DifferentiableAt.prodMk, differentiableAt_const, differentiableAt_id
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
⊢ Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) (range (↑I : H → E))
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)

Tactic:
have B : fderivWithin 𝕜 (fun x' : E ↦ (x', (0 : E))) (Set.range I) (I ((chartAt H x) x)) v
      = (v, 0) := by
    rw [fderivWithin_eq_fderiv, DifferentiableAt.fderiv_prodMk]
    · simp
    · exact differentiableAt_fun_id
    · exact differentiableAt_const _
    · exact ModelWithCorners.uniqueDiffWithinAt_image I
    · exact differentiableAt_id.prodMk (differentiableAt_const _)
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) (range (↑I : H → E))
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
simp :
  Eq (α := TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    ((fderivWithin 𝕜
            (fun (x_1 : E) ↦
              ((↑I : H → E)
                  ((↑(ChartedSpace.chartAt x) : M → H)
                    ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
                0))
            (range (↑I : H → E)) ((↑I : H → E) ((↑(ChartedSpace.chartAt x) : M → H) x)) :
          (a : TangentSpace I x) → TangentSpace I.tangent ⟨x, 0⟩)
        v :
      TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    ((v, 0) : E × E)
⊢ Eq (α := TangentBundle I.tangent (TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)))
    (tangentMap I I.tangent (zeroSection E (TangentSpace I)) ⟨x, v⟩)
    ⟨⟨TotalSpace.proj (F := E) (E := TangentSpace I) ⟨x, v⟩, 0⟩, (TotalSpace.snd (E := TangentSpace I) ⟨x, v⟩, 0)⟩

Tactic:
simp +unfoldPartialApp only [Bundle.zeroSection, tangentMap, mfderiv, A,
    if_pos, chartAt, FiberBundle.chartedSpace_chartAt, TangentBundle.trivializationAt_apply,
    Function.comp_def, map_zero, mfld_simps]

Premises used: mfderiv, chartAt, FiberBundle.chartedSpace_chartAt, TangentBundle.trivializationAt_apply, map_zero, Bundle.zeroSection, if_pos, Function.comp_def, tangentMap
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0)) (range (↑I : H → E))
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
⊢ Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)

Tactic:
rw [← fderivWithin_inter N] at B

Premises used: fderivWithin_inter
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
rw :
  Eq (α := TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    ((fderivWithin 𝕜
            (fun (x_1 : E) ↦
              ((↑I : H → E)
                  ((↑(ChartedSpace.chartAt x) : M → H)
                    ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
                0))
            (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
            ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
          (a : TangentSpace I x) → TangentSpace I.tangent ⟨x, 0⟩)
        v :
      TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
⊢ Eq (α := TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    ((fderivWithin 𝕜
            (fun (x_1 : E) ↦
              ((↑I : H → E)
                  ((↑(ChartedSpace.chartAt x) : M → H)
                    ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
                0))
            (range (↑I : H → E)) ((↑I : H → E) ((↑(ChartedSpace.chartAt x) : M → H) x)) :
          (a : TangentSpace I x) → TangentSpace I.tangent ⟨x, 0⟩)
        v :
      TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    ((v, 0) : E × E)

Tactic:
rw [← fderivWithin_inter N, ← B]

Premises used: fderivWithin_inter
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
e_a :
  Eq (α :=
    TangentSpace I x →L[𝕜] TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    (fderivWithin 𝕜
      (fun (x_1 : E) ↦
        ((↑I : H → E)
            ((↑(ChartedSpace.chartAt x) : M → H)
              ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
          0))
      (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
    (fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
      (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
⊢ Eq (α := TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    ((fderivWithin 𝕜
            (fun (x_1 : E) ↦
              ((↑I : H → E)
                  ((↑(ChartedSpace.chartAt x) : M → H)
                    ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
                0))
            (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
            ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
          (a : TangentSpace I x) → TangentSpace I.tangent ⟨x, 0⟩)
        v :
      TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)

Tactic:
congr 1
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
⊢ Eq (α :=
    TangentSpace I x →L[𝕜] TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    (fderivWithin 𝕜
      (fun (x_1 : E) ↦
        ((↑I : H → E)
            ((↑(ChartedSpace.chartAt x) : M → H)
              ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
          0))
      (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
    (fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
      (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))

Tactic:
fderivWithin_congr (fun y hy ↦ ?_) ?_

Premises used: setOf, fderivWithin_congr, instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
e_a :
  ∀ (y : E)
    (hy : y ∈ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target),
    Eq (α := E × E)
      ((↑I : H → E)
          ((↑(ChartedSpace.chartAt x) : M → H)
            ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) y))),
        0)
      (y, 0)
e_a₁ :
  Eq (α := E × E)
    ((↑I : H → E)
        ((↑(ChartedSpace.chartAt x) : M → H)
          ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M)
            ((↑I.symm : E → H) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))))),
      0)
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x), 0)
⊢ Eq (α :=
    TangentSpace I x →L[𝕜] TangentSpace I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I)) ⟨x, 0⟩)
    (fderivWithin 𝕜
      (fun (x_1 : E) ↦
        ((↑I : H → E)
            ((↑(ChartedSpace.chartAt x) : M → H)
              ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) x_1))),
          0))
      (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
    (fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
      (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))

Tactic:
refine fderivWithin_congr (fun y hy ↦ ?_) ?_

Premises used: fderivWithin_congr
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
y : E
hy : y ∈ range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
⊢ y ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target

Tactic:
simp only [mfld_simps] at hy
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
y : E
hy : y ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
⊢ Eq (α := E × E)
    ((↑I : H → E)
        ((↑(ChartedSpace.chartAt x) : M → H)
          ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M) ((↑I.symm : E → H) y))),
      0)
    (y, 0)

Tactic:
simp only [hy, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∈
    𝓝 ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
A : (MDiffAt fun (x : M) ↦ ⟨x, 0⟩) x
B :
  Eq (α := E × E)
    (((fderivWithin 𝕜 (F := E × E) (fun (x' : E) ↦ (x', 0))
              (range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
              ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) :
            E →L[𝕜] E × E) :
          (a : E) → E × E)
        v :
      E × E)
    ((v, 0) : TangentSpace I x × E)
⊢ Eq (α := E × E)
    ((↑I : H → E)
        ((↑(ChartedSpace.chartAt x) : M → H)
          ((↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt x)) : H → M)
            ((↑I.symm : E → H) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))))),
      0)
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x), 0)

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : C^n⟮I, M; I', M'⟯
hn : n ≠ 0
⊢ MDiff (⇑f : (a : M) → M')

Tactic:
f.contMDiff.mdifferentiable hn

Premises used: ContMDiff.mdifferentiable, ContMDiffMap.contMDiff