awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace HM M
R : Type u
inst_9 : TopologicalSpace R
inst_10 : ChartedSpace H R
inst_11 : CommRing R
inst_12 : ContMDiffRing I ∞ R
x : M
y : TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x
h :
  (eval IM I M R x : (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → R)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (forgetStalk IM I M R x)) :
            (a : (fun (X : Type u) ↦ X) ((smoothSheaf IM I M R).presheaf.stalk x)) →
              (fun (X : Type u) ↦ X) (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u))
          y :
        (fun (X : Type u) ↦ X)
          (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) :
            Type u)) =
    smoothSheaf.eval IM I R x y
⊢ ∃ (a :
    (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u)),
    (eval IM I M R x : (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → R) a =
      smoothSheaf.eval IM I R x y

Tactic:
use (smoothSheafCommRing.forgetStalk IM I M R x).inv y

Premises used: CategoryTheory.ConcreteCategory.hom, smoothSheafCommRing.forgetStalk, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace HM M
R : Type u
inst_9 : TopologicalSpace R
inst_10 : ChartedSpace H R
inst_11 : CommRing R
inst_12 : ContMDiffRing I ∞ R
x : M
y : TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x
⊢ (eval IM I M R x : (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → R)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (forgetStalk IM I M R x)) :
            (a : (fun (X : Type u) ↦ X) ((smoothSheaf IM I M R).presheaf.stalk x)) →
              (fun (X : Type u) ↦ X) (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u))
          y :
        (fun (X : Type u) ↦ X)
          (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) :
            Type u)) =
    smoothSheaf.eval IM I R x y

Tactic:
apply smoothSheafCommRing.forgetStalk_inv_comp_eval_apply

Premises used: smoothSheafCommRing.forgetStalk_inv_comp_eval_apply
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : CommRing R
inst_26 : ContMDiffRing I ∞ R
inst_27 : Nontrivial R
x : M
⊢ Nontrivial.{u}
    (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u)

Tactic:
(smoothSheafCommRing.eval_surjective IM I M R x).nontrivial

Premises used: Function.Surjective.nontrivial, smoothSheafCommRing.eval_surjective
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace HM M
R : Type u
inst_9 : TopologicalSpace R
inst_10 : ChartedSpace H R
inst_11 : CommRing R
inst_12 : ContMDiffRing I ∞ R
U : Opens M
x : M
hx : x ∈ U
f : (↑(Functor.obj (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) (op U)) : Type u)
⊢ (eval IM I M R x : (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → R)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Functor.obj (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) (op U))
              (Y := TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x)
              (TopCat.Presheaf.germ (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U x hx) :
            (a : (↑((smoothSheafCommRing IM I M R).presheaf.obj (op U)) : Type u)) →
              (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u))
          f :
        (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) :
          Type u)) =
    (↑f : (x : ↥(unop (op U))) → (fun (x : (↑(TopCat.of M) : Type u)) ↦ R) (↑x : (↑(TopCat.of M) : Type u)))
      (Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ unop (op U)) x hx)

Tactic:
smoothSheafCommRing.evalHom_germ IM I M R U x hx f

Premises used: smoothSheafCommRing.evalHom_germ
-- 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
⊢ ∀ (x : M), dist (f x) (f x) < ε x

Tactic:
simpa only [dist_self] using ε_pos

Premises used: dist_self
-- 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
⊢ ∀ (x : M), dist (f x) (f x) < ε x

Tactic:
have dist_f_f : ∀ x, dist (f x) (f x) < ε x := by simpa only [dist_self] using ε_pos
-- 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)}
this : ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯), ∀ (x : M), Membership.mem (α := F) (t x) ((g : (a : M) → F) x : F)
rcases :
  ∀ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯) (hg : ∀ (x : M), Membership.mem (α := F) (t x) ((g : (a : M) → F) x : F)),
    ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯),
      (∀ (x : M), dist ((g : (a : M) → F) x) (f x) < ε x) ∧
        EqOn (⇑g : (a : M) → F) f S ∧ 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) ∧
      EqOn (⇑g : (a : M) → F) f S ∧ support.{u_4, u_2} (M := F) (⇑g : (a : M) → F) ⊆ support f

Tactic:
rcases this with ⟨g, hg⟩
-- 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)}
g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯
hg : ∀ (x : M), Membership.mem (α := F) (t x) ((g : (a : M) → F) x : F)
⊢ ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯),
    (∀ (x : M), dist ((g : (a : M) → F) x) (f x) < ε x) ∧
      EqOn (⇑g : (a : M) → F) f S ∧ support.{u_4, u_2} (M := F) (⇑g : (a : M) → F) ⊆ support f

Tactic:
⟨g, fun x ↦ (hg x).1, fun x ↦ (hg x).2.1, fun x ↦ mt (hg x).2.2⟩

Premises used: mt, And.right, And.left, 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
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)}
g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯
hg : ∀ (x : M), Membership.mem (α := F) (t x) ((g : (a : M) → F) x : F)
⊢ ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯),
    (∀ (x : M), dist ((g : (a : M) → F) x) (f x) < ε x) ∧
      EqOn (⇑g : (a : M) → F) f S ∧ support.{u_4, u_2} (M := F) (⇑g : (a : M) → F) ⊆ support f

Tactic:
exact ⟨g, fun x ↦ (hg x).1, fun x ↦ (hg x).2.1, fun x ↦ mt (hg x).2.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
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)}
suffices : ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯), ∀ (x : M), Membership.mem (α := F) (t x) ((g : (a : M) → F) x : F)
⊢ ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯),
    (∀ (x : M), dist ((g : (a : M) → F) x) (f x) < ε x) ∧
      EqOn (⇑g : (a : M) → F) f S ∧ support.{u_4, u_2} (M := F) (⇑g : (a : M) → F) ⊆ support f

Tactic:
suffices ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x by
    rcases this with ⟨g, hg⟩
    exact ⟨g, fun x ↦ (hg x).1, fun x ↦ (hg x).2.1, fun x ↦ mt (hg x).2.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
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)}
⊢ ∀ (x : M), Convex ℝ (t x)

Tactic:
have t_conv (x) : Convex ℝ (t x) := (convex_ball (f x) (ε x)).inter <|
    (convex_singleton _).setOf_const_imp.inter (convex_singleton _).setOf_const_imp
-- 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)
apply : ∀ (x : M), ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y
⊢ ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯), ∀ (x : M), Membership.mem (α := F) (t x) ((g : (a : M) → F) x : F)

Tactic:
apply exists_contMDiffMap_forall_mem_convex_of_local I t_conv

Premises used: exists_contMDiffMap_forall_mem_convex_of_local
-- 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
pos : ∀ (hx : x ∈ S), ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y
neg : ∀ (hx : x ∉ S), ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y
⊢ ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y

Tactic:
by_cases hx : x ∈ S
-- 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
⊢ ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y

Tactic:
⟨U, mem_nhdsSet_iff_forall.mp hU x hx, ?_⟩

Premises used: mem_nhdsSet_iff_forall, And.intro, Exists.intro, Iff.mp
-- 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
pos : ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y
⊢ ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y

Tactic:
refine ⟨U, mem_nhdsSet_iff_forall.mp hU x 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
⊢ ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y

Tactic:
⟨f, hfU, fun y _ ↦ ⟨dist_f_f y, fun _ ↦ rfl, id⟩⟩

Premises used: id, And.intro, Exists.intro, rfl
-- 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
⊢ ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y

Tactic:
exact ⟨f, hfU, fun y _ ↦ ⟨dist_f_f y, fun _ ↦ rfl, id⟩⟩
-- 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
⊢ ∀ᶠ (y : M) in 𝓝 x, y ∉ S ∧ dist (f x) (f y) < ε y

Tactic:
have : ∀ᶠ y in 𝓝 x, y ∉ S ∧ dist (f x) (f y) < ε y := (hS.isOpen_compl.eventually_mem hx).and
      ((continuous_const.dist f_cont).continuousAt.eventually_lt ε_cont.continuousAt (dist_f_f x))
-- 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
pos : ∀ (hx' : f x = 0), ∀ᶠ (y : M) in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)
neg : ∀ (hx' : ¬f x = 0), ∀ᶠ (y : M) in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)
⊢ ∀ᶠ (y : M) in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)

Tactic:
by_cases hx' : f x = 0