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'
f : M → M'
s : Set M
x : M
m_1 n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
h' : Eq (α := ℕ∞ω) (↑m : ℕ∞ω) ∞ → n = ω
this_1 : IsManifold I (↑m : ℕ∞ω) M
this : IsManifold I' (↑m : ℕ∞ω) M'
rcases :
  ∀ (t : Set M) (ht : t ∈ 𝓝[insert x s] x) (h't : ContMDiffOn I I' (↑m : ℕ∞ω) f t),
    ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' (↑m : ℕ∞ω) f (insert x s ∩ u)
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' (↑m : ℕ∞ω) f (insert x s ∩ u)

Tactic:
rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp)).1 (h.of_le hm) with ⟨t, ht, h't⟩

Premises used: contMDiffWithinAt_iff_contMDiffOn_nhds, ContMDiffWithinAt.of_le, 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 : Set M
x : M
m_1 n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
h' : Eq (α := ℕ∞ω) (↑m : ℕ∞ω) ∞ → n = ω
this_1 : IsManifold I (↑m : ℕ∞ω) M
this : IsManifold I' (↑m : ℕ∞ω) M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' (↑m : ℕ∞ω) f t
rcases :
  ∀ (u : Set M) (u_open : IsOpen[inst_4] u) (xu : x ∈ u) (hu : u ∩ insert x s ⊆ t),
    ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' (↑m : ℕ∞ω) f (insert x s ∩ u)
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' (↑m : ℕ∞ω) f (insert x s ∩ u)

Tactic:
rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩

Premises used: mem_nhdsWithin, 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 : Set M
x : M
m_1 n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
h' : Eq (α := ℕ∞ω) (↑m : ℕ∞ω) ∞ → n = ω
this_1 : IsManifold I (↑m : ℕ∞ω) M
this : IsManifold I' (↑m : ℕ∞ω) M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' (↑m : ℕ∞ω) f t
u : Set M
u_open : IsOpen[inst_4] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ t
⊢ insert x s ∩ u ⊆ t

Tactic:
rw [inter_comm] at hu

Premises used: Set.inter_comm
-- 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
m_1 n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
h' : Eq (α := ℕ∞ω) (↑m : ℕ∞ω) ∞ → n = ω
this_1 : IsManifold I (↑m : ℕ∞ω) M
this : IsManifold I' (↑m : ℕ∞ω) M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' (↑m : ℕ∞ω) f t
u : Set M
u_open : IsOpen[inst_4] u
xu : x ∈ u
hu : insert x s ∩ u ⊆ t
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' (↑m : ℕ∞ω) f (insert x s ∩ u)

Tactic:
⟨u, u_open, xu, h't.mono hu⟩

Premises used: ContMDiffOn.mono, And.intro, Exists.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 : Set M
x : M
m_1 n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
m : ℕ
hm : (↑m : ℕ∞ω) ≤ n
h' : Eq (α := ℕ∞ω) (↑m : ℕ∞ω) ∞ → n = ω
this_1 : IsManifold I (↑m : ℕ∞ω) M
this : IsManifold I' (↑m : ℕ∞ω) M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' (↑m : ℕ∞ω) f t
u : Set M
u_open : IsOpen[inst_4] u
xu : x ∈ u
hu : insert x s ∩ u ⊆ t
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' (↑m : ℕ∞ω) f (insert x s ∩ u)

Tactic:
exact ⟨u, u_open, xu, h't.mono hu⟩
-- 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
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ω ≤ n
h' : Eq (α := ℕ∞ω) ω ∞ → n = ω
this_1 : IsManifold I ω M
this : IsManifold I' ω M'
⊢ Ne (α := ℕ∞ω) ω ∞

Tactic:
simp
-- 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
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ω ≤ n
h' : Eq (α := ℕ∞ω) ω ∞ → n = ω
this_1 : IsManifold I ω M
this : IsManifold I' ω M'
rcases :
  ∀ (t : Set M) (ht : t ∈ 𝓝[insert x s] x) (h't : ContMDiffOn I I' ω f t),
    ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ω f (insert x s ∩ u)
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ω f (insert x s ∩ u)

Tactic:
rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp)).1 (h.of_le hm) with ⟨t, ht, h't⟩

Premises used: contMDiffWithinAt_iff_contMDiffOn_nhds, ContMDiffWithinAt.of_le, 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 : Set M
x : M
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ω ≤ n
h' : Eq (α := ℕ∞ω) ω ∞ → n = ω
this_1 : IsManifold I ω M
this : IsManifold I' ω M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' ω f t
rcases :
  ∀ (u : Set M) (u_open : IsOpen[inst_4] u) (xu : x ∈ u) (hu : u ∩ insert x s ⊆ t),
    ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ω f (insert x s ∩ u)
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ω f (insert x s ∩ u)

Tactic:
rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩

Premises used: mem_nhdsWithin, 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 : Set M
x : M
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ω ≤ n
h' : Eq (α := ℕ∞ω) ω ∞ → n = ω
this_1 : IsManifold I ω M
this : IsManifold I' ω M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' ω f t
u : Set M
u_open : IsOpen[inst_4] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ t
⊢ insert x s ∩ u ⊆ t

Tactic:
rw [inter_comm] at hu

Premises used: Set.inter_comm
-- 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
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ω ≤ n
h' : Eq (α := ℕ∞ω) ω ∞ → n = ω
this_1 : IsManifold I ω M
this : IsManifold I' ω M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' ω f t
u : Set M
u_open : IsOpen[inst_4] u
xu : x ∈ u
hu : insert x s ∩ u ⊆ t
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ω f (insert x s ∩ u)

Tactic:
⟨u, u_open, xu, h't.mono hu⟩

Premises used: ContMDiffOn.mono, And.intro, Exists.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 : Set M
x : M
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ω ≤ n
h' : Eq (α := ℕ∞ω) ω ∞ → n = ω
this_1 : IsManifold I ω M
this : IsManifold I' ω M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' ω f t
u : Set M
u_open : IsOpen[inst_4] u
xu : x ∈ u
hu : insert x s ∩ u ⊆ t
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ω f (insert x s ∩ u)

Tactic:
exact ⟨u, u_open, xu, h't.mono hu⟩
-- 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
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ∞ ≤ n
h' : Eq (α := ℕ∞ω) ∞ ∞ → n = ω
this_1 : IsManifold I ∞ M
this : IsManifold I' ∞ M'
⊢ n ≠ ∞

Tactic:
simp [h']
-- 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
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ∞ ≤ n
h' : Eq (α := ℕ∞ω) ∞ ∞ → n = ω
this_1 : IsManifold I ∞ M
this : IsManifold I' ∞ M'
rcases :
  ∀ (t : Set M) (ht : t ∈ 𝓝[insert x s] x) (h't : ContMDiffOn I I' n f t),
    ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)

Tactic:
rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp [h'])).1 h with ⟨t, ht, h't⟩

Premises used: contMDiffWithinAt_iff_contMDiffOn_nhds, 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 : Set M
x : M
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ∞ ≤ n
h' : Eq (α := ℕ∞ω) ∞ ∞ → n = ω
this_1 : IsManifold I ∞ M
this : IsManifold I' ∞ M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' n f t
rcases :
  ∀ (u : Set M) (u_open : IsOpen[inst_4] u) (xu : x ∈ u) (hu : u ∩ insert x s ⊆ t),
    ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)

Tactic:
rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩

Premises used: mem_nhdsWithin, 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 : Set M
x : M
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ∞ ≤ n
h' : Eq (α := ℕ∞ω) ∞ ∞ → n = ω
this_1 : IsManifold I ∞ M
this : IsManifold I' ∞ M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' n f t
u : Set M
u_open : IsOpen[inst_4] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ t
⊢ insert x s ∩ u ⊆ t

Tactic:
rw [inter_comm] at hu

Premises used: Set.inter_comm
-- 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
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ∞ ≤ n
h' : Eq (α := ℕ∞ω) ∞ ∞ → n = ω
this_1 : IsManifold I ∞ M
this : IsManifold I' ∞ M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' n f t
u : Set M
u_open : IsOpen[inst_4] u
xu : x ∈ u
hu : insert x s ∩ u ⊆ t
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)

Tactic:
⟨u, u_open, xu, (h't.mono hu).of_le hm⟩

Premises used: ContMDiffOn.of_le, ContMDiffOn.mono, And.intro, Exists.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 : Set M
x : M
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ∞ ≤ n
h' : Eq (α := ℕ∞ω) ∞ ∞ → n = ω
this_1 : IsManifold I ∞ M
this : IsManifold I' ∞ M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' n f t
u : Set M
u_open : IsOpen[inst_4] u
xu : x ∈ u
hu : insert x s ∩ u ⊆ t
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)

Tactic:
exact ⟨u, u_open, xu, (h't.mono hu).of_le hm⟩
-- 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
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hm : m ≤ n
h' : m = ∞ → n = ω
h : ContMDiffWithinAt I I' n f s x
this_1 : IsManifold I m M
this : IsManifold I' m M'
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' m f (insert x s ∩ u)

Tactic:
match m with
  | (m : ℕ) | ω =>
    rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp)).1 (h.of_le hm) with ⟨t, ht, h't⟩
    rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩
    rw [inter_comm] at hu
    exact ⟨u, u_open, xu, h't.mono hu⟩
  | ∞ =>
    rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp [h'])).1 h with ⟨t, ht, h't⟩
    rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩
    rw [inter_comm] at hu
    exact ⟨u, u_open, xu, (h't.mono hu).of_le hm⟩
-- 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
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hm : m ≤ n
h' : m = ∞ → n = ω
h : ContMDiffWithinAt I I' n f s x
let :
  ∀ (_u : Set M) (uo : IsOpen[inst_4] _u) (xu : x ∈ _u) (h : ContMDiffOn I I' m f (insert x s ∩ _u)),
    ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContMDiffOn I I' m f u
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContMDiffOn I I' m f u

Tactic:
let ⟨_u, uo, xu, h⟩ := h.contMDiffOn' hm h'
-- 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
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hm : m ≤ n
h' : m = ∞ → n = ω
h_1 : ContMDiffWithinAt I I' n f s x
_u : Set M
uo : IsOpen[inst_4] _u
xu : x ∈ _u
h : ContMDiffOn I I' m f (insert x s ∩ _u)
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContMDiffOn I I' m f u

Tactic:
⟨_, inter_mem_nhdsWithin _ (uo.mem_nhds xu), inter_subset_left, h⟩

Premises used: inter_mem_nhdsWithin, Set.inter_subset_left, And.intro, IsOpen.mem_nhds, Exists.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 : Set M
x : M
m n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hm : m ≤ n
h' : m = ∞ → n = ω
h_1 : ContMDiffWithinAt I I' n f s x
_u : Set M
uo : IsOpen[inst_4] _u
xu : x ∈ _u
h : ContMDiffOn I I' m f (insert x s ∩ _u)
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContMDiffOn I I' m f u

Tactic:
exact ⟨_, inter_mem_nhdsWithin _ (uo.mem_nhds xu), inter_subset_left, h⟩
-- 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'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
⊢ ContMDiffAt I I' n f x ↔ ∃ u ∈ 𝓝 x, ContMDiffOn I I' n f u

Tactic:
simp [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_contMDiffOn_nhds hn, nhdsWithin_univ]

Premises used: nhdsWithin_univ, contMDiffWithinAt_iff_contMDiffOn_nhds, contMDiffWithinAt_univ
-- 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'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hn : n ≠ ∞
⊢ ContMDiffAt I I' n f x ↔ ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'

Tactic:
⟨?_, fun h => h.self_of_nhds⟩

Premises used: Filter.Eventually.self_of_nhds, Iff.intro