awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
refine :
  (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
refine₁ :
  writtenInExtChartAt I I' x f ''
      ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E)) ⊆
    (↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' f '' s ∩ range (↑I' : H' → E')
refine₂ : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) = (↑(extChartAt I' (f x)) : M' → E') (f x)
⊢ UniqueMDiffWithinAt I' (f '' s) (f x)

Tactic:
refine (((hf.2.mono ?sub1).uniqueDiffWithinAt this hd).mono ?sub2).congr_pt ?pt

Premises used: UniqueDiffWithinAt.congr_pt, HasFDerivWithinAt.uniqueDiffWithinAt, And.right, UniqueDiffWithinAt.mono, HasFDerivWithinAt.mono
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) = (↑(extChartAt I' (f x)) : M' → E') (f x)

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) = (↑(extChartAt I' (f x)) : M' → E') (f x)

Tactic:
case pt => simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ :
  ∀ ⦃my_y : E⦄,
    my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E) →
      my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
mfld_set_tac₃ mfld_set_tac₄ :
  ∀ ⦃my_y : E⦄,
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) my_y) ∈ s ∧
          f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) my_y)) ∈
            (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∧
        my_y ∈ range (↑I : H → E) →
      my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)

Tactic:
mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)

Tactic:
case sub1 => mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
y : E
hys : (↑(extChartAt I x).symm : E → M) y ∈ s
hfy : (↑(extChartAt I x).symm : E → M) y ∈ f ⁻¹' (extChartAt I' (f x)).source
⊢ writtenInExtChartAt I I' x f y ∈ (↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' f '' s ∩ range (↑I' : H' → E')

Tactic:
⟨⟨_, hys, ((extChartAt I' (f x)).left_inv hfy).symm⟩, mem_range_self _⟩

Premises used: Set.mem_range_self, extChartAt, Set.Mem, setOf, Set.inter, And.intro, Exists.intro, PartialEquiv.left_inv, Eq.symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
y : E
hys : (↑(extChartAt I x).symm : E → M) y ∈ s
hfy : (↑(extChartAt I x).symm : E → M) y ∈ f ⁻¹' (extChartAt I' (f x)).source
⊢ writtenInExtChartAt I I' x f y ∈ (↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' f '' s ∩ range (↑I' : H' → E')

Tactic:
exact ⟨⟨_, hys, ((extChartAt I' (f x)).left_inv hfy).symm⟩, mem_range_self _⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
case :
  ∀ (y : E) (hys : (↑(extChartAt I x).symm : E → M) y ∈ s)
    (hfy : (↑(extChartAt I x).symm : E → M) y ∈ f ⁻¹' (extChartAt I' (f x)).source),
    writtenInExtChartAt I I' x f y ∈ (↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' f '' s ∩ range (↑I' : H' → E')
⊢ writtenInExtChartAt I I' x f ''
      ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range (↑I : H → E)) ⊆
    (↑(extChartAt I' (f x)).symm : E' → M') ⁻¹' f '' s ∩ range (↑I' : H' → E')

Tactic:
case sub2 =>
    rintro _ ⟨y, ⟨⟨hys, hfy⟩, -⟩, rfl⟩
    exact ⟨⟨_, hys, ((extChartAt I' (f x)).left_inv hfy).symm⟩, mem_range_self _⟩

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
hs : UniqueMDiffOn I s
f : M → M'
f' : M → E →L[𝕜] E'
hf : ∀ x ∈ s, HasMFDerivWithinAt I I' f s x (f' x)
hd : ∀ x ∈ s, DenseRange.{u_5, u_2} (X := E') (α := E) (⇑(f' x) : (a : E) → E')
⊢ UniqueMDiffOn I' (f '' s)

Tactic:
forall_mem_image.2 fun x hx ↦ (hs x hx).image_denseRange (hf x hx) (hd x hx)

Premises used: Iff.mpr, UniqueMDiffOn, UniqueMDiffWithinAt.image_denseRange, Set.forall_mem_image
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
hs : UniqueMDiffOn I s
f : M → M'
hf : MDiff[s] f
hd :
  ∀ x ∈ s,
    DenseRange.{u_5, u_2} (X := TangentSpace I' (f x)) (α := TangentSpace I x)
      (⇑(mfderivWithin I I' f s x) : (a : TangentSpace I x) → TangentSpace I' (f x))
⊢ UniqueMDiffOn I' (f '' s)

Tactic:
hs.image_denseRange' (fun x hx ↦ (hf x hx).hasMFDerivWithinAt) hd

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, UniqueMDiffOn.image_denseRange'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
e : OpenPartialHomeomorph M M'
he : OpenPartialHomeomorph.MDifferentiable I I' e
hx : x ∈ e.source
rw : UniqueMDiffWithinAt I' ((↑e : M → M') '' (s ∩ e.source)) ((↑e : M → M') x)
⊢ UniqueMDiffWithinAt I' (e.target ∩ (↑e.symm : M' → M) ⁻¹' s) ((↑e : M → M') x)

Tactic:
rw [← e.image_source_inter_eq', inter_comm]

Premises used: Set.inter_comm, OpenPartialHomeomorph.image_source_inter_eq'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
e : OpenPartialHomeomorph M M'
he : OpenPartialHomeomorph.MDifferentiable I I' e
hx : x ∈ e.source
⊢ UniqueMDiffWithinAt I' ((↑e : M → M') '' (s ∩ e.source)) ((↑e : M → M') x)

Tactic:
(hs.inter (e.open_source.mem_nhds hx)).image_denseRange
    (he.mdifferentiableAt hx).hasMFDerivAt.hasMFDerivWithinAt
    (he.mfderiv_surjective hx).denseRange

Premises used: OpenPartialHomeomorph.open_source, MDifferentiableAt.hasMFDerivAt, UniqueMDiffWithinAt.inter, Function.Surjective.denseRange, OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective, HasMFDerivAt.hasMFDerivWithinAt, IsOpen.mem_nhds, OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt, UniqueMDiffWithinAt.image_denseRange
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
e : OpenPartialHomeomorph M M'
he : OpenPartialHomeomorph.MDifferentiable I I' e
hx : x ∈ e.source
⊢ UniqueMDiffWithinAt I' ((↑e : M → M') '' (s ∩ e.source)) ((↑e : M → M') x)

Tactic:
exact (hs.inter (e.open_source.mem_nhds hx)).image_denseRange
    (he.mdifferentiableAt hx).hasMFDerivAt.hasMFDerivWithinAt
    (he.mfderiv_surjective hx).denseRange

Premises used: OpenPartialHomeomorph.open_source, MDifferentiableAt.hasMFDerivAt, UniqueMDiffWithinAt.inter, Function.Surjective.denseRange, OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective, HasMFDerivAt.hasMFDerivWithinAt, IsOpen.mem_nhds, OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt, UniqueMDiffWithinAt.image_denseRange
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
hs : UniqueMDiffOn I s
e : OpenPartialHomeomorph M M'
he : OpenPartialHomeomorph.MDifferentiable I I' e
⊢ UniqueMDiffOn I' (e.target ∩ (↑e.symm : M' → M) ⁻¹' s)

Tactic:
fun _x hx ↦
  e.right_inv hx.1 ▸ (hs _ hx.2).preimage_openPartialHomeomorph he (e.map_target hx.1)

Premises used: UniqueMDiffOn, Eq.rec, OpenPartialHomeomorph.toFun', UniqueMDiffWithinAt.preimage_openPartialHomeomorph, OpenPartialHomeomorph.map_target, And.right, And.left, OpenPartialHomeomorph.symm, OpenPartialHomeomorph.right_inv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
inst_6 : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
rw :
  UniqueMDiffOn 𝓘(𝕜, E)
    ((↑(extChartAt I x) : M → E) '' (s ∩ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source))
⊢ UniqueMDiffOn 𝓘(𝕜, E) ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)

Tactic:
rw [← PartialEquiv.image_source_inter_eq', inter_comm, extChartAt_source]

Premises used: extChartAt_source, Set.inter_comm, PartialEquiv.image_source_inter_eq'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
inst_6 : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
⊢ UniqueMDiffOn 𝓘(𝕜, E)
    ((↑(extChartAt I x) : M → E) '' (s ∩ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source))

Tactic:
(hs.inter (chartAt H x).open_source).image_denseRange'
    (fun y hy ↦ hasMFDerivWithinAt_extChartAt hy.2)
    fun y hy ↦ ((mdifferentiable_chart _).mfderiv_surjective hy.2).denseRange

Premises used: mdifferentiable_chart, chartAt, OpenPartialHomeomorph.open_source, UniqueMDiffOn.inter, UniqueMDiffOn.image_denseRange', hasMFDerivWithinAt_extChartAt, Function.Surjective.denseRange, OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective, And.right
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
inst_6 : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
⊢ UniqueMDiffOn 𝓘(𝕜, E)
    ((↑(extChartAt I x) : M → E) '' (s ∩ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source))

Tactic:
exact (hs.inter (chartAt H x).open_source).image_denseRange'
    (fun y hy ↦ hasMFDerivWithinAt_extChartAt hy.2)
    fun y hy ↦ ((mdifferentiable_chart _).mfderiv_surjective hy.2).denseRange

Premises used: mdifferentiable_chart, chartAt, OpenPartialHomeomorph.open_source, UniqueMDiffOn.inter, UniqueMDiffOn.image_denseRange', hasMFDerivWithinAt_extChartAt, Function.Surjective.denseRange, OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective, And.right
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
inst_6 : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
⊢ UniqueDiffOn 𝕜 ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s)

Tactic:
(hs.uniqueMDiffOn_target_inter x).uniqueDiffOn

Premises used: UniqueMDiffOn.uniqueDiffOn, UniqueMDiffOn.uniqueMDiffOn_target_inter
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
inst_6 : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : E
hy : y ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s
apply :
  (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s ⊆
    range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s
⊢ UniqueDiffWithinAt 𝕜 (range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s) y

Tactic:
apply (hs.uniqueDiffOn_target_inter x y hy).mono

Premises used: UniqueMDiffOn.uniqueDiffOn_target_inter, UniqueDiffWithinAt.mono
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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
inst_6 : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : E
hy : y ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s
⊢ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s ⊆
    range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' s

Tactic:
apply inter_subset_inter_left _ (extChartAt_target_subset_range x)

Premises used: Set.inter_subset_inter_left, extChartAt_target_subset_range
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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_8
inst_9 : TopologicalSpace M''
inst_10 : ChartedSpace H' M''
s : Set M
inst_11 : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : M''
f : M → M''
hf : ContinuousOn f s
z : M
hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source
apply : f ⁻¹' (extChartAt I' y).source ∈ nhdsWithin z s
⊢ UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' y).source) z

Tactic:
apply (hs z hz.1).inter'

Premises used: UniqueMDiffWithinAt.inter', And.left
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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_8
inst_9 : TopologicalSpace M''
inst_10 : ChartedSpace H' M''
s : Set M
inst_11 : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : M''
f : M → M''
hf : ContinuousOn f s
z : M
hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source
apply : (extChartAt I' y).source ∈ nhds (f z)
⊢ f ⁻¹' (extChartAt I' y).source ∈ nhdsWithin z s

Tactic:
apply (hf z hz.1).preimage_mem_nhdsWithin

Premises used: ContinuousWithinAt.preimage_mem_nhdsWithin, And.left
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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_8
inst_9 : TopologicalSpace M''
inst_10 : ChartedSpace H' M''
s : Set M
inst_11 : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : M''
f : M → M''
hf : ContinuousOn f s
z : M
hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source
⊢ (extChartAt I' y).source ∈ nhds (f z)

Tactic:
(isOpen_extChartAt_source y).mem_nhds hz.2

Premises used: isOpen_extChartAt_source, And.right, IsOpen.mem_nhds