awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
have this : Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
  (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
  (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
    (mfderiv% (↑e : M → M') x))
Tactic: have : mfderiv% (e.symm ∘ e) x = (mfderiv% e.symm (e x)).comp (mfderiv% e x) :=
    mfderiv_comp x (he.mdifferentiableAt_symm (e.map_source hx)) (he.mdifferentiableAt hx)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
have rw : Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
  (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
have this₁ : Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
Tactic: have : mfderiv% (_root_.id : M → M) x = ContinuousLinearMap.id _ _ := mfderiv_id
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this_1 :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
this :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
have rw : Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
  (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x) (mfderiv% id x)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this_1 :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
this :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x) (mfderiv% id x)
have hL : (↑e.symm : M' → M) ∘ (↑e : M → M') =ᶠ[𝓝 x] id
Tactic: apply Filter.EventuallyEq.mfderiv_eq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this_1 :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
this :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
⊢ (↑e.symm : M' → M) ∘ (↑e : M → M') =ᶠ[𝓝 x] id
have this₁ : e.source ∈ 𝓝 x
Tactic: have : e.source ∈ 𝓝 x := e.open_source.mem_nhds hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this_1 :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (((↑e.symm : M' → M) ∘ (↑e : M → M')) x))
    (mfderiv% ((↑e.symm : M' → M) ∘ (↑e : M → M')) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
      (mfderiv% (↑e : M → M') x))
this_2 :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
this : e.source ∈ 𝓝 x
⊢ e.source ⊆ {x : M | (fun (x : M) ↦ ((↑e.symm : M' → M) ∘ (↑e : M → M')) x = id x) x}
have mfld_set_tac : ∀ ⦃my_y : M⦄,
  my_y ∈ e.source →
    Membership.mem (γ := Set M) {x : M | (fun (x : M) ↦ ((↑e.symm : M' → M) ∘ (↑e : M → M')) x = id x) x} my_y
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
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 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)))
      (AddHom.toFun
        (LinearMap.toAddHom (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
        y) =
    y
have this : (ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) y = y
Tactic: have : (ContinuousLinearMap.id _ _ : TangentSpace I x →L[𝕜] TangentSpace I x) y = y := rfl
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
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 x
this : (ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) y = y
| y
have rw : (((ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
          (mfderiv% (↑e : M → M') x) :
        TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x))) :
      (a : TangentSpace I x) → TangentSpace I x)
    y :
  TangentSpace I x)
Tactic: rw [← this, ← he.symm_comp_deriv hx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
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 x
this : (ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : TangentSpace I x) → TangentSpace I x) y = y
⊢ ((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)))
      (AddHom.toFun
        (LinearMap.toAddHom (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
        y) =
    y
have conv_rhs : Eq.{u_2 + 1} (α := TangentSpace I 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)))
      (AddHom.toFun
        (LinearMap.toAddHom (↑(mfderiv% (↑e : M → M') x) : TangentSpace I x →ₗ[𝕜] TangentSpace I' ((↑e : M → M') x)))
        y) :
    TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x)))
  (((ContinuousLinearMap.comp (M₂ := TangentSpace I' ((↑e : M → M') x)) (mfderiv% (↑e.symm : M' → M) ((↑e : M → M') x))
            (mfderiv% (↑e : M → M') x) :
          TangentSpace I x →L[𝕜] TangentSpace I ((↑e.symm : M' → M) ((↑e : M → M') x))) :
        (a : TangentSpace I x) → TangentSpace I x)
      y :
    TangentSpace I x)
Tactic: conv_rhs => rw [← this, ← he.symm_comp_deriv hx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
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)
⊢ 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
have this : (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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
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
| y
have 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))
Tactic: rw [← this, ← he.comp_symm_deriv (e.map_source hx)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
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
⊢ 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
have 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)
Tactic: conv_rhs => rw [← this, ← he.comp_symm_deriv (e.map_source hx)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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'
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 ((↑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)
have 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)
Tactic: rw [e.left_inv hx]