-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem nhds_basis_tsupport :
    (𝓝 c).HasBasis (fun _ : SmoothBumpFunction I c => True) fun f => tsupport f

Proof state:
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
c : M
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ (map (↑(extChartAt I c).symm) (𝓝[range ↑I] ↑(extChartAt I c) c)).HasBasis (fun x => True) fun f =>
    ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)

Tactic:
exact nhdsWithin_range_basis.map _

Result:
no goals

Proof state:
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
c : M
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
this :
  (𝓝 c).HasBasis (fun x => True) fun f => ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
⊢ (𝓝 c).HasBasis (fun x => True) fun f => tsupport ↑f

Tactic:
exact this.to_hasBasis' (fun f _ => ⟨f, trivial, f.tsupport_subset_symm_image_closedBall⟩)
  fun f _ => f.tsupport_mem_nhds

Result:
no goals

Proof state:
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
c : M
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ (𝓝 c).HasBasis (fun x => True) fun f => tsupport ↑f

Tactic:
have :
  (𝓝 c).HasBasis (fun _ : SmoothBumpFunction I c => True) fun f =>
    (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I) := by
  rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c]
  exact nhdsWithin_range_basis.map _

Result:
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
c : M
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
this :
  (𝓝 c).HasBasis (fun x => True) fun f => ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
⊢ (𝓝 c).HasBasis (fun x => True) fun f => tsupport ↑f

Proof state:
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
c : M
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ (𝓝 c).HasBasis (fun x => True) fun f => ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)

Tactic:
rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c]

Result:
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
c : M
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ (map (↑(extChartAt I c).symm) (𝓝[range ↑I] ↑(extChartAt I c) c)).HasBasis (fun x => True) fun f =>
    ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)