awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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 ∈
    𝓝[(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 ⊆ (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)
refine_1 : (↑(extChartAt I x).symm : E → M) '' v ∈ 𝓝[s] x
⊢ ∃ u ∈ 𝓝[s] x, ContMDiffOn I I' n f u
have refine_2 : ContMDiffOn I I' n f ((↑(extChartAt I x).symm : E → M) '' v)
Tactic: refine ⟨(extChartAt I x).symm '' v, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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 ∈
    𝓝[(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 ⊆ (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)
⊢ (↑(extChartAt I x).symm : E → M) '' v ∈ 𝓝[s] x
have refine_1 : (↑(extChartAt I x).symm : E → M) '' v ∈
  map (↑(extChartAt I x).symm : E → M)
    (𝓝[(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 [← map_extChartAt_symm_nhdsWithin (I := I),
      h.1.nhdsWithin_extChartAt_symm_preimage_inter_range (I := I) (I' := I')]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (hypothesis)
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 ∈
    𝓝[(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 ⊆ (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)
⊢ ContMDiffOn I I' n f ((↑(extChartAt I x).symm : E → M) '' v)
have hv₁ : (↑(extChartAt I x).symm : E → M) '' v ⊆ (extChartAt I x).source
Tactic: have hv₁ : (extChartAt I x).symm '' v ⊆ (extChartAt I x).source :=
      image_subset_iff.2 fun y hy ↦ (extChartAt I x).map_target (hsub hy).1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (hypothesis)
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 ∈
    𝓝[(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 ⊆ (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)
hv₁ : (↑(extChartAt I x).symm : E → M) '' v ⊆ (extChartAt I x).source
⊢ ContMDiffOn I I' n f ((↑(extChartAt I x).symm : E → M) '' v)
have hv₂ : MapsTo f ((↑(extChartAt I x).symm : E → M) '' v) (extChartAt I' (f x)).source
Tactic: have hv₂ : MapsTo f ((extChartAt I x).symm '' v) (extChartAt I' (f x)).source := by
      rintro _ ⟨y, hy, rfl⟩
      exact (hsub hy).2.2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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 ∈
    𝓝[(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 ⊆ (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)
hv₁ : (↑(extChartAt I x).symm : E → M) '' v ⊆ (extChartAt I x).source
hv₂ : MapsTo f ((↑(extChartAt I x).symm : E → M) '' v) (extChartAt I' (f x)).source
⊢ ContMDiffOn I I' n f ((↑(extChartAt I x).symm : E → M) '' v)
have refine_2 : v ⊆ (extChartAt I x).target
Tactic: rwa [contMDiffOn_iff_of_subset_source' hv₁ hv₂, PartialEquiv.image_symm_image_of_subset_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (hypothesis)
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
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' m f (insert x s ∩ u)
have this : IsManifold I m M
Tactic: have : IsManifold I m M := .of_le hm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (hypothesis)
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 : IsManifold I m M
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' m f (insert x s ∩ u)
have this₁ : IsManifold I' m M'
Tactic: have : IsManifold I' m M' := .of_le hm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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'
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' (↑m : ℕ∞ω) f (insert x s ∩ u)
have 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)
Tactic: rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp)).1 (h.of_le hm) with ⟨t, ht, h't⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' (↑m : ℕ∞ω) f (insert x s ∩ u)
have 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)
Tactic: rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (hypothesis)
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
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' (↑m : ℕ∞ω) f (insert x s ∩ u)
have hu₁ : insert x s ∩ u ⊆ t
Tactic: rw [inter_comm] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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'
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ω f (insert x s ∩ u)
have 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)
Tactic: rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp)).1 (h.of_le hm) with ⟨t, ht, h't⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ω f (insert x s ∩ u)
have 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)
Tactic: rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (hypothesis)
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
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ω f (insert x s ∩ u)
have hu₁ : insert x s ∩ u ⊆ t
Tactic: rw [inter_comm] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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'
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)
have 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)
Tactic: rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp [h'])).1 h with ⟨t, ht, h't⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)
have 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)
Tactic: rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (hypothesis)
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
⊢ ∃ (u : Set M), IsOpen[inst_4] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)
have hu₁ : insert x s ∩ u ⊆ t
Tactic: rw [inter_comm] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContMDiffOn I I' m f u
have 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
Tactic: let ⟨_u, uo, xu, h⟩ := h.contMDiffOn' hm h'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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'
have refine : ContMDiffAt I I' n f x → ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'
Tactic: refine ⟨?_, fun h => h.self_of_nhds⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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'
have rw : (∃ u ∈ 𝓝 x, ContMDiffOn I I' n f u) → ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'
Tactic: rw [contMDiffAt_iff_contMDiffOn_nhds hn]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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 ≠ ∞
u : Set M
hu : u ∈ 𝓝 x
h : ContMDiffOn I I' n f u
⊢ ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' n f x'
have refine : ∀ (x' : M) (hx' : u ∈ 𝓝 x'), ContMDiffAt I I' n f x'
Tactic: refine (eventually_mem_nhds_iff.mpr hu).mono fun x' hx' => ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Defs (goal)
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 ≠ ∞
⊢ ContMDiffWithinAt I I' n f s x ↔ ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'
have refine : ContMDiffWithinAt I I' n f s x → ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'
Tactic: refine ⟨?_, fun h ↦ mem_of_mem_nhdsWithin (mem_insert x s) h⟩