awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
e : OpenPartialHomeomorph M M'
he_1 : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
y : TangentSpace I' ((↑e : M → M') x)
⊢ (ContinuousLinearMap.id 𝕜 (TangentSpace I' ((↑e : M → M') x)) :
        (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I' ((↑e : M → M') x))
      y =
    y

Tactic:
have :
        (ContinuousLinearMap.id 𝕜 _ : TangentSpace I' (e x) →L[𝕜] TangentSpace I' (e x)) y = y :=
        rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
e : OpenPartialHomeomorph M M'
he_1 : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
y : TangentSpace I' ((↑e : M → M') x)
this :
  (ContinuousLinearMap.id 𝕜 (TangentSpace I' ((↑e : M → M') x)) :
        (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I' ((↑e : M → M') x))
      y =
    y
rw :
  (((ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
            (mfderiv% (↑e : M → M') ((↑e.symm : M' → M) ((↑e : M → M') x)))
            (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x)) :
          TangentSpace I' ((↑e : M → M') x) →L[𝕜]
            TangentSpace I' ((↑e : M → M') ((↑e.symm : M' → M) ((↑e : M → M') x)))) :
        (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I' ((↑e : M → M') x))
      y :
    TangentSpace I' ((↑e : M → M') x))
| y

Tactic:
rw [← this, ← he.comp_symm_deriv (e.map_source hx)]

Premises used: OpenPartialHomeomorph.MDifferentiable.comp_symm_deriv, OpenPartialHomeomorph.map_source
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
e : OpenPartialHomeomorph M M'
he_1 : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
y : TangentSpace I' ((↑e : M → M') x)
this :
  (ContinuousLinearMap.id 𝕜 (TangentSpace I' ((↑e : M → M') x)) :
        (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I' ((↑e : M → M') x))
      y =
    y
conv_rhs :
  Eq (α := TangentSpace I' ((↑e : M → M') x))
    (AddHom.toFun (M := TangentSpace I x)
      (LinearMap.toAddHom (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
      (((mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (TangentSpace I' ((↑e : M → M') x))
              (TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))) :
          (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
        y))
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
            (mfderiv% (↑e : M → M') ((↑e.symm : M' → M) ((↑e : M → M') x)))
            (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x)) :
          TangentSpace I' ((↑e : M → M') x) →L[𝕜]
            TangentSpace I' ((↑e : M → M') ((↑e.symm : M' → M) ((↑e : M → M') x)))) :
        (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I' ((↑e : M → M') x))
      y)
⊢ AddHom.toFun (M := TangentSpace I x)
      (LinearMap.toAddHom (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
      (((mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (TangentSpace I' ((↑e : M → M') x))
              (TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))) :
          (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
        y) =
    y

Tactic:
conv_rhs => rw [← this, ← he.comp_symm_deriv (e.map_source hx)]

Premises used: OpenPartialHomeomorph.MDifferentiable.comp_symm_deriv, OpenPartialHomeomorph.map_source
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
e : OpenPartialHomeomorph M M'
he_1 : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
y : TangentSpace I' ((↑e : M → M') x)
this :
  (ContinuousLinearMap.id 𝕜 (TangentSpace I' ((↑e : M → M') x)) :
        (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I' ((↑e : M → M') x))
      y =
    y
rw :
  Eq (α := TangentSpace I' ((↑e : M → M') x))
    (AddHom.toFun (M := TangentSpace I x)
      (LinearMap.toAddHom (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
      (((mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (TangentSpace I' ((↑e : M → M') x))
              (TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))) :
          (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I x)
        y))
    ((ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% (↑e : M → M') x)
          (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x)) :
        (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I' ((↑e : M → M') x))
      y)
⊢ Eq (α := TangentSpace I' ((↑e : M → M') x))
    (AddHom.toFun (M := TangentSpace I x)
      (LinearMap.toAddHom (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
      (((mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (TangentSpace I' ((↑e : M → M') x))
              (TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))) :
          (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
        y))
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
            (mfderiv% (↑e : M → M') ((↑e.symm : M' → M) ((↑e : M → M') x)))
            (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x)) :
          TangentSpace I' ((↑e : M → M') x) →L[𝕜]
            TangentSpace I' ((↑e : M → M') ((↑e.symm : M' → M) ((↑e : M → M') x)))) :
        (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I' ((↑e : M → M') x))
      y)

Tactic:
rw [e.left_inv hx]

Premises used: OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
e : OpenPartialHomeomorph M M'
he_1 : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
y : TangentSpace I' ((↑e : M → M') x)
this :
  (ContinuousLinearMap.id 𝕜 (TangentSpace I' ((↑e : M → M') x)) :
        (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I' ((↑e : M → M') x))
      y =
    y
⊢ Eq (α := TangentSpace I' ((↑e : M → M') x))
    (AddHom.toFun (M := TangentSpace I x)
      (LinearMap.toAddHom (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
      (((mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (TangentSpace I' ((↑e : M → M') x))
              (TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))) :
          (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I x)
        y))
    ((ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% (↑e : M → M') x)
          (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x)) :
        (a : TangentSpace I' ((↑e : M → M') x)) → TangentSpace I' ((↑e : M → M') x))
      y)

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
⊢ Function.Bijective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' ((↑e : M → M') x))
    (⇑(mfderiv% (↑e : M → M') x) : (a : TangentSpace I x) → TangentSpace I' ((↑e : M → M') x))

Tactic:
(he.mfderiv hx).bijective

Premises used: ContinuousLinearEquiv.bijective, OpenPartialHomeomorph.MDifferentiable.mfderiv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
⊢ Function.Injective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' ((↑e : M → M') x))
    (⇑(mfderiv% (↑e : M → M') x) : (a : TangentSpace I x) → TangentSpace I' ((↑e : M → M') x))

Tactic:
(he.mfderiv hx).injective

Premises used: OpenPartialHomeomorph.MDifferentiable.mfderiv, ContinuousLinearEquiv.injective
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
⊢ Function.Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' ((↑e : M → M') x))
    (⇑(mfderiv% (↑e : M → M') x) : (a : TangentSpace I x) → TangentSpace I' ((↑e : M → M') x))

Tactic:
(he.mfderiv hx).surjective

Premises used: OpenPartialHomeomorph.MDifferentiable.mfderiv, ContinuousLinearEquiv.surjective
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
⊢ Eq (α := Submodule 𝕜 (TangentSpace I x))
    (LinearMap.ker (M₂ := TangentSpace I' ((↑e : M → M') x))
      (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
    ⊥

Tactic:
(he.mfderiv hx).toLinearEquiv.ker

Premises used: ContinuousLinearEquiv.toLinearEquiv, OpenPartialHomeomorph.MDifferentiable.mfderiv, LinearEquiv.ker
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
⊢ Eq (α := Submodule 𝕜 (TangentSpace I' ((↑e : M → M') x)))
    (LinearMap.range (M := TangentSpace I x)
      (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
    ⊤

Tactic:
(he.mfderiv hx).toLinearEquiv.range

Premises used: ContinuousLinearEquiv.toLinearEquiv, OpenPartialHomeomorph.MDifferentiable.mfderiv, LinearEquiv.range
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
⊢ Eq.{u_5 + 1} (α := Set (TangentSpace I' ((↑e : M → M') x)))
    (range.{u_5, u_2 + 1} (ι := TangentSpace I x)
      (⇑(mfderiv% (↑e : M → M') x) : (a : TangentSpace I x) → TangentSpace I' ((↑e : M → M') x)))
    univ

Tactic:
(he.mfderiv_surjective hx).range_eq

Premises used: Function.Surjective.range_eq, OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he' : MDifferentiable I' I'' e'
left : MDiff[(e ≫ₕ e').source] (↑(e ≫ₕ e') : M → M'')
right : MDiff[(e ≫ₕ e').target] (↑(e ≫ₕ e').symm : M'' → M)
⊢ MDifferentiable I I'' (e ≫ₕ e')

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he' : MDifferentiable I' I'' e'
x : M
hx : x ∈ (e ≫ₕ e').source
⊢ x ∈ e.source ∧ (↑e : M → M') x ∈ e'.source

Tactic:
simp only [mfld_simps] at hx
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he' : MDifferentiable I' I'' e'
x : M
hx : x ∈ e.source ∧ (↑e : M → M') x ∈ e'.source
⊢ MDiffAt[(e ≫ₕ e').source] (↑(e ≫ₕ e') : M → M'') x

Tactic:
((he'.mdifferentiableAt hx.2).comp _ (he.mdifferentiableAt hx.1)).mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, OpenPartialHomeomorph.toFun', And.right, And.left, OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt, MDifferentiableAt.comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he' : MDifferentiable I' I'' e'
x : M
hx : x ∈ e.source ∧ (↑e : M → M') x ∈ e'.source
⊢ MDiffAt[(e ≫ₕ e').source] (↑(e ≫ₕ e') : M → M'') x

Tactic:
exact
      ((he'.mdifferentiableAt hx.2).comp _ (he.mdifferentiableAt hx.1)).mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, And.right, And.left, OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt, MDifferentiableAt.comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he' : MDifferentiable I' I'' e'
x : M''
hx : x ∈ (e ≫ₕ e').target
⊢ x ∈ e'.target ∧ (↑e'.symm : M'' → M') x ∈ e.target

Tactic:
simp only [mfld_simps] at hx
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he' : MDifferentiable I' I'' e'
x : M''
hx : x ∈ e'.target ∧ (↑e'.symm : M'' → M') x ∈ e.target
⊢ MDiffAt[(e ≫ₕ e').target] (↑(e ≫ₕ e').symm : M'' → M) x

Tactic:
((he.symm.mdifferentiableAt hx.2).comp _
          (he'.symm.mdifferentiableAt hx.1)).mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, OpenPartialHomeomorph.toFun', And.right, And.left, OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt, MDifferentiableAt.comp, OpenPartialHomeomorph.MDifferentiable.symm