awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.Smooth (goal)
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 : (↑(TopCat.of M) : Type u)
⊢ Eq (α := (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u) ⟶ R)
    (Iso.hom (forgetStalk IM I M R x) ≫ smoothSheaf.evalHom IM I R x)
    (↾(⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x)
            (evalHom IM I M R x)) :
        (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → (↑(CommRingCat.of R) : Type u)))
have simp_rw : Eq (α := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x ⟶ R) (smoothSheaf.evalHom IM I R x)
  (CategoryStruct.comp (Y :=
    (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
    (Iso.inv (forgetStalk IM I M R x))
    (↾(⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x)
            (evalHom IM I M R x)) :
        (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → R)))
Tactic: simp_rw [← CategoryTheory.Iso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.Smooth (goal)
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 : (↑(TopCat.of M) : Type u)
⊢ Eq (α := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x ⟶ R) (smoothSheaf.evalHom IM I R x)
    (CategoryStruct.comp (Y :=
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
      (Iso.inv (forgetStalk IM I M R x))
      (↾(⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x)
              (evalHom IM I M R x)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → R)))
have rw : Eq (α := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x ⟶ R)
  (CategoryStruct.comp (Y :=
    (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
    (Iso.inv (forgetStalk IM I M R x))
    (↾(⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) :
        (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → (↑(CommRingCat.of R) : Type u))))
  (CategoryStruct.comp (Y :=
    (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
    (Iso.inv (forgetStalk IM I M R x))
    (↾(⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x)
            (evalHom IM I M R x)) :
        (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → R)))
Tactic: rw [← smoothSheafCommRing.forgetStalk_inv_comp_eval]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.Smooth (goal)
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
r : R
⊢ ∃ (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 = r
have obtain : ∀ (y : TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x),
  ∃ (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: obtain ⟨y, rfl⟩ := smoothSheaf.eval_surjective IM I R x r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.Smooth (goal)
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
⊢ ∃ (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
have 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
Tactic: use (smoothSheafCommRing.forgetStalk IM I M R x).inv y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (hypothesis)
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
⊢ ∃ (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
have dist_f_f : ∀ (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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (goal)
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)
⊢ ∃ (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
have 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
Tactic: rcases this with ⟨g, hg⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (goal)
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⟯),
    (∀ (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
have suffices : ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯), ∀ (x : M), Membership.mem (α := F) (t x) ((g : (a : M) → F) x : 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⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (hypothesis)
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⟯), ∀ (x : M), Membership.mem (α := F) (t x) ((g : (a : M) → F) x : F)
have t_conv : ∀ (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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (goal)
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)
⊢ ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯), ∀ (x : M), Membership.mem (α := F) (t x) ((g : (a : M) → F) x : F)
have apply : ∀ (x : M), ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y
Tactic: apply exists_contMDiffMap_forall_mem_convex_of_local I t_conv
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (goal)
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
⊢ ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y
have pos : ∀ (hx : x ∈ S), ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y
Tactic: by_cases hx : x ∈ S
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (goal)
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
⊢ ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y
have neg : ∀ (hx : x ∉ S), ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y
Tactic: by_cases hx : x ∈ S
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (goal)
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
have pos : ∃ (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, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (hypothesis)
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
have this : ∀ᶠ (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))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (goal)
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)
have pos : ∀ (hx' : 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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (goal)
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)
⊢ ∀ᶠ (y : M) in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)
have neg : ∀ (hx' : ¬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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (hypothesis)
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
⊢ ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y
have this₁ : ∀ᶠ (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')
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (goal)
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⟯),
    (∀ (x : M), dist ((g : (a : M) → F) x) (f x) < ε x) ∧ support.{u_4, u_2} (M := F) (⇑g : (a : M) → F) ⊆ support f
have 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
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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (goal)
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 : E → F), ContDiff ℝ (↑n : ℕ∞ω) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ EqOn g f S ∧ support g ⊆ support f
have 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
Tactic: obtain ⟨g, g_approx, g_eqOn, g_supp⟩ := f_cont.exists_contMDiff_approx_and_eqOn 𝓘(ℝ, E) n
    ε_cont ε_pos hS hU hfU.contMDiffOn