awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hs : s ⊆ e.source
simp_rw :
  (∀ x ∈ s, ContMDiffWithinAt I I' n f s x) ↔
    ∀ ⦃x : M⦄,
      x ∈ s →
        ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)
          ((↑(e.extend I) : M → E) x)
⊢ ContMDiffOn I I' n f s ↔ ContMDiffOn 𝓘(𝕜, E) I' n (f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)

Tactic:
simp_rw [ContMDiffOn, Set.forall_mem_image]

Premises used: Set.forall_mem_image, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hs : s ⊆ e.source
⊢ (∀ x ∈ s, ContMDiffWithinAt I I' n f s x) ↔
    ∀ ⦃x : M⦄,
      x ∈ s →
        ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)
          ((↑(e.extend I) : M → E) x)

Tactic:
forall₂_congr fun x hx => ?_

Premises used: forall₂_congr
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hs : s ⊆ e.source
refine :
  ∀ (x : M) (hx : x ∈ s),
    ContMDiffWithinAt I I' n f s x ↔
      ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)
        ((↑(e.extend I) : M → E) x)
⊢ (∀ x ∈ s, ContMDiffWithinAt I I' n f s x) ↔
    ∀ ⦃x : M⦄,
      x ∈ s →
        ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)
          ((↑(e.extend I) : M → E) x)

Tactic:
refine forall₂_congr fun x hx => ?_

Premises used: forall₂_congr
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hs : s ⊆ e.source
x : M
hx : x ∈ s
rw :
  ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(e.extend I).symm : E → M))
      ((↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(e.extend I) : M → E) x) ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)
      ((↑(e.extend I) : M → E) x)
⊢ ContMDiffWithinAt I I' n f s x ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)
      ((↑(e.extend I) : M → E) x)

Tactic:
rw [contMDiffWithinAt_iff_source_of_mem_maximalAtlas he (hs hx)]

Premises used: contMDiffWithinAt_iff_source_of_mem_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hs : s ⊆ e.source
x : M
hx : x ∈ s
h :
  (↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝 ((↑(e.extend I) : M → E) x)] (↑(e.extend I) : M → E) '' s
⊢ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(e.extend I).symm : E → M))
      ((↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(e.extend I) : M → E) x) ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)
      ((↑(e.extend I) : M → E) x)

Tactic:
apply contMDiffWithinAt_congr_set

Premises used: contMDiffWithinAt_congr_set
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hs : s ⊆ e.source
x : M
hx : x ∈ s
⊢ (↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝 ((↑(e.extend I) : M → E) x)] (↑(e.extend I) : M → E) '' s

Tactic:
simp_rw [e.extend_symm_preimage_inter_range_eventuallyEq hs (hs hx)]

Premises used: OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
inr :
  ∀ (this : ∀ {s : Set M} (hxs : x ∈ s), ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u)
    (hxs : x ∉ s), ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u
wlog : ∀ {s : Set M} (hxs : x ∈ s), ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u
⊢ ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u

Tactic:
wlog hxs : x ∈ s generalizing s
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
this : ∀ {s : Set M} (hxs : x ∈ s), ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u
hxs : x ∉ s
inr : ContMDiffWithinAt I I' n f (insert x s) x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u
inr₁ : (∃ u ∈ 𝓝[insert x (insert x s)] x, ContMDiffOn I I' n f u) ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u
inr₂ inr₃ : (∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u) ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u
⊢ ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u

Tactic:
rw [← contMDiffWithinAt_insert_self, this (mem_insert _ _), insert_idem]

Premises used: contMDiffWithinAt_insert_self, Set.insert_idem, Set.mem_insert
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s_1 : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
rw : ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[s] x, ContMDiffOn I I' n f u
⊢ ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u

Tactic:
rw [insert_eq_of_mem hxs]

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s_1 : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
⊢ ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[s] x, ContMDiffOn I I' n f u

Tactic:
⟨fun h ↦ ?_, fun ⟨u, hmem, hu⟩ ↦
    (hu _ (mem_of_mem_nhdsWithin hxs hmem)).mono_of_mem_nhdsWithin hmem⟩

Premises used: ContMDiffWithinAt, _private.0.contMDiffWithinAt_iff_contMDiffOn_nhds.match_1, ContMDiffWithinAt.mono_of_mem_nhdsWithin, mem_of_mem_nhdsWithin, Iff.intro
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s_1 : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
refine : ∀ (h : ContMDiffWithinAt I I' n f s x), ∃ u ∈ 𝓝[s] x, ContMDiffOn I I' n f u
⊢ ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[s] x, ContMDiffOn I I' n f u

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨u, hmem, hu⟩ ↦
    (hu _ (mem_of_mem_nhdsWithin hxs hmem)).mono_of_mem_nhdsWithin hmem⟩
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s_1 : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
h : ContMDiffWithinAt I I' n f s x
⊢ n = ∞ → n = ω

Tactic:
simp [hn]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s_1 : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
h : ContMDiffWithinAt I I' n f s x
rcases :
  ∀ (v : Set E)
    (hmem :
      v ∈
        𝓝[insert ((↑(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)
    (hsub :
      v ⊆
        insert ((↑(extChartAt I x) : M → E) x)
          ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)))
    (hv : ContDiffOn 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) v),
    ∃ u ∈ 𝓝[s] x, ContMDiffOn I I' n f u
⊢ ∃ u ∈ 𝓝[s] x, ContMDiffOn I I' n f u

Tactic:
rcases (contMDiffWithinAt_iff'.1 h).2.contDiffOn le_rfl (by simp [hn]) with ⟨v, hmem, hsub, hv⟩

Premises used: le_rfl, ContDiffWithinAt.contDiffOn, contMDiffWithinAt_iff', And.right, Iff.mp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s_1 : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
h : ContMDiffWithinAt I I' n f s x
v : Set E
hmem :
  v ∈
    𝓝[insert ((↑(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
hsub :
  v ⊆
    insert ((↑(extChartAt I x) : M → E) x)
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
hv : ContDiffOn 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) v
rwa rwa₁ rwa₂ rwa₃ : x ∈ s
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) ∈ s

Tactic:
rwa [extChartAt_to_inv]

Premises used: extChartAt_to_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s_1 : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
h : ContMDiffWithinAt I I' n f s x
v : Set E
hmem :
  v ∈
    𝓝[insert ((↑(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
hsub :
  v ⊆
    insert ((↑(extChartAt I x) : M → E) x)
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
hv : ContDiffOn 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) v
rw : x ∈ f ⁻¹' (extChartAt I' (f x)).source
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) ∈ f ⁻¹' (extChartAt I' (f x)).source

Tactic:
rw [extChartAt_to_inv]

Premises used: extChartAt_to_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s_1 : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
h : ContMDiffWithinAt I I' n f s x
v : Set E
hmem :
  v ∈
    𝓝[insert ((↑(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
hsub :
  v ⊆
    insert ((↑(extChartAt I x) : M → E) x)
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
hv : ContDiffOn 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) v
⊢ x ∈ f ⁻¹' (extChartAt I' (f x)).source

Tactic:
apply mem_extChartAt_source

Premises used: mem_extChartAt_source
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s_1 : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
h : ContMDiffWithinAt I I' n f s x
v : Set E
hmem :
  v ∈
    𝓝[insert ((↑(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
hsub :
  v ⊆
    insert ((↑(extChartAt I x) : M → E) x)
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
hv : ContDiffOn 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) v
⊢ (↑(extChartAt I x) : M → E) x ∈
    (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)

Tactic:
have hxs' : extChartAt I x x ∈ (extChartAt I x).target ∩
      (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) :=
    ⟨(extChartAt I x).map_source (mem_extChartAt_source _), by rwa [extChartAt_to_inv], by
      rw [extChartAt_to_inv]; apply mem_extChartAt_source⟩
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s_1 : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
h : ContMDiffWithinAt I I' n f s x
v : Set E
hmem :
  v ∈
    𝓝[insert ((↑(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
hsub :
  v ⊆
    insert ((↑(extChartAt I x) : M → E) x)
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
hv : ContDiffOn 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) v
hxs' :
  (↑(extChartAt I x) : M → E) x ∈
    (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)
⊢ v ∈
    𝓝[(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 [insert_eq_of_mem hxs'] at hmem hsub

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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'
f : M → M'
s_1 : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
h : ContMDiffWithinAt I I' n f s x
v : Set E
hmem :
  v ∈
    𝓝[insert ((↑(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
hsub :
  v ⊆
    insert ((↑(extChartAt I x) : M → E) x)
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
hv : ContDiffOn 𝕜 n ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) v
hxs' :
  (↑(extChartAt I x) : M → E) x ∈
    (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)
hmem₁ :
  v ∈
    𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)]
      (↑(extChartAt I x) : M → E) x
⊢ v ⊆ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)

Tactic:
rw [insert_eq_of_mem hxs'] at hmem hsub

Premises used: Set.insert_eq_of_mem