awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
hs : s ⊆ f.source
hmaps : MapsTo g s f'.source
x : M
hx : x ∈ s
refine :
  (↑(f.extend I) : M → E) '' s =ᶠ[𝓝 ((↑(f.extend I) : M → E) x)] (↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
⊢ ContinuousWithinAt ((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) '' s)
      ((↑(f.extend I) : M → E) x) ↔
    ContinuousWithinAt g s x

Tactic:
refine (continuousWithinAt_congr_set ?_).trans
    (continuousWithinAt_writtenInExtend_iff _ (hs hx) (hmaps hx) hmaps)

Premises used: OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff, continuousWithinAt_congr_set, Iff.trans
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
hs : s ⊆ f.source
hmaps : MapsTo g s f'.source
x : M
hx : x ∈ s
hy hy₁ : x ∈ f.source
hs₁ : s ⊆ f.source
⊢ (↑(f.extend I) : M → E) '' s =ᶠ[𝓝 ((↑(f.extend I) : M → E) x)] (↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin_eq_image_of_subset,
    ← map_extend_nhdsWithin]

Premises used: OpenPartialHomeomorph.map_extend_nhdsWithin_eq_image_of_subset, nhdsWithin_eq_iff_eventuallyEq, OpenPartialHomeomorph.map_extend_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
hs : s ⊆ f.source
hmaps : MapsTo g s f'.source
x : M
hx : x ∈ s
⊢ x ∈ f.source

Tactic:
hs hx
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
hs : s ⊆ f.source
hmaps : MapsTo g s f'.source
x : M
hx : x ∈ s
⊢ s ⊆ f.source

Tactic:
hs
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
hs : s ⊆ f.source
hmaps : MapsTo g s f'.source
x : M
hx : x ∈ s
⊢ x ∈ f.source

Tactic:
exacts [hs hx, hs hx, hs]
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set E
x : M
hx : x ∈ f.source
hs : s ∈ 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x
rwa rwa₁ rwa₂ rwa₃ : ∀ (hs : s ∈ map (↑(f.extend I) : M → E) (𝓝 x)), (↑(f.extend I) : M → E) ⁻¹' s ∈ 𝓝 x
⊢ (↑(f.extend I) : M → E) ⁻¹' s ∈ 𝓝 x

Tactic:
rwa [← map_extend_nhds (I := I) f hx] at hs

Premises used: OpenPartialHomeomorph.map_extend_nhds
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝[s] x
rwa :
  ∀
    (ht :
      t ∈
        map (↑(f.extend I).symm : E → M)
          (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x)),
    (↑(f.extend I).symm : E → M) ⁻¹' t ∈
      𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (ht :
      (↑(f.extend I).symm : E → M) ⁻¹' t ∈
        𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x),
    (↑(f.extend I).symm : E → M) ⁻¹' t ∈
      𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x
⊢ (↑(f.extend I).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x

Tactic:
rwa [← map_extend_symm_nhdsWithin f (I := I) h, mem_map] at ht

Premises used: OpenPartialHomeomorph.map_extend_symm_nhdsWithin, Filter.mem_map
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
apply : t ∈ 𝓝 ((↑(f.extend I).symm : E → M) ((↑(f.extend I) : M → E) x))
⊢ (↑(f.extend I).symm : E → M) ⁻¹' t ∈ 𝓝 ((↑(f.extend I) : M → E) x)

Tactic:
apply (continuousAt_extend_symm f h).preimage_mem_nhds

Premises used: ContinuousAt.preimage_mem_nhds, OpenPartialHomeomorph.continuousAt_extend_symm
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
rwa : x ∈ (f.extend I).source
⊢ t ∈ 𝓝 ((↑(f.extend I).symm : E → M) ((↑(f.extend I) : M → E) x))

Tactic:
rwa [(f.extend I).left_inv]

Premises used: PartialEquiv.left_inv, OpenPartialHomeomorph.extend
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
rwa rwa₁ rwa₂ rwa₃ : x ∈ f.source
⊢ x ∈ (f.extend I).source

Tactic:
rwa [f.extend_source]

Premises used: OpenPartialHomeomorph.extend_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s t : Set M
h h₁ h₂ h₃ :
  ∀ (my_y : E),
    my_y ∈ (↑(f.extend I).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E) ↔
      my_y ∈ (↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑(f.extend I).symm : E → M) ⁻¹' t
⊢ (↑(f.extend I).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E) =
    (↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑(f.extend I).symm : E → M) ⁻¹' t

Tactic:
mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
x : M
hs : s ⊆ f.source
hx : x ∈ f.source
rw :
  𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x =
    𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) x
rw₁ : map (↑(f.extend I) : M → E) (𝓝[s] x) = 𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) x
rw₂ rw₃ :
  𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) x = 𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) x
⊢ (↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝 ((↑(f.extend I) : M → E) x)] (↑(f.extend I) : M → E) '' s

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin _ hx,
    map_extend_nhdsWithin_eq_image_of_subset _ hx hs]

Premises used: OpenPartialHomeomorph.map_extend_nhdsWithin_eq_image_of_subset, nhdsWithin_eq_iff_eventuallyEq, OpenPartialHomeomorph.map_extend_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
f' : OpenPartialHomeomorph M' H'
⊢ (f.prod f').extend (I.prod I') = (f.extend I).prod (f'.extend I')

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ Eq.{u_2 + 1} (α := PartialEquiv E E)
    (PartialEquiv.symm (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))
    (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e' e)

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
simp_rw :
  (↑I.symm : E → H) ⁻¹' e.target ∩ (↑(e.extend I).symm : E → M) ⁻¹' e'.source ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)
⊢ PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') =
    (↑I : H → E) '' (e.symm ≫ₕ e').source

Tactic:
simp_rw [extendCoordChange, PartialEquiv.trans_source, I.image_eq, e'.extend_source,
    PartialEquiv.symm_source, e.extend_target, inter_right_comm _ (range I)]

Premises used: PartialEquiv.trans_source, ModelWithCorners.image_eq, OpenPartialHomeomorph.extend_target, ModelWithCorners.toFun', PartialEquiv.symm_source, OpenPartialHomeomorph.extend_source, Set.inter_right_comm, Set.range, ModelWithCorners.extendCoordChange
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ (↑I.symm : E → H) ⁻¹' e.target ∩ (↑(e.extend I).symm : E → M) ⁻¹' e'.source ∩ range (↑I : H → E) =
    (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)

Tactic:
simp [Set.preimage_comp]

Premises used: Set.preimage_comp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ PartialEquiv.source (PartialEquiv.symm (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) =
    (↑I : H → E) '' (e.symm ≫ₕ e').symm.source

Tactic:
I.extendCoordChange_source

Premises used: ModelWithCorners.extendCoordChange_source, PartialEquiv.trans, PartialEquiv.symm, PartialEquiv.trans', OpenPartialHomeomorph.extend, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ PartialEquiv.source (PartialEquiv.symm (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) =
    (↑I : H → E) '' (e.symm ≫ₕ e').symm.source

Tactic:
exact I.extendCoordChange_source

Premises used: ModelWithCorners.extendCoordChange_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f f' : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
simp_rw : (↑(f.extend I) : M → E) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
simp_rw₁ :
  (fun (a : M) ↦ ((↑I : H → E) ∘ (↑f : M → H)) a) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
simp_rw₂ : (↑I : H → E) '' (↑f : M → H) '' (f.source ∩ f'.source) = (↑I : H → E) '' (f.symm ≫ₕ f').source
simp_rw₃ :
  (↑I : H → E) '' (↑f : M → H) '' (f.source ∩ f'.source) =
    (↑I : H → E) '' (↑f.symm.symm : M → H) '' (f.symm.target ∩ f'.source)
simp_rw₄ :
  (↑I : H → E) '' (↑f : M → H) '' (f.source ∩ f'.source) =
    (↑I : H → E) '' (fun (a : M) ↦ (↑f : M → H) a) '' (f.symm.target ∩ f'.source)
⊢ (↑(f.extend I) : M → E) '' (f.source ∩ f'.source) =
    PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) f f')

Tactic:
simp_rw [I.extendCoordChange_source, f.extend_coe, image_comp I f,
    OpenPartialHomeomorph.trans_source'', OpenPartialHomeomorph.symm_symm,
    OpenPartialHomeomorph.symm_target]

Premises used: ModelWithCorners.extendCoordChange_source, OpenPartialHomeomorph.trans_source'', OpenPartialHomeomorph.toFun', ModelWithCorners.toFun', OpenPartialHomeomorph.symm_target, OpenPartialHomeomorph.extend_coe, Set.image_comp, OpenPartialHomeomorph.symm_symm
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : E
hx : Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) x
rw : ∀ (hx : x ∈ (↑I : H → E) '' (e.symm ≫ₕ e').source), (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] x
⊢ PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') ∈ 𝓝[range (↑I : H → E)] x

Tactic:
rw [I.extendCoordChange_source] at hx ⊢

Premises used: ModelWithCorners.extendCoordChange_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : E
hx : x ∈ (↑I : H → E) '' (e.symm ≫ₕ e').source
obtain :
  ∀ (x : H) (hx : x ∈ (e.symm ≫ₕ e').source),
    (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) x
⊢ (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] x

Tactic:
obtain ⟨x, hx, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : H
hx : x ∈ (e.symm ≫ₕ e').source
⊢ (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) x

Tactic:
I.image_mem_nhdsWithin ?_

Premises used: ModelWithCorners.image_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : H
hx : x ∈ (e.symm ≫ₕ e').source
refine : (e.symm ≫ₕ e').source ∈ 𝓝 x
⊢ (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) x

Tactic:
refine I.image_mem_nhdsWithin ?_

Premises used: ModelWithCorners.image_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : H
hx : x ∈ (e.symm ≫ₕ e').source
⊢ (e.symm ≫ₕ e').source ∈ 𝓝 x

Tactic:
(OpenPartialHomeomorph.open_source _).mem_nhds hx

Premises used: OpenPartialHomeomorph.open_source, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : H
hx : x ∈ (e.symm ≫ₕ e').source
⊢ (e.symm ≫ₕ e').source ∈ 𝓝 x

Tactic:
exact (OpenPartialHomeomorph.open_source _).mem_nhds hx

Premises used: OpenPartialHomeomorph.open_source, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
hx :
  Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))
    ((↑(e.extend I) : M → E) x)
⊢ PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') ∈
    𝓝[range (↑I : H → E)] (↑(e.extend I) : M → E) x

Tactic:
apply extendCoordChange_source_mem_nhdsWithin

Premises used: ModelWithCorners.extendCoordChange_source_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
hx : (↑(e.extend I) : M → E) x ∈ (↑(e.extend I) : M → E) '' (e.source ∩ e'.source)
⊢ Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))
    ((↑(e.extend I) : M → E) x)

Tactic:
rw [← OpenPartialHomeomorph.extend_image_source_inter]

Premises used: OpenPartialHomeomorph.extend_image_source_inter
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
⊢ (↑(e.extend I) : M → E) x ∈ (↑(e.extend I) : M → E) '' (e.source ∩ e'.source)

Tactic:
mem_image_of_mem _ ⟨hxe, hxe'⟩

Premises used: Set.mem_image_of_mem, And.intro
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
⊢ (↑(e.extend I) : M → E) x ∈ (↑(e.extend I) : M → E) '' (e.source ∩ e'.source)

Tactic:
exact mem_image_of_mem _ ⟨hxe, hxe'⟩
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
rw : UniqueDiffOn 𝕜 ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))
⊢ UniqueDiffOn.{u_1, u_2} 𝕜 (E := E)
    (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))

Tactic:
rw [extendCoordChange_source, I.image_eq]

Premises used: ModelWithCorners.image_eq, ModelWithCorners.extendCoordChange_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ UniqueDiffOn 𝕜 ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))

Tactic:
I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source

Premises used: OpenPartialHomeomorph.open_source, ModelWithCorners.uniqueDiffOn_preimage, OpenPartialHomeomorph.isOpen_inter_preimage_symm
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ UniqueDiffOn 𝕜 ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))

Tactic:
exact I.uniqueDiffOn_preimage <| e.isOpen_inter_preimage_symm e'.open_source

Premises used: OpenPartialHomeomorph.open_source, ModelWithCorners.uniqueDiffOn_preimage, OpenPartialHomeomorph.isOpen_inter_preimage_symm
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
rw :
  UniqueDiffOn.{u_1, u_2} 𝕜 (E := E)
    (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e' e))
⊢ UniqueDiffOn.{u_1, u_2} 𝕜 (E := E)
    (PartialEquiv.target (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))

Tactic:
rw [← extendCoordChange_symm, PartialEquiv.symm_target]

Premises used: PartialEquiv.symm_target, ModelWithCorners.extendCoordChange_symm