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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
e : PartialEquiv M E := f.extend I
⊢ map (↑e : M → E) (𝓝[s] y) = map (↑e : M → E) (𝓝[e.source ∩ s] y)

Tactic:
congr_arg (map e) (nhdsWithin_inter_of_mem (extend_source_mem_nhdsWithin f hy)).symm

Premises used: Filter.map, nhdsWithin_inter_of_mem, congr_arg, OpenPartialHomeomorph.extend_source_mem_nhdsWithin, PartialEquiv.toFun, Eq.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
s : Set M
y : M
hy : y ∈ f.source
e : PartialEquiv M E := f.extend I
rwa rwa₁ rwa₂ rwa₃ : y ∈ f.source
⊢ y ∈ (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 : Set M
y : M
hy : y ∈ f.source
e : PartialEquiv M E := f.extend I
⊢ map (↑e : M → E) (𝓝[s] y) = 𝓝[(↑e : M → E) '' (e.source ∩ s)] (↑e : M → E) y

Tactic:
calc
    map e (𝓝[s] y) = map e (𝓝[e.source ∩ s] y) :=
      congr_arg (map e) (nhdsWithin_inter_of_mem (extend_source_mem_nhdsWithin f hy)).symm
    _ = 𝓝[e '' (e.source ∩ s)] e y :=
      ((f.extend I).leftInvOn.mono inter_subset_left).map_nhdsWithin_eq
        ((f.extend I).left_inv <| by rwa [f.extend_source])
        (continuousAt_extend_symm f hy).continuousWithinAt
        (continuousAt_extend f hy).continuousWithinAt

Premises used: Filter.map, nhdsWithin, ContinuousAt.continuousWithinAt, Set.LeftInvOn.map_nhdsWithin_eq, OpenPartialHomeomorph.continuousAt_extend, Set.inter_subset_left, nhdsWithin_inter_of_mem, Set.LeftInvOn.mono, Inter.inter, congr_arg, OpenPartialHomeomorph.continuousAt_extend_symm, PartialEquiv.source, PartialEquiv.leftInvOn, OpenPartialHomeomorph.extend_source_mem_nhdsWithin, PartialEquiv.left_inv, PartialEquiv.toFun, Eq.symm, 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
s : Set M
y : M
hy : y ∈ f.source
hs : s ⊆ f.source
rw : s ⊆ (f.extend I).source
⊢ map (↑(f.extend I) : M → E) (𝓝[s] y) = 𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) y

Tactic:
rw [map_extend_nhdsWithin_eq_image _ hy, inter_eq_self_of_subset_right]

Premises used: OpenPartialHomeomorph.map_extend_nhdsWithin_eq_image, Set.inter_eq_self_of_subset_right
-- 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
y : M
hy : y ∈ f.source
hs rwa rwa₁ rwa₂ rwa₃ : s ⊆ f.source
⊢ s ⊆ (f.extend I).source

Tactic:
rwa [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 : Set M
y : M
hy : y ∈ f.source
rw :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y
rw₁ :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y ⊓ 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y
rw₂ :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y ⊓ 𝓝[(f.extend I).target] (↑(f.extend I) : M → E) y
rw₃ :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ (f.extend I).target] (↑(f.extend I) : M → E) y
rw₄ :
  𝓝[(f.extend I).target ∩ (↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ (f.extend I).target] (↑(f.extend I) : M → E) y
rw₅ rw₆ :
  𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ (f.extend I).target] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ (f.extend I).target] (↑(f.extend I) : M → E) y
⊢ map (↑(f.extend I) : M → E) (𝓝[s] y) =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y

Tactic:
rw [map_extend_nhdsWithin_eq_image f hy, nhdsWithin_inter, ←
    nhdsWithin_extend_target_eq _ hy, ← nhdsWithin_inter, (f.extend I).image_source_inter_eq',
    inter_comm]

Premises used: OpenPartialHomeomorph.map_extend_nhdsWithin_eq_image, Set.inter_comm, PartialEquiv.image_source_inter_eq', nhdsWithin_inter, OpenPartialHomeomorph.nhdsWithin_extend_target_eq, 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
s : Set M
y : M
hy : y ∈ f.source
rw : (↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) =ᶠ[𝓝[s] y] id
⊢ map (↑(f.extend I).symm : E → M)
      (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y) =
    𝓝[s] y

Tactic:
rw [← map_extend_nhdsWithin f hy, map_map, Filter.map_congr, map_id]

Premises used: Filter.map_congr, Filter.map_map, OpenPartialHomeomorph.map_extend_nhdsWithin, Filter.map_id
-- 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
y : M
hy : y ∈ f.source
⊢ (↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) =ᶠ[𝓝[s] y] id

Tactic:
(f.extend I).leftInvOn.eqOn.eventuallyEq_of_mem (extend_source_mem_nhdsWithin _ hy)

Premises used: Set.LeftInvOn.eqOn, Set.EqOn.eventuallyEq_of_mem, PartialEquiv.leftInvOn, OpenPartialHomeomorph.extend_source_mem_nhdsWithin, 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
s : Set M
y : M
hy : y ∈ f.source
⊢ (↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) =ᶠ[𝓝[s] y] id

Tactic:
exact (f.extend I).leftInvOn.eqOn.eventuallyEq_of_mem (extend_source_mem_nhdsWithin _ hy)

Premises used: Set.LeftInvOn.eqOn, Set.EqOn.eventuallyEq_of_mem, PartialEquiv.leftInvOn, OpenPartialHomeomorph.extend_source_mem_nhdsWithin, 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
y : M
hy : y ∈ f.source
rw : map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) = 𝓝[univ] y
rw₁ :
  map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) =
    map (↑(f.extend I).symm : E → M)
      (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
rw₂ :
  map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) =
    map (↑(f.extend I).symm : E → M) (𝓝[univ ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
rw₃ rw₄ :
  map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) =
    map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y)
⊢ map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) = 𝓝 y

Tactic:
rw [← nhdsWithin_univ, ← map_extend_symm_nhdsWithin f (I := I) hy, preimage_univ, univ_inter]

Premises used: nhdsWithin_univ, OpenPartialHomeomorph.map_extend_symm_nhdsWithin, Set.univ_inter, Set.preimage_univ
-- 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
α : Type u_8
l : Filter α
g : α → M
hg : ∀ᶠ (z : α) in l, g z ∈ f.source
y : M
hy : y ∈ f.source
⊢ Tendsto ((↑(f.extend I) : M → E) ∘ g) l (𝓝 ((↑(f.extend I) : M → E) y)) ↔ Tendsto g l (𝓝 y)

Tactic:
⟨fun h u hu ↦ mem_map.2 ?_, (continuousAt_extend _ hy).tendsto.comp⟩

Premises used: Iff.mpr, OpenPartialHomeomorph.continuousAt_extend, ContinuousAt.tendsto, Iff.intro, Filter.Tendsto.comp, 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
α : Type u_8
l : Filter α
g : α → M
hg : ∀ᶠ (z : α) in l, g z ∈ f.source
y : M
hy : y ∈ f.source
refine :
  ∀ (h : Tendsto ((↑(f.extend I) : M → E) ∘ g) l (𝓝 ((↑(f.extend I) : M → E) y))) (u : Set M) (hu : u ∈ 𝓝 y),
    g ⁻¹' u ∈ l
⊢ Tendsto ((↑(f.extend I) : M → E) ∘ g) l (𝓝 ((↑(f.extend I) : M → E) y)) ↔ Tendsto g l (𝓝 y)

Tactic:
refine ⟨fun h u hu ↦ mem_map.2 ?_, (continuousAt_extend _ hy).tendsto.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
α : Type u_8
l : Filter α
g : α → M
hg : ∀ᶠ (z : α) in l, g z ∈ f.source
y : M
hy : y ∈ f.source
h : Tendsto ((↑(f.extend I) : M → E) ∘ g) l (𝓝 ((↑(f.extend I) : M → E) y))
u : Set M
hu : u ∈ 𝓝 y
⊢ Tendsto ((↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) ∘ g) l
    (𝓝 ((↑(f.extend I).symm : E → M) ((↑(f.extend I) : M → E) y)))

Tactic:
have := (f.continuousAt_extend_symm hy).tendsto.comp h
-- 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
α : Type u_8
l : Filter α
g : α → M
hg : ∀ᶠ (z : α) in l, g z ∈ f.source
y : M
hy : y ∈ f.source
h : Tendsto ((↑(f.extend I) : M → E) ∘ g) l (𝓝 ((↑(f.extend I) : M → E) y))
u : Set M
hu : u ∈ 𝓝 y
this :
  Tendsto ((↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) ∘ g) l
    (𝓝 ((↑(f.extend I).symm : E → M) ((↑(f.extend I) : M → E) y)))
⊢ Tendsto ((↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) ∘ g) l (𝓝 y)

Tactic:
rw [extend_left_inv _ hy] at this

Premises used: OpenPartialHomeomorph.extend_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
α : Type u_8
l : Filter α
g : α → M
hg : ∀ᶠ (z : α) in l, g z ∈ f.source
y : M
hy : y ∈ f.source
h : Tendsto ((↑(f.extend I) : M → E) ∘ g) l (𝓝 ((↑(f.extend I) : M → E) y))
u : Set M
hu : u ∈ 𝓝 y
this : Tendsto ((↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) ∘ g) l (𝓝 y)
h₁ :
  ∀ (z : α) (hz : g z ∈ f.source) (hzu : z ∈ (↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) ∘ g ⁻¹' u),
    z ∈ g ⁻¹' u
⊢ g ⁻¹' u ∈ l

Tactic:
filter_upwards [hg, mem_map.1 (this hu)] with z hz hzu

Premises used: Iff.mp, 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
α : Type u_8
l : Filter α
g : α → M
hg : ∀ᶠ (z : α) in l, g z ∈ f.source
y : M
hy : y ∈ f.source
h : Tendsto ((↑(f.extend I) : M → E) ∘ g) l (𝓝 ((↑(f.extend I) : M → E) y))
u : Set M
hu : u ∈ 𝓝 y
this : Tendsto ((↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) ∘ g) l (𝓝 y)
z : α
hz : g z ∈ f.source
hzu : z ∈ (↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) ∘ g ⁻¹' u
⊢ z ∈ g ⁻¹' u

Tactic:
simpa only [(· ∘ ·), extend_left_inv _ hz, mem_preimage] using hzu

Premises used: Function.comp, OpenPartialHomeomorph.extend_left_inv, Set.mem_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
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'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
simp :
  Tendsto ((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M))
      (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
      (𝓝 ((↑(f'.extend I') : M' → E') (g ((↑(f.extend I).symm : E → M) ((↑(f.extend I) : M → E) y))))) ↔
    Tendsto g (𝓝[s] y) (𝓝 (g y))
⊢ Tendsto ((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M))
      (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
      (𝓝 (((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) y))) ↔
    Tendsto g (𝓝[s] y) (𝓝 (g y))

Tactic:
simp only [comp_apply]

Premises used: Function.comp_apply
-- 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'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
rw :
  ∀ᶠ (z : E) in 𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y,
    (g ∘ (↑(f.extend I).symm : E → M)) z ∈ f'.source
⊢ Tendsto ((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M))
      (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
      (𝓝 ((↑(f'.extend I') : M' → E') (g ((↑(f.extend I).symm : E → M) ((↑(f.extend I) : M → E) y))))) ↔
    Tendsto g (𝓝[s] y) (𝓝 (g y))

Tactic:
rw [extend_left_inv _ hy, f'.tendsto_extend_comp_iff _ hgy,
    ← f.map_extend_symm_nhdsWithin (I := I) hy, tendsto_map'_iff]

Premises used: OpenPartialHomeomorph.tendsto_extend_comp_iff, Filter.tendsto_map'_iff, OpenPartialHomeomorph.map_extend_symm_nhdsWithin, OpenPartialHomeomorph.extend_left_inv
-- 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'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
rw : ∀ᶠ (a : M) in 𝓝[s] y, (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) a) ∈ f'.source
⊢ ∀ᶠ (z : E) in 𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y,
    (g ∘ (↑(f.extend I).symm : E → M)) z ∈ f'.source

Tactic:
rw [← f.map_extend_nhdsWithin (I := I) hy, eventually_map]

Premises used: Filter.eventually_map, 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'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
h : ∀ (z : M) (hz : z ∈ s ∩ f.source), (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) z) ∈ f'.source
⊢ ∀ᶠ (a : M) in 𝓝[s] y, (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) a) ∈ f'.source

Tactic:
filter_upwards [inter_mem_nhdsWithin _ (f.open_source.mem_nhds hy)] with z hz

Premises used: inter_mem_nhdsWithin, 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
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'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
z : M
hz : z ∈ s ∩ f.source
h : g z ∈ f'.source
⊢ (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) z) ∈ f'.source

Tactic:
rw [comp_apply, extend_left_inv _ hz.2]

Premises used: OpenPartialHomeomorph.extend_left_inv, And.right, Function.comp_apply
-- 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'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
z : M
hz : z ∈ s ∩ f.source
⊢ g z ∈ f'.source

Tactic:
hmaps hz.1

Premises used: And.left
-- 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'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
z : M
hz : z ∈ s ∩ f.source
⊢ g z ∈ f'.source

Tactic:
exact hmaps hz.1

Premises used: And.left
-- 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
⊢ ContinuousOn ((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) '' s) ↔
    ContinuousOn g s

Tactic:
forall_mem_image.trans <| forall₂_congr fun x hx ↦ ?_

Premises used: forall₂_congr, Iff.trans, ContinuousOn, Set.forall_mem_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
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
refine :
  ∀ (x : M) (hx : x ∈ s),
    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
⊢ ContinuousOn ((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) '' s) ↔
    ContinuousOn g s

Tactic:
refine forall_mem_image.trans <| forall₂_congr fun x hx ↦ ?_

Premises used: forall₂_congr, Iff.trans, Set.forall_mem_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
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
⊢ 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:
(continuousWithinAt_congr_set ?_).trans
    (continuousWithinAt_writtenInExtend_iff _ (hs hx) (hmaps hx) hmaps)

Premises used: OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff, continuousWithinAt_congr_set, Iff.trans