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
inst_6 : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ Eq (α := TangentSpace I y →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y))
      (mfderiv% (↑(extChartAt I x) : M → E) y))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I y))
have this : y = (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)
Tactic: have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm
-- 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
inst_6 : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ ContinuousLinearMap.IsInvertible (M := TangentSpace I y) (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (mfderiv% (↑(extChartAt I x) : M → E) y)
have h'y : (↑(extChartAt I x) : M → E) y ∈ (extChartAt I x).target
Tactic: have h'y : extChartAt I x y ∈ (extChartAt I x).target := (extChartAt I x).map_source hy
-- 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
inst_6 : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
h'y : (↑(extChartAt I x) : M → E) y ∈ (extChartAt I x).target
⊢ ContinuousLinearMap.IsInvertible (M := TangentSpace I y) (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (mfderiv% (↑(extChartAt I x) : M → E) y)
have Z : ContinuousLinearMap.IsInvertible (M :=
  TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) (M₂ :=
  TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
  (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) :
    TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) →L[𝕜]
      TangentSpace 𝓘(𝕜, E)
        ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))))
Tactic: have Z := ContinuousLinearMap.IsInvertible.of_inverse
    (mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm h'y)
    (mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt h'y)
-- 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
inst_6 : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
h'y : (↑(extChartAt I x) : M → E) y ∈ (extChartAt I x).target
Z :
  ContinuousLinearMap.IsInvertible (M :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) (M₂ :=
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) →L[𝕜]
        TangentSpace 𝓘(𝕜, E)
          ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))))
⊢ ContinuousLinearMap.IsInvertible (M := TangentSpace I y) (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (mfderiv% (↑(extChartAt I x) : M → E) y)
have this : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y
Tactic: have : (extChartAt I x).symm ((extChartAt I x) y) = y := (extChartAt I x).left_inv hy
-- 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
inst_6 : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
h'y : (↑(extChartAt I x) : M → E) y ∈ (extChartAt I x).target
Z :
  ContinuousLinearMap.IsInvertible (M :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) (M₂ :=
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) →L[𝕜]
        TangentSpace 𝓘(𝕜, E)
          ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))))
this : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y
⊢ ContinuousLinearMap.IsInvertible (M := TangentSpace I y) (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (mfderiv% (↑(extChartAt I x) : M → E) y)
have rwa : ∀
  (Z :
    ContinuousLinearMap.IsInvertible (M := TangentSpace I y) (M₂ :=
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y)) (mfderiv% (↑(extChartAt I x) : M → E) y))
  (this : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y),
  ContinuousLinearMap.IsInvertible (M := TangentSpace I y) (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (mfderiv% (↑(extChartAt I x) : M → E) y)
Tactic: rwa [this] at Z
Cleared hypotheses: Z, 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
inst_6 : IsManifold I 1 M
x₀ x : M
hx : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x₀)).source
⊢ Eq (α := TangentSpace I x →L[𝕜] E)
    (Trivialization.continuousLinearMapAt 𝕜 (E := TangentSpace I) (trivializationAt E (TangentSpace I) x₀) x)
    (mfderiv% (↑(extChartAt I x₀) : M → E) x)
have this : MDiffAt (↑(extChartAt I x₀) : M → E) x
Tactic: have : MDiffAt (extChartAt I x₀) x := mdifferentiableAt_extChartAt 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
inst_6 : IsManifold I 1 M
x₀ x : M
hx : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x₀)).source
⊢ Eq (α := E →L[𝕜] TangentSpace I x)
    (Trivialization.symmL 𝕜 (E := TangentSpace I) (trivializationAt E (TangentSpace I) x₀) x)
    (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x))
have this : MDiffAt[range (↑I : H → E)] ((↑(OpenPartialHomeomorph.symm (chartAt H x₀)) : H → M) ∘ (↑I.symm : E → H))
  ((↑I : H → E) ((↑(chartAt H x₀) : M → H) x))
Tactic: have : MDiffAt[range I] ((chartAt H x₀).symm ∘ I.symm) (I (chartAt H x₀ x)) := by
    simpa using mdifferentiableWithinAt_extChartAt_symm (by simp [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
x : M
φ : PartialEquiv M E := extChartAt I x
⊢ Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 ((↑φ : M → E) ∘ (↑φ.symm : E → M)) (range (↑I : H → E)) ((↑φ : M → E) x))
    (ContinuousLinearMap.id 𝕜 E)
have eq_nhd : (↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M) =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
  id
Tactic: have eq_nhd : ((extChartAt I x) ∘ (extChartAt I x).symm) =ᶠ[𝓝[range I] (extChartAt I x x)] id :=
    Filter.eventuallyEq_of_mem (extChartAt_target_mem_nhdsWithin x)
      (fun _ ↦ (extChartAt I x).right_inv)
-- 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
x : M
φ : PartialEquiv M E := extChartAt I x
eq_nhd :
  (↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M) =ᶠ[𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    id
⊢ Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 ((↑φ : M → E) ∘ (↑φ.symm : E → M)) (range (↑I : H → E)) ((↑φ : M → E) x))
    (ContinuousLinearMap.id 𝕜 E)
have rw : Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 id (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
  (ContinuousLinearMap.id 𝕜 E)
Tactic: rw [eq_nhd.fderivWithin_eq (by simp)]
-- 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
inst_6 : IsManifold I 1 M
x : M
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    (mfderiv% (↑(extChartAt I x) : M → E) x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
have rw : VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H x)
    (achart H x) x =
  ContinuousLinearMap.id 𝕜 (TangentSpace I x)
Tactic: rw [← TangentBundle.continuousLinearMapAt_trivializationAt (by simp),
    TangentBundle.continuousLinearMapAt_trivializationAt_eq_core (by simp)]
-- 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
inst_6 : IsManifold I 1 M
x : M
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H x)
      (achart H x) x =
    ContinuousLinearMap.id 𝕜 (TangentSpace I x)
have h : ∀ (v : E),
  Eq (α := E)
    ((VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H x)
            (achart H x) x :
          (a : E) → E)
        v :
      E)
    ((ContinuousLinearMap.id 𝕜 (TangentSpace I x) : (a : E) → E) v : E)
Tactic: ext v
-- 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
inst_6 : IsManifold I 1 M
x : M
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) →L[𝕜]
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)))
have hcomp : Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
  (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (mfderiv% (↑(extChartAt I x) : M → E) x))
  (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
Tactic: have hcomp := mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt' (I := I)
    (mem_extChartAt_source x)
-- 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
inst_6 : IsManifold I 1 M
x : M
hcomp :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
      (mfderiv% (↑(extChartAt I x) : M → E) x))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) →L[𝕜]
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)))
have hcomp₁ : Eq (α := TangentSpace I x →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
  (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) :
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) →L[𝕜]
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
  (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
Tactic: rw [mfderiv_extChartAt_self, ContinuousLinearMap.comp_id] at hcomp
Cleared hypotheses: hcomp
-- 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
inst_6 : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ (ContinuousLinearMap.inverse
          (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
            ((↑(extChartAt I x) : M → E) x)) :
        (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) →
          TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      v =
    v
have rw : (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :
      (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) →
        TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    v =
  v
Tactic: rw [mfderivWithin_range_extChartAt_symm, ContinuousLinearMap.inverse_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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
x : M
⊢ UniqueDiffWithinAt 𝕜 ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have simp : UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: simp only [preimage_univ, univ_inter]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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
s : Set M
x : M
⊢ UniqueMDiffWithinAt I s x ↔
    UniqueDiffWithinAt 𝕜 ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ (extChartAt I x).target)
      ((↑(extChartAt I x) : M → E) x)
have st : 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ (extChartAt I x).target] (↑(extChartAt I x) : M → E) x
Tactic: apply uniqueDiffWithinAt_congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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
s : Set M
x : M
⊢ 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ (extChartAt I x).target] (↑(extChartAt I x) : M → E) x
have st : 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x ⊓
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ (extChartAt I x).target] (↑(extChartAt I x) : M → E) x
Tactic: rw [nhdsWithin_inter, nhdsWithin_inter, nhdsWithin_extChartAt_target_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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
s : Set M
x : M
st :
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x ⊓
      𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ (extChartAt I x).target] (↑(extChartAt I x) : M → E) x
⊢ 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ (extChartAt I x).target] (↑(extChartAt I x) : M → E) x
have st₁ : 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x ⊓
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x ⊓
    𝓝[(extChartAt I x).target] (↑(extChartAt I x) : M → E) x
Tactic: rw [nhdsWithin_inter, nhdsWithin_inter, nhdsWithin_extChartAt_target_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (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
s : Set M
x : M
st :
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x ⊓
      𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ (extChartAt I x).target] (↑(extChartAt I x) : M → E) x
st₁ :
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x ⊓
      𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x ⊓
      𝓝[(extChartAt I x).target] (↑(extChartAt I x) : M → E) x
⊢ 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ (extChartAt I x).target] (↑(extChartAt I x) : M → E) x
have st₂ : 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x ⊓
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x ⊓
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
Tactic: rw [nhdsWithin_inter, nhdsWithin_inter, nhdsWithin_extChartAt_target_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
x : M
y : M'
s : Set M
t : Set M'
hs : UniqueMDiffWithinAt I s x
ht : UniqueMDiffWithinAt I' t y
⊢ UniqueMDiffWithinAt (I.prod I') (s ×ˢ t) (x, y)
have refine : ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ×ˢ
    ((↑(extChartAt I' y).symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ⊆
  (↑(extChartAt (I.prod I') (x, y)).symm : E × E' → M × M') ⁻¹' s ×ˢ t ∩ range (↑(I.prod I') : ModelProd H H' → E × E')
Tactic: refine (hs.prod ht).mono ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
x : M
y : M'
s : Set M
t : Set M'
hs : UniqueMDiffWithinAt I s x
ht : UniqueMDiffWithinAt I' t y
⊢ ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ×ˢ
      ((↑(extChartAt I' y).symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ⊆
    (↑(extChartAt (I.prod I') (x, y)).symm : E × E' → M × M') ⁻¹' s ×ˢ t ∩
      range (↑(I.prod I') : ModelProd H H' → E × E')
have rw : ((↑(extChartAt I x).symm : E → M) ⁻¹' s) ×ˢ ((↑(extChartAt I' y).symm : E' → M') ⁻¹' t) ∩
    range (↑I : H → E) ×ˢ range (↑I' : H' → E') ⊆
  ((↑(extChartAt I x).symm : E → M) ⁻¹' s) ×ˢ ((↑(extChartAt I' y).symm : E' → M') ⁻¹' t) ∩
    range (↑I : H → E) ×ˢ range (↑I' : H' → E')
Tactic: rw [ModelWithCorners.range_prod, ← prod_inter_prod]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
⊢ MDifferentiableWithinAt I I' f univ x ↔ MDifferentiableAt I I' f x
have simp_rw : LiftPropWithinAt (DifferentiableWithinAtProp I I') f univ x ↔ MDifferentiableAt I I' f x
Tactic: simp_rw [MDifferentiableWithinAt, MDifferentiableAt, ChartedSpace.LiftPropAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
simp_rw : LiftPropWithinAt (DifferentiableWithinAtProp I I') f univ x ↔ MDifferentiableAt I I' f x
⊢ MDifferentiableWithinAt I I' f univ x ↔ MDifferentiableAt I I' f x
have simp_rw₁ : LiftPropWithinAt (DifferentiableWithinAtProp I I') f univ x ↔ LiftPropAt (DifferentiableWithinAtProp I I') f x
Tactic: simp_rw [MDifferentiableWithinAt, MDifferentiableAt, ChartedSpace.LiftPropAt]