awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I ∞ M
inst_9 : SigmaCompactSpace M
inst_10 : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst_6, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst_6] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun (x : M) ↦ {y : F | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∉ S
this : ∀ᶠ (y : M) in 𝓝 x, y ∉ S ∧ dist (f x) (f y) < ε y
hx' : f x = 0
⊢ ∀ᶠ (y : M) in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)

Tactic:
simpa [hx'] using this
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I ∞ M
inst_9 : SigmaCompactSpace M
inst_10 : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst_6, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst_6] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun (x : M) ↦ {y : F | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∉ S
this : ∀ᶠ (y : M) in 𝓝 x, y ∉ S ∧ dist (f x) (f y) < ε y
hx' : ¬f x = 0
⊢ ∀ᶠ (y : M) in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)

Tactic:
simpa [hx'] using this.and (f_cont.continuousAt.eventually_ne hx')

Premises used: Filter.Eventually.and, Continuous.continuousAt, ContinuousAt.eventually_ne
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I ∞ M
inst_9 : SigmaCompactSpace M
inst_10 : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst_6, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst_6] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun (x : M) ↦ {y : F | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∉ S
this : ∀ᶠ (y : M) in 𝓝 x, y ∉ S ∧ dist (f x) (f y) < ε y
⊢ ∀ᶠ (y : M) in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)

Tactic:
have : ∀ᶠ y in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0) := by
      by_cases hx' : f x = 0
      · simpa [hx'] using this
      · simpa [hx'] using this.and (f_cont.continuousAt.eventually_ne hx')
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I ∞ M
inst_9 : SigmaCompactSpace M
inst_10 : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst_6, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst_6] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun (x : M) ↦ {y : F | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∉ S
this_1 : ∀ᶠ (y : M) in 𝓝 x, y ∉ S ∧ dist (f x) (f y) < ε y
this : ∀ᶠ (y : M) in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)
y : M
hy :
  Membership.mem (γ := Set M) {x_1 : M | (fun (y : M) ↦ (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)) x_1} y
⊢ y ∈ S → (fun (x_1 : M) ↦ f x) y = f y

Tactic:
simp [hy.1.1]

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I ∞ M
inst_9 : SigmaCompactSpace M
inst_10 : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst_6, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst_6] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun (x : M) ↦ {y : F | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∉ S
this_1 : ∀ᶠ (y : M) in 𝓝 x, y ∉ S ∧ dist (f x) (f y) < ε y
this : ∀ᶠ (y : M) in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)
⊢ ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y

Tactic:
exact ⟨_, this, (fun _ ↦ f x), contMDiffOn_const, fun y hy ↦ ⟨hy.1.2, by simp [hy.1.1], hy.2⟩⟩
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I ∞ M
inst_9 : SigmaCompactSpace M
inst_10 : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst_6, _] ε
ε_pos : ∀ (x : M), 0 < ε x
obtain :
  ∀ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯) (g_approx : ∀ (x : M), dist ((g : (a : M) → F) x) (f x) < ε x)
    (g_supp : support.{u_4, u_2} (M := F) (⇑g : (a : M) → F) ⊆ support f),
    ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯),
      (∀ (x : M), dist ((g : (a : M) → F) x) (f x) < ε x) ∧ support.{u_4, u_2} (M := F) (⇑g : (a : M) → F) ⊆ support f
⊢ ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯),
    (∀ (x : M), dist ((g : (a : M) → F) x) (f x) < ε x) ∧ support.{u_4, u_2} (M := F) (⇑g : (a : M) → F) ⊆ support f

Tactic:
obtain ⟨g, g_approx, -, g_supp⟩ := f_cont.exists_contMDiff_approx_and_eqOn I n ε_cont ε_pos
    isClosed_empty mem_nhdsSet_empty contMDiffOn_empty

Premises used: mem_nhdsSet_empty, isClosed_empty, Continuous.exists_contMDiff_approx_and_eqOn, contMDiffOn_empty
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I ∞ M
inst_9 : SigmaCompactSpace M
inst_10 : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst_6, _] ε
ε_pos : ∀ (x : M), 0 < ε x
g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯
g_approx : ∀ (x : M), dist ((g : (a : M) → F) x) (f x) < ε x
g_supp : support.{u_4, u_2} (M := F) (⇑g : (a : M) → F) ⊆ support f
⊢ ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯),
    (∀ (x : M), dist ((g : (a : M) → F) x) (f x) < ε x) ∧ support.{u_4, u_2} (M := F) (⇑g : (a : M) → F) ⊆ support f

Tactic:
⟨g, g_approx, g_supp⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
inst_8 : IsManifold I ∞ M
inst_9 : SigmaCompactSpace M
inst_10 : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst_6, _] ε
ε_pos : ∀ (x : M), 0 < ε x
g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯
g_approx : ∀ (x : M), dist ((g : (a : M) → F) x) (f x) < ε x
g_supp : support.{u_4, u_2} (M := F) (⇑g : (a : M) → F) ⊆ support f
⊢ ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯),
    (∀ (x : M), dist ((g : (a : M) → F) x) (f x) < ε x) ∧ support.{u_4, u_2} (M := F) (⇑g : (a : M) → F) ⊆ support f

Tactic:
exact ⟨g, g_approx, g_supp⟩
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
ε : E → ℝ
n : ℕ∞
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ε
ε_pos : ∀ (x : E), 0 < ε x
S U : Set E
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] S
hU : U ∈ 𝓝ˢ S
hfU : ContDiffOn ℝ (↑n : ℕ∞ω) f U
obtain :
  ∀ (g : C^(↑n : ℕ∞ω)⟮𝓘(ℝ, E), E; 𝓘(ℝ, F), F⟯) (g_approx : ∀ (x : E), dist ((g : (a : E) → F) x) (f x) < ε x)
    (g_eqOn : EqOn (⇑g : (a : E) → F) f S) (g_supp : support.{u_1, u_2} (M := F) (⇑g : (a : E) → F) ⊆ support f),
    ∃ (g : E → F), ContDiff ℝ (↑n : ℕ∞ω) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ EqOn g f S ∧ support g ⊆ support f
⊢ ∃ (g : E → F), ContDiff ℝ (↑n : ℕ∞ω) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ EqOn g f S ∧ support g ⊆ support f

Tactic:
obtain ⟨g, g_approx, g_eqOn, g_supp⟩ := f_cont.exists_contMDiff_approx_and_eqOn 𝓘(ℝ, E) n
    ε_cont ε_pos hS hU hfU.contMDiffOn

Premises used: Real, ContDiffOn.contMDiffOn, Continuous.exists_contMDiff_approx_and_eqOn, modelWithCornersSelf
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
ε : E → ℝ
n : ℕ∞
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ε
ε_pos : ∀ (x : E), 0 < ε x
S U : Set E
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] S
hU : U ∈ 𝓝ˢ S
hfU : ContDiffOn ℝ (↑n : ℕ∞ω) f U
g : C^(↑n : ℕ∞ω)⟮𝓘(ℝ, E), E; 𝓘(ℝ, F), F⟯
g_approx : ∀ (x : E), dist ((g : (a : E) → F) x) (f x) < ε x
g_eqOn : EqOn (⇑g : (a : E) → F) f S
g_supp : support.{u_1, u_2} (M := F) (⇑g : (a : E) → F) ⊆ support f
⊢ ∃ (g : E → F), ContDiff ℝ (↑n : ℕ∞ω) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ EqOn g f S ∧ support g ⊆ support f

Tactic:
⟨g, g.contMDiff.contDiff, g_approx, g_eqOn, g_supp⟩

Premises used: ContMDiffMap.contMDiff, And.intro, Exists.intro, ContMDiff.contDiff, DFunLike.coe
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
ε : E → ℝ
n : ℕ∞
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ε
ε_pos : ∀ (x : E), 0 < ε x
S U : Set E
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] S
hU : U ∈ 𝓝ˢ S
hfU : ContDiffOn ℝ (↑n : ℕ∞ω) f U
g : C^(↑n : ℕ∞ω)⟮𝓘(ℝ, E), E; 𝓘(ℝ, F), F⟯
g_approx : ∀ (x : E), dist ((g : (a : E) → F) x) (f x) < ε x
g_eqOn : EqOn (⇑g : (a : E) → F) f S
g_supp : support.{u_1, u_2} (M := F) (⇑g : (a : E) → F) ⊆ support f
⊢ ∃ (g : E → F), ContDiff ℝ (↑n : ℕ∞ω) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ EqOn g f S ∧ support g ⊆ support f

Tactic:
exact ⟨g, g.contMDiff.contDiff, g_approx, g_eqOn, g_supp⟩
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
ε : E → ℝ
n : ℕ∞
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ε
ε_pos : ∀ (x : E), 0 < ε x
obtain :
  ∀ (g : E → F) (g_contDiff : ContDiff ℝ (↑n : ℕ∞ω) g) (g_approx : ∀ (x : E), dist (g x) (f x) < ε x)
    (g_supp : support g ⊆ support f),
    ∃ (g : E → F), ContDiff ℝ (↑n : ℕ∞ω) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ support g ⊆ support f
⊢ ∃ (g : E → F), ContDiff ℝ (↑n : ℕ∞ω) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ support g ⊆ support f

Tactic:
obtain ⟨g, g_contDiff, g_approx, -, g_supp⟩ := f_cont.exists_contDiff_approx_and_eqOn n
    ε_cont ε_pos isClosed_empty mem_nhdsSet_empty contDiffOn_empty

Premises used: mem_nhdsSet_empty, Continuous.exists_contDiff_approx_and_eqOn, isClosed_empty, contDiffOn_empty
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
ε : E → ℝ
n : ℕ∞
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ε
ε_pos : ∀ (x : E), 0 < ε x
g : E → F
g_contDiff : ContDiff ℝ (↑n : ℕ∞ω) g
g_approx : ∀ (x : E), dist (g x) (f x) < ε x
g_supp : support g ⊆ support f
⊢ ∃ (g : E → F), ContDiff ℝ (↑n : ℕ∞ω) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ support g ⊆ support f

Tactic:
⟨g, g_contDiff, g_approx, g_supp⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
ε : E → ℝ
n : ℕ∞
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ε
ε_pos : ∀ (x : E), 0 < ε x
g : E → F
g_contDiff : ContDiff ℝ (↑n : ℕ∞ω) g
g_approx : ∀ (x : E), dist (g x) (f x) < ε x
g_supp : support g ⊆ support f
⊢ ∃ (g : E → F), ContDiff ℝ (↑n : ℕ∞ω) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ support g ⊆ support f

Tactic:
exact ⟨g, g_contDiff, g_approx, g_supp⟩
-- Module: Mathlib.Geometry.Manifold.SmoothEmbedding
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
H : Type u_6
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E₁ H
M : Type u_10
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
⊢ IsSmoothEmbedding.{u_1, u_2, u_2, u_6, u_6, u_10, u_10} I I (M := M) n id

Tactic:
⟨.id, .id⟩

Premises used: Manifold.IsImmersion.id, Topology.IsEmbedding.id, Manifold.IsSmoothEmbedding.mk
-- Module: Mathlib.Geometry.Manifold.SmoothEmbedding
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
E₂ : Type u_3
E₃ : Type u_4
E₄ : Type u_5
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : NormedAddCommGroup E₂
inst_4 : NormedSpace 𝕜 E₂
inst_5 : NormedAddCommGroup E₃
inst_6 : NormedSpace 𝕜 E₃
inst_7 : NormedAddCommGroup E₄
inst_8 : NormedSpace 𝕜 E₄
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst_9 : TopologicalSpace H
inst_10 : TopologicalSpace H'
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E₁ H
I' : ModelWithCorners 𝕜 E₂ H'
J : ModelWithCorners 𝕜 E₃ G
J' : ModelWithCorners 𝕜 E₄ G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : TopologicalSpace M'
inst_16 : ChartedSpace H' M'
inst_17 : TopologicalSpace N
inst_18 : ChartedSpace G N
inst_19 : TopologicalSpace N'
inst_20 : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
g : M' → N'
inst_21 : IsManifold I n M
inst_22 : IsManifold I' n M'
inst_23 : IsManifold J n N
inst_24 : IsManifold J' n N'
hf : IsSmoothEmbedding I J n f
hg : IsSmoothEmbedding I' J' n g
⊢ IsSmoothEmbedding (I.prod I') (J.prod J') n (Prod.map f g)

Tactic:
⟨hf.1.prodMap hg.1, hf.2.prodMap hg.2⟩

Premises used: Manifold.IsSmoothEmbedding.isEmbedding, Topology.IsEmbedding.prodMap, Manifold.IsImmersion.prodMap, Manifold.IsSmoothEmbedding.isImmersion, Manifold.IsSmoothEmbedding.mk
-- Module: Mathlib.Geometry.Manifold.SmoothEmbedding
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
H : Type u_6
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E₁ H
M : Type u_10
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
s : TopologicalSpace.Opens M
rw :
  IsImmersion.{u_2, u_1, u_2, u_6, u_6, u_10, u_10} I I (M := ↥s) n (Subtype.val (p := fun (x : M) ↦ x ∈ s)) ∧
    IsEmbedding.{u_10, u_10} (X := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ IsSmoothEmbedding.{u_1, u_2, u_2, u_6, u_6, u_10, u_10} I I (M := ↥s) n (Subtype.val (p := fun (x : M) ↦ x ∈ s))

Tactic:
rw [isSmoothEmbedding_iff]

Premises used: Manifold.isSmoothEmbedding_iff
-- Module: Mathlib.Geometry.Manifold.SmoothEmbedding
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
H : Type u_6
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E₁ H
M : Type u_10
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
s : TopologicalSpace.Opens M
⊢ IsImmersion.{u_2, u_1, u_2, u_6, u_6, u_10, u_10} I I (M := ↥s) n (Subtype.val (p := fun (x : M) ↦ x ∈ s)) ∧
    IsEmbedding.{u_10, u_10} (X := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s))

Tactic:
⟨IsImmersion.of_opens s, IsEmbedding.subtypeVal⟩

Premises used: Manifold.IsImmersion.of_opens, And.intro, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Geometry.Manifold.SmoothEmbedding
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
H : Type u_6
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E₁ H
M : Type u_10
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
s : TopologicalSpace.Opens M
⊢ IsImmersion.{u_2, u_1, u_2, u_6, u_6, u_10, u_10} I I (M := ↥s) n (Subtype.val (p := fun (x : M) ↦ x ∈ s)) ∧
    IsEmbedding.{u_10, u_10} (X := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s))

Tactic:
exact ⟨IsImmersion.of_opens s, IsEmbedding.subtypeVal⟩
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
N O : StructureGroupoid H
h :
  Eq.{u_2 + 1} (α := Set (OpenPartialHomeomorph H H)) ((fun (s : StructureGroupoid H) ↦ s.members) N)
    ((fun (s : StructureGroupoid H) ↦ s.members) O)
mk :
  ∀ (members : Set (OpenPartialHomeomorph H H))
    (trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members)
    (symm' : ∀ e ∈ members, e.symm ∈ members) (id_mem' : OpenPartialHomeomorph.refl H ∈ members)
    (locality' :
      ∀ (e : OpenPartialHomeomorph H H),
        (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst_1] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members)
    (mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members)
    (h :
      Eq.{u_2 + 1} (α := Set (OpenPartialHomeomorph H H))
        ((fun (s : StructureGroupoid H) ↦ s.members)
          { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
            mem_of_eqOnSource' := mem_of_eqOnSource' })
        ((fun (s : StructureGroupoid H) ↦ s.members) O)),
    { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
      O
⊢ N = O

Tactic:
cases N
-- Module: Mathlib.Geometry.Manifold.StructureGroupoid
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
O : StructureGroupoid H
members : Set (OpenPartialHomeomorph H H)
trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members
symm' : ∀ e ∈ members, e.symm ∈ members
id_mem' : OpenPartialHomeomorph.refl H ∈ members
locality' :
  ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst_1] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members
mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members
h :
  Eq.{u_2 + 1} (α := Set (OpenPartialHomeomorph H H))
    ((fun (s : StructureGroupoid H) ↦ s.members)
      { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' })
    ((fun (s : StructureGroupoid H) ↦ s.members) O)
mk :
  ∀ (members_1 : Set (OpenPartialHomeomorph H H))
    (trans'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ∈ members_1 → e ≫ₕ e' ∈ members_1)
    (symm'_1 : ∀ e ∈ members_1, e.symm ∈ members_1) (id_mem'_1 : OpenPartialHomeomorph.refl H ∈ members_1)
    (locality'_1 :
      ∀ (e : OpenPartialHomeomorph H H),
        (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst_1] s ∧ x ∈ s ∧ e.restr s ∈ members_1) → e ∈ members_1)
    (mem_of_eqOnSource'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ≈ e → e' ∈ members_1)
    (h :
      Eq.{u_2 + 1} (α := Set (OpenPartialHomeomorph H H))
        ((fun (s : StructureGroupoid H) ↦ s.members)
          { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
            mem_of_eqOnSource' := mem_of_eqOnSource' })
        ((fun (s : StructureGroupoid H) ↦ s.members)
          { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
            mem_of_eqOnSource' := mem_of_eqOnSource'_1 })),
    { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
      { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
        mem_of_eqOnSource' := mem_of_eqOnSource'_1 }
⊢ { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
      mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
    O

Tactic:
cases O