awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
⊢ closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆
    (↑(extChartAt I c) : M → E) '' s

Tactic:
Subset.trans (inter_subset_inter_left _ f.closedBall_subset) ?_

Premises used: Set.Subset.trans, Set.inter_subset_inter_left, SmoothBumpFunction.closedBall_subset
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
h₂ : (extChartAt I c).target ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆ (↑(extChartAt I c) : M → E) '' s
⊢ closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆
    (↑(extChartAt I c) : M → E) '' s

Tactic:
refine Subset.trans (inter_subset_inter_left _ f.closedBall_subset) ?_

Premises used: Set.Subset.trans, Set.inter_subset_inter_left, SmoothBumpFunction.closedBall_subset
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
h₂ h₃ :
  (extChartAt I c).target ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆
    (extChartAt I c).target ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s
⊢ (extChartAt I c).target ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆ (↑(extChartAt I c) : M → E) '' s

Tactic:
rw [(extChartAt I c).image_eq_target_inter_inv_preimage hse]

Premises used: extChartAt, PartialEquiv.image_eq_target_inter_inv_preimage
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
⊢ (↑f : M → ℝ) x = 0 ∨ (↑f : M → ℝ) x = ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x

Tactic:
have : f x = 0 ∨ f x = _ := indicator_eq_zero_or_self _ _ _
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
this : (↑f : M → ℝ) x = 0 ∨ (↑f : M → ℝ) x = ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x
inl : ∀ (h : (↑f : M → ℝ) x = 0), Membership.mem (γ := Set ℝ) (Icc 0 1) ((↑f : M → ℝ) x)
inr :
  ∀ (h : (↑f : M → ℝ) x = ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x),
    Membership.mem (γ := Set ℝ) (Icc 0 1) ((↑f : M → ℝ) x)
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) ((↑f : M → ℝ) x)

Tactic:
rcases this with h | h
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
h : (↑f : M → ℝ) x = 0
inl : Membership.mem (γ := Set ℝ) (Icc 0 1) 0
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) ((↑f : M → ℝ) x)

Tactic:
rw [h]
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
h : (↑f : M → ℝ) x = ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x
inr : Membership.mem (γ := Set ℝ) (Icc 0 1) (((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x)
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) ((↑f : M → ℝ) x)

Tactic:
rw [h]
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
h : (↑f : M → ℝ) x = 0
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) 0

Tactic:
left_mem_Icc.2 zero_le_one

Premises used: Iff.mpr, zero_le_one, Set.left_mem_Icc
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
h : (↑f : M → ℝ) x = ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) (((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x)

Tactic:
⟨f.nonneg, f.le_one⟩

Premises used: Set.Mem, ContDiffBump.nonneg, setOf, SmoothBumpFunction.toContDiffBump, Set.Icc, And.intro, ContDiffBump.le_one
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
h : (↑f : M → ℝ) x = 0
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) 0

Tactic:
exacts [left_mem_Icc.2 zero_le_one, ⟨f.nonneg, f.le_one⟩]

Premises used: Iff.mpr, zero_le_one, Set.left_mem_Icc
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
⊢ 0 ≤ (↑f : M → ℝ) x

Tactic:
f.mem_Icc.1

Premises used: SmoothBumpFunction.mem_Icc, And.left
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
⊢ (↑f : M → ℝ) x ≤ 1

Tactic:
f.mem_Icc.2

Premises used: SmoothBumpFunction.mem_Icc, And.right
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
hs : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
hd : dist ((↑(extChartAt I c) : M → E) x) ((↑(extChartAt I c) : M → E) c) < f.rIn
h :
  ∀
    a ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
        (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rIn,
    (↑f : M → ℝ) a = 1 a
⊢ (↑f : M → ℝ) =ᶠ[𝓝 x] 1

Tactic:
filter_upwards [IsOpen.mem_nhds (isOpen_extChartAt_preimage c isOpen_ball) ⟨hs, hd⟩]

Premises used: isOpen_extChartAt_preimage, Metric.isOpen_ball, And.intro, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
hs : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
hd : dist ((↑(extChartAt I c) : M → E) x) ((↑(extChartAt I c) : M → E) c) < f.rIn
z : M
hzs : z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
hzd : z ∈ (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rIn
⊢ (↑f : M → ℝ) z = 1 z

Tactic:
f.one_of_dist_le hzs <| le_of_lt hzd

Premises used: le_of_lt, SmoothBumpFunction.one_of_dist_le
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
hs : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
hd : dist ((↑(extChartAt I c) : M → E) x) ((↑(extChartAt I c) : M → E) c) < f.rIn
z : M
hzs : z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
hzd : z ∈ (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rIn
⊢ (↑f : M → ℝ) z = 1 z

Tactic:
exact f.one_of_dist_le hzs <| le_of_lt hzd

Premises used: le_of_lt, SmoothBumpFunction.one_of_dist_le
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
rw : 0 < f.rIn
⊢ dist ((↑(extChartAt I c) : M → E) c) ((↑(extChartAt I c) : M → E) c) < f.rIn

Tactic:
rw [dist_self]

Premises used: dist_self
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
⊢ 0 < f.rIn

Tactic:
f.rIn_pos

Premises used: SmoothBumpFunction.toContDiffBump, ContDiffBump.rIn_pos
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
⊢ 0 < f.rIn

Tactic:
exact f.rIn_pos

Premises used: SmoothBumpFunction.toContDiffBump, ContDiffBump.rIn_pos
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
⊢ (↑f : M → ℝ) c = 1

Tactic:
f.eventuallyEq_one.eq_of_nhds

Premises used: Filter.EventuallyEq.eq_of_nhds, SmoothBumpFunction.eventuallyEq_one
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
x : M
hx : (↑f : M → ℝ) x = 1 x
rw : Ne (α := ℝ) (1 x) 0
⊢ (↑f : M → ℝ) x ≠ 0

Tactic:
rw [hx]
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
x : M
hx : (↑f : M → ℝ) x = 1 x
⊢ Ne (α := ℝ) (1 x) 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
x : M
hx : (↑f : M → ℝ) x = 1 x
⊢ Ne (α := ℝ) (1 x) 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
⊢ tsupport (↑f : M → ℝ) ∈ 𝓝 c

Tactic:
mem_of_superset f.support_mem_nhds subset_closure

Premises used: subset_closure, SmoothBumpFunction.support_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
⊢ c ∈ support (↑f : M → ℝ)

Tactic:
mem_of_mem_nhds f.support_mem_nhds

Premises used: SmoothBumpFunction.support_mem_nhds, mem_of_mem_nhds
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
⊢ (support (↑f : M → ℝ)).Nonempty

Tactic:
⟨c, f.c_mem_support⟩

Premises used: SmoothBumpFunction.c_mem_support, Set.Nonempty, Exists.intro
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
⊢ IsCompact
    ((↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E)))

Tactic:
((isCompact_closedBall _ _).inter_right I.isClosed_range).image_of_continuousOn <|
    (continuousOn_extChartAt_symm _).mono f.closedBall_subset

Premises used: continuousOn_extChartAt_symm, IsCompact.image_of_continuousOn, ContinuousOn.mono, IsCompact.inter_right, ModelWithCorners.isClosed_range, ProperSpace.isCompact_closedBall, SmoothBumpFunction.closedBall_subset
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
⊢ (𝓝[range (↑I : H → E)] (↑(extChartAt I c) : M → E) c).HasBasis (fun (x : SmoothBumpFunction I c) ↦ True)
    fun (f : SmoothBumpFunction I c) ↦ closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E)

Tactic:
((nhdsWithin_hasBasis nhds_basis_closedBall _).restrict_subset
    (extChartAt_target_mem_nhdsWithin _)).to_hasBasis' ?_ ?_

Premises used: extChartAt_target_mem_nhdsWithin, Filter.HasBasis.restrict_subset, Filter.HasBasis.to_hasBasis', nhdsWithin_hasBasis, Metric.nhds_basis_closedBall
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
refine_1 :
  ∀ (i : ℝ),
    0 < i ∧ closedBall ((↑(extChartAt I c) : M → E) c) i ∩ range (↑I : H → E) ⊆ (extChartAt I c).target →
      ∃ (i' : SmoothBumpFunction I c),
        True ∧
          closedBall ((↑(extChartAt I c) : M → E) c) i'.rOut ∩ range (↑I : H → E) ⊆
            closedBall ((↑(extChartAt I c) : M → E) c) i ∩ range (↑I : H → E)
refine_2 :
  ∀ (i' : SmoothBumpFunction I c),
    True →
      closedBall ((↑(extChartAt I c) : M → E) c) i'.rOut ∩ range (↑I : H → E) ∈
        𝓝[range (↑I : H → E)] (↑(extChartAt I c) : M → E) c
⊢ (𝓝[range (↑I : H → E)] (↑(extChartAt I c) : M → E) c).HasBasis (fun (x : SmoothBumpFunction I c) ↦ True)
    fun (f : SmoothBumpFunction I c) ↦ closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E)

Tactic:
refine ((nhdsWithin_hasBasis nhds_basis_closedBall _).restrict_subset
    (extChartAt_target_mem_nhdsWithin _)).to_hasBasis' ?_ ?_

Premises used: extChartAt_target_mem_nhdsWithin, Filter.HasBasis.restrict_subset, Filter.HasBasis.to_hasBasis', nhdsWithin_hasBasis, Metric.nhds_basis_closedBall
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
R : ℝ
hR0 : 0 < R
hsub : closedBall ((↑(extChartAt I c) : M → E) c) R ∩ range (↑I : H → E) ⊆ (extChartAt I c).target
⊢ ∃ (i' : SmoothBumpFunction I c),
    True ∧
      closedBall ((↑(extChartAt I c) : M → E) c) i'.rOut ∩ range (↑I : H → E) ⊆
        closedBall ((↑(extChartAt I c) : M → E) c) R ∩ range (↑I : H → E)

Tactic:
⟨⟨⟨R / 2, R, half_pos hR0, half_lt_self hR0⟩, hsub⟩, trivial, Subset.rfl⟩

Premises used: half_lt_self, trivial, half_pos, HDiv.hDiv, Set.Subset.rfl, And.intro, Exists.intro, OfNat.ofNat, SmoothBumpFunction.mk, ContDiffBump.mk
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
R : ℝ
hR0 : 0 < R
hsub : closedBall ((↑(extChartAt I c) : M → E) c) R ∩ range (↑I : H → E) ⊆ (extChartAt I c).target
⊢ ∃ (i' : SmoothBumpFunction I c),
    True ∧
      closedBall ((↑(extChartAt I c) : M → E) c) i'.rOut ∩ range (↑I : H → E) ⊆
        closedBall ((↑(extChartAt I c) : M → E) c) R ∩ range (↑I : H → E)

Tactic:
exact ⟨⟨⟨R / 2, R, half_pos hR0, half_lt_self hR0⟩, hsub⟩, trivial, Subset.rfl⟩
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
⊢ ∀ (i' : SmoothBumpFunction I c),
    True →
      closedBall ((↑(extChartAt I c) : M → E) c) i'.rOut ∩ range (↑I : H → E) ∈
        𝓝[range (↑I : H → E)] (↑(extChartAt I c) : M → E) c

Tactic:
fun f _ => inter_mem (mem_nhdsWithin_of_mem_nhds <| closedBall_mem_nhds _ f.rOut_pos)
      self_mem_nhdsWithin

Premises used: SmoothBumpFunction.rOut_pos, extChartAt, Metric.closedBall_mem_nhds, Filter.inter_mem, mem_nhdsWithin_of_mem_nhds, self_mem_nhdsWithin, PartialEquiv.toFun
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
⊢ ∀ (i' : SmoothBumpFunction I c),
    True →
      closedBall ((↑(extChartAt I c) : M → E) c) i'.rOut ∩ range (↑I : H → E) ∈
        𝓝[range (↑I : H → E)] (↑(extChartAt I c) : M → E) c

Tactic:
exact fun f _ => inter_mem (mem_nhdsWithin_of_mem_nhds <| closedBall_mem_nhds _ f.rOut_pos)
      self_mem_nhdsWithin

Premises used: Metric.closedBall_mem_nhds, Filter.inter_mem, mem_nhdsWithin_of_mem_nhds, self_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed[inst_3] s
hs : s ⊆ support (↑f : M → ℝ)
rw :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑(extChartAt I c) : M → E) '' s)

Tactic:
rw [f.image_eq_inter_preimage_of_subset_support hs]

Premises used: SmoothBumpFunction.image_eq_inter_preimage_of_subset_support
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed[inst_3] s
hs : s ⊆ support (↑f : M → ℝ)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s)

Tactic:
ContinuousOn.preimage_isClosed_of_isClosed
    ((continuousOn_extChartAt_symm _).mono f.closedBall_subset) ?_ hsc

Premises used: ContinuousOn.preimage_isClosed_of_isClosed, continuousOn_extChartAt_symm, ContinuousOn.mono, SmoothBumpFunction.closedBall_subset
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed[inst_3] s
hs : s ⊆ support (↑f : M → ℝ)
refine :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s)

Tactic:
refine ContinuousOn.preimage_isClosed_of_isClosed
    ((continuousOn_extChartAt_symm _).mono f.closedBall_subset) ?_ hsc

Premises used: ContinuousOn.preimage_isClosed_of_isClosed, continuousOn_extChartAt_symm, ContinuousOn.mono, SmoothBumpFunction.closedBall_subset
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed[inst_3] s
hs : s ⊆ support (↑f : M → ℝ)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))

Tactic:
IsClosed.inter isClosed_closedBall I.isClosed_range

Premises used: Metric.isClosed_closedBall, IsClosed.inter, ModelWithCorners.isClosed_range
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed[inst_3] s
hs : s ⊆ support (↑f : M → ℝ)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))

Tactic:
exact IsClosed.inter isClosed_closedBall I.isClosed_range

Premises used: Metric.isClosed_closedBall, IsClosed.inter, ModelWithCorners.isClosed_range