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
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
⊢ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) ((↑(extChartAt I x) : M → E) x) =
    id ((↑(extChartAt I x) : M → E) x)

Tactic:
simp
-- 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
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
rw :
  Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 id (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (ContinuousLinearMap.id 𝕜 E)
⊢ Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 ((↑φ : M → E) ∘ (↑φ.symm : E → M)) (range (↑I : H → E)) ((↑φ : M → E) x))
    (ContinuousLinearMap.id 𝕜 E)

Tactic:
rw [eq_nhd.fderivWithin_eq (by simp)]

Premises used: Filter.EventuallyEq.fderivWithin_eq
-- 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
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 𝕜 id (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (ContinuousLinearMap.id 𝕜 E)

Tactic:
fderivWithin_id <| I.uniqueDiffOn.uniqueDiffWithinAt (mem_range_self _)

Premises used: Set.mem_range_self, UniqueDiffOn.uniqueDiffWithinAt, fderivWithin_id, ModelWithCorners.uniqueDiffOn
-- 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
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 𝕜 id (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (ContinuousLinearMap.id 𝕜 E)

Tactic:
exact fderivWithin_id <| I.uniqueDiffOn.uniqueDiffWithinAt (mem_range_self _)

Premises used: Set.mem_range_self, UniqueDiffOn.uniqueDiffWithinAt, fderivWithin_id, ModelWithCorners.uniqueDiffOn
-- 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
inst_6 : IsManifold I 1 M
x : M
⊢ x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
simp
-- 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
inst_6 : IsManifold I 1 M
x : M
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)
⊢ 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))

Tactic:
rw [← TangentBundle.continuousLinearMapAt_trivializationAt (by simp),
    TangentBundle.continuousLinearMapAt_trivializationAt_eq_core (by simp)]

Premises used: TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, TangentBundle.continuousLinearMapAt_trivializationAt
-- 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
inst_6 : IsManifold I 1 M
x : M
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)
⊢ 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:
ext v
-- 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
inst_6 : IsManifold I 1 M
x : M
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:
simpa using (tangentBundleCore I M).coordChange_self (achart H x) x (mem_chart_source H x) v

Premises used: mem_chart_source, VectorBundleCore.coordChange_self, achart, tangentBundleCore
-- 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
inst_6 : IsManifold I 1 M
x : M
⊢ 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)
-- 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
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 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

Premises used: mfderiv_extChartAt_self, ContinuousLinearMap.comp_id
-- 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
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)))
    (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))
⊢ 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)))

Tactic:
simpa using hcomp
-- 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
inst_6 : IsManifold I 1 M
x : M
v : TangentSpace I x
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
⊢ (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

Tactic:
rw [mfderivWithin_range_extChartAt_symm, ContinuousLinearMap.inverse_id]

Premises used: mfderivWithin_range_extChartAt_symm, ContinuousLinearMap.inverse_id
-- 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
inst_6 : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ (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:
ContinuousLinearMap.id_apply ..

Premises used: ContinuousLinearMap.id_apply
-- 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
inst_6 : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ (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:
exact ContinuousLinearMap.id_apply ..

Premises used: ContinuousLinearMap.id_apply
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
simp : UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ UniqueDiffWithinAt 𝕜 ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
simp only [preimage_univ, univ_inter]

Premises used: Set.univ_inter, Set.preimage_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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 𝕜 (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
I.uniqueDiffOn _ (mem_range_self _)

Premises used: Set.mem_range_self, ModelWithCorners.uniqueDiffOn
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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 𝕜 (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
exact I.uniqueDiffOn _ (mem_range_self _)

Premises used: Set.mem_range_self, ModelWithCorners.uniqueDiffOn
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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 ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
Iff.rfl

Premises used: Iff.rfl, UniqueMDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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 ∩ 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
⊢ UniqueMDiffWithinAt I s x ↔
    UniqueDiffWithinAt 𝕜 ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ (extChartAt I x).target)
      ((↑(extChartAt I x) : M → E) x)

Tactic:
apply uniqueDiffWithinAt_congr

Premises used: uniqueDiffWithinAt_congr
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
st₂ 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
⊢ 𝓝[(↑(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:
rw [nhdsWithin_inter, nhdsWithin_inter, nhdsWithin_extChartAt_target_eq]

Premises used: nhdsWithin_inter, nhdsWithin_extChartAt_target_eq
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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 t : Set M
x : M
hs : UniqueMDiffWithinAt I s x
ht : 𝓝[s] x ≤ 𝓝[t] x
⊢ 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x ≤
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
simpa only [← map_extChartAt_nhdsWithin] using Filter.map_mono ht

Premises used: Filter.map_mono, map_extChartAt_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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 t : Set M
x : M
hs : UniqueMDiffWithinAt I s x
ht : t ∈ 𝓝[s] x
⊢ UniqueMDiffWithinAt I t x

Tactic:
hs.mono_nhds (nhdsWithin_le_iff.2 ht)

Premises used: Iff.mpr, UniqueMDiffWithinAt.mono_nhds, nhdsWithin_le_iff
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
s t : Set M
h : UniqueMDiffWithinAt I s x
st : s ⊆ t
⊢ UniqueMDiffWithinAt I t x

Tactic:
UniqueDiffWithinAt.mono h <| inter_subset_inter (preimage_mono st) (Subset.refl _)

Premises used: Set.Subset.refl, UniqueMDiffWithinAt, Set.inter_subset_inter, Set.preimage_mono, UniqueDiffWithinAt.mono
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
s t : Set M
hs : UniqueMDiffWithinAt I s x
ht : t ∈ 𝓝[s] x
⊢ UniqueMDiffWithinAt I (s ∩ t) x

Tactic:
hs.mono_of_mem_nhdsWithin (Filter.inter_mem self_mem_nhdsWithin ht)

Premises used: Filter.inter_mem, UniqueMDiffWithinAt.mono_of_mem_nhdsWithin, self_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
s t : Set M
hs : UniqueMDiffWithinAt I s x
ht : t ∈ 𝓝 x
⊢ UniqueMDiffWithinAt I (s ∩ t) x

Tactic:
hs.inter' (nhdsWithin_le_nhds ht)

Premises used: UniqueMDiffWithinAt.inter', nhdsWithin_le_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
s : Set M
hs : IsOpen[inst_4] s
xs : x ∈ s
⊢ UniqueMDiffWithinAt I s x

Tactic:
(uniqueMDiffWithinAt_univ I).mono_of_mem_nhdsWithin <| nhdsWithin_le_nhds <| hs.mem_nhds xs

Premises used: UniqueMDiffWithinAt.mono_of_mem_nhdsWithin, uniqueMDiffWithinAt_univ, nhdsWithin_le_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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 t : Set M
hs : UniqueMDiffOn I s
ht : IsOpen[inst_4] t
⊢ UniqueMDiffOn I (s ∩ t)

Tactic:
fun _x hx => UniqueMDiffWithinAt.inter (hs _ hx.1) (ht.mem_nhds hx.2)

Premises used: UniqueMDiffOn, UniqueMDiffWithinAt.inter, And.right, And.left, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
hs : IsOpen[inst_4] s
⊢ UniqueMDiffOn I s

Tactic:
fun _x hx => hs.uniqueMDiffWithinAt hx

Premises used: UniqueMDiffOn, IsOpen.uniqueMDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
⊢ UniqueMDiffOn.{u_1, u_2, u_3, u_4} I (M := M) univ

Tactic:
isOpen_univ.uniqueMDiffOn

Premises used: IsOpen.uniqueMDiffOn, isOpen_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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)

Tactic:
(hs.prod ht).mono ?_

Premises used: setOf, UniqueMDiffWithinAt, ModelWithCorners.toFun', UniqueDiffWithinAt.mono, UniqueDiffWithinAt.prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
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')
⊢ UniqueMDiffWithinAt (I.prod I') (s ×ˢ t) (x, y)

Tactic:
refine (hs.prod ht).mono ?_

Premises used: UniqueMDiffWithinAt.mono, UniqueMDiffWithinAt.prod