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
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst_4] ((extChartAt I x).source ∩ (↑(extChartAt I x) : M → E) ⁻¹' s)

Tactic:
isOpen_extChartAt_preimage' x hs

Premises used: isOpen_extChartAt_preimage'
-- 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
inst_5 : ChartedSpace H M
x : M
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst_4] ((extChartAt I x).source ∩ (↑(extChartAt I x) : M → E) ⁻¹' s)

Tactic:
exact isOpen_extChartAt_preimage' x hs

Premises used: isOpen_extChartAt_preimage'
-- 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
s : Set M
inst_5 : ChartedSpace H M
x y : M
hy rwa rwa₁ rwa₂ rwa₃ : y ∈ (extChartAt I x).source
⊢ y ∈ (toPartialEquiv (chartAt H x)).source

Tactic:
rwa [← extChartAt_source I]

Premises used: extChartAt_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
s : Set M
inst_5 : ChartedSpace H M
x : M
⊢ map (↑(extChartAt I x) : M → E) (𝓝[s] x) =
    𝓝[(↑(extChartAt I x) : M → E) '' ((extChartAt I x).source ∩ s)] (↑(extChartAt I x) : M → E) x

Tactic:
map_extChartAt_nhdsWithin_eq_image' (mem_extChartAt_source x)

Premises used: mem_extChartAt_source, map_extChartAt_nhdsWithin_eq_image'
-- 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
s : Set M
inst_5 : ChartedSpace H M
x : M
⊢ map (↑(extChartAt I x) : M → E) (𝓝[s] x) =
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
map_extChartAt_nhdsWithin' (mem_extChartAt_source x)

Premises used: map_extChartAt_nhdsWithin', mem_extChartAt_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
s : Set M
inst_5 : ChartedSpace H M
x : M
⊢ map (↑(extChartAt I x).symm : E → M)
      (𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x) =
    𝓝[s] x

Tactic:
map_extChartAt_symm_nhdsWithin' (mem_extChartAt_source x)

Premises used: map_extChartAt_symm_nhdsWithin', mem_extChartAt_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
inst_5 : ChartedSpace H M
x : M
⊢ map (↑(extChartAt I x).symm : E → M) (𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x) = 𝓝 x

Tactic:
map_extChartAt_symm_nhdsWithin_range' (mem_extChartAt_source x)

Premises used: map_extChartAt_symm_nhdsWithin_range', mem_extChartAt_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
inst_5 : ChartedSpace H M
s : Set E
x x' : M
hx : x' ∈ (extChartAt I x).source
hs : s ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x'
⊢ x' ∈ (toPartialEquiv (chartAt H x)).source

Tactic:
simpa using hx
-- 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
s t : Set M
inst_5 : ChartedSpace H M
x x' : M
h : x' ∈ (extChartAt I x).source
ht : t ∈ 𝓝[s] x'
rwa :
  ∀
    (ht :
      t ∈
        map (↑(extChartAt I x).symm : E → M)
          (𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x')),
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
      𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x'
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (ht :
      (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
        𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x'),
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
      𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x'
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x'

Tactic:
rwa [← map_extChartAt_symm_nhdsWithin' h, mem_map] at ht

Premises used: map_extChartAt_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
I : ModelWithCorners 𝕜 E H
s t : Set M
inst_5 : ChartedSpace H M
x : M
ht : t ∈ 𝓝[s] x
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
extChartAt_preimage_mem_nhdsWithin' (mem_extChartAt_source x) ht

Premises used: extChartAt_preimage_mem_nhdsWithin', mem_extChartAt_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
t : Set M
inst_5 : ChartedSpace H M
x x' : M
h : x' ∈ (extChartAt I x).source
ht : t ∈ 𝓝 x'
rwa rwa₁ rwa₂ rwa₃ : x' ∈ (extChartAt I x).source
⊢ x' ∈ (toPartialEquiv (chartAt H x)).source

Tactic:
rwa [← extChartAt_source I]

Premises used: extChartAt_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
t : Set M
inst_5 : ChartedSpace H M
x : M
ht : t ∈ 𝓝 x
apply : t ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)

Tactic:
apply (continuousAt_extChartAt_symm x).preimage_mem_nhds

Premises used: ContinuousAt.preimage_mem_nhds, continuousAt_extChartAt_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
t : Set M
inst_5 : ChartedSpace H M
x : M
ht rwa rwa₁ rwa₂ rwa₃ : t ∈ 𝓝 x
⊢ t ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))

Tactic:
rwa [(extChartAt I x).left_inv (mem_extChartAt_source _)]

Premises used: extChartAt, mem_extChartAt_source, PartialEquiv.left_inv
-- 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
s t : Set M
inst_5 : ChartedSpace H M
x : M
h h₁ h₂ h₃ :
  ∀ (my_y : E),
    my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E) ↔
      my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' t
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E) =
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑(extChartAt I x).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
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
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
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
rw : f ⁻¹' (extChartAt I' (f x)).source ∈ 𝓝[s] x
⊢ 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
    𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)]
      (↑(extChartAt I x) : M → E) x

Tactic:
rw [← (extChartAt I x).image_source_inter_eq', ← map_extChartAt_nhdsWithin_eq_image,
    ← map_extChartAt_nhdsWithin, nhdsWithin_inter_of_mem']

Premises used: extChartAt, nhdsWithin_inter_of_mem', PartialEquiv.image_source_inter_eq', map_extChartAt_nhdsWithin, map_extChartAt_nhdsWithin_eq_image
-- 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
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
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
⊢ f ⁻¹' (extChartAt I' (f x)).source ∈ 𝓝[s] x

Tactic:
hc (extChartAt_source_mem_nhds _)

Premises used: Set.Mem, setOf, extChartAt_source_mem_nhds, Set.preimage
-- 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
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
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
⊢ f ⁻¹' (extChartAt I' (f x)).source ∈ 𝓝[s] x

Tactic:
exact hc (extChartAt_source_mem_nhds _)

Premises used: extChartAt_source_mem_nhds
-- 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
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
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
rw :
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
    𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)]
      (↑(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).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq]

Premises used: nhdsWithin_eq_iff_eventuallyEq
-- 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
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
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
⊢ 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
    𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)]
      (↑(extChartAt I x) : M → E) x

Tactic:
hc.nhdsWithin_extChartAt_symm_preimage_inter_range

Premises used: ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range
-- 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
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
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
⊢ 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
    𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)]
      (↑(extChartAt I x) : M → E) x

Tactic:
exact hc.nhdsWithin_extChartAt_symm_preimage_inter_range

Premises used: ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range
-- 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
inst_5 : ChartedSpace H M
x x' : M
⊢ ((extChartAt I x').symm ≫ extChartAt I x).source =
    (↑I : H → E) '' (toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x') ≫ₕ chartAt H x)).source

Tactic:
I.extendCoordChange_source

Premises used: extChartAt, 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
inst_6 : IsManifold I n M
x x' : M
⊢ ContDiffOn 𝕜 n ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x').symm : E → M))
    ((extChartAt I x').symm ≫ extChartAt I x).source

Tactic:
I.contDiffOn_extendCoordChange (chart_mem_maximalAtlas x') (chart_mem_maximalAtlas x)

Premises used: extChartAt, IsManifold.chart_mem_maximalAtlas, ModelWithCorners.contDiffOn_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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
inst_6 : IsManifold I n M
x x' : M
y : E
hy : y ∈ ((extChartAt I x').symm ≫ extChartAt I x).source
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x').symm : E → M)) (range (↑I : H → E)) y

Tactic:
I.contDiffWithinAt_extendCoordChange (chart_mem_maximalAtlas x') (chart_mem_maximalAtlas x) hy

Premises used: ModelWithCorners.contDiffWithinAt_extendCoordChange, IsManifold.chart_mem_maximalAtlas
-- 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
inst_5 : ChartedSpace H M
x : M
y : E
h : y ∈ (extChartAt I x).target
⊢ writtenInExtChartAt I I x (↑(chartAt H x) : M → H) y = y

Tactic:
simp_all only [mfld_simps]
-- 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
inst_5 : ChartedSpace H M
x : M
y : E
h : y ∈ (extChartAt I x).target
⊢ writtenInExtChartAt I I ((↑(chartAt H x) : M → H) x) (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) y = y

Tactic:
simp_all only [mfld_simps]
-- 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
inst_5 : ChartedSpace H M
x : M
y : E
h : y ∈ (extChartAt I x).target
⊢ writtenInExtChartAt I 𝓘(𝕜, E) x (↑(extChartAt I x) : M → E) y = y

Tactic:
simp_all only [mfld_simps]
-- 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
inst_5 : ChartedSpace H M
x : M
y : E
h : y ∈ (extChartAt I x).target
⊢ writtenInExtChartAt 𝓘(𝕜, E) I ((↑(extChartAt I x) : M → E) x) (↑(extChartAt I x).symm : E → M) y = y

Tactic:
simp_all only [mfld_simps]
-- 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
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
x : M
f : M → M'
x' : E
hx' : x' ∈ (extChartAt I x).target ∩ f ∘ (↑(extChartAt I x).symm : E → M) ⁻¹' (extChartAt I' (f x)).source
⊢ f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) x')) ∈
    (toPartialEquiv (chartAt H' (f x))).source

Tactic:
simpa using hx'.2

Premises used: And.right
-- 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
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
x : M
f : M → M'
x' : E
hx' : x' ∈ (extChartAt I x).target ∩ f ∘ (↑(extChartAt I x).symm : E → M) ⁻¹' (extChartAt I' (f x)).source
⊢ writtenInExtChartAt I I' x f x' ∈ (extChartAt I' (f x)).target

Tactic:
simpa using (chartAt H' (f x)).mapsTo (by simpa using hx'.2)

Premises used: chartAt, OpenPartialHomeomorph.mapsTo
-- 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
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
G : Type u_8
G' : Type u_9
F : Type u_10
F' : Type u_11
N : Type u_12
N' : Type u_13
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
inst_15 : TopologicalSpace G
inst_16 : TopologicalSpace N
inst_17 : TopologicalSpace G'
inst_18 : TopologicalSpace N'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
inst_19 : ChartedSpace G N
inst_20 : ChartedSpace G' N'
f : M → N
g : M' → N'
x : M
x' : M'
h :
  ∀ (p : E × E'),
    (writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) p).1 =
      (Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g) p).1
h₁ :
  ∀ (p : E × E'),
    (writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) p).2 =
      (Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g) p).2
⊢ writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) =
    Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g)

Tactic:
ext p
-- 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
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
G : Type u_8
G' : Type u_9
F : Type u_10
F' : Type u_11
N : Type u_12
N' : Type u_13
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
inst_15 : TopologicalSpace G
inst_16 : TopologicalSpace N
inst_17 : TopologicalSpace G'
inst_18 : TopologicalSpace N'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
inst_19 : ChartedSpace G N
inst_20 : ChartedSpace G' N'
f : M → N
g : M' → N'
x : M
x' : M'
p : E × E'
⊢ (writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) p).1 =
    (Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g) p).1

Tactic:
simp [writtenInExtChartAt, I.toPartialEquiv.prod_symm, (chartAt H x).toPartialEquiv.prod_symm]

Premises used: chartAt, ModelWithCorners.toPartialEquiv, PartialEquiv.prod_symm, writtenInExtChartAt, OpenPartialHomeomorph.toPartialEquiv