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
hsc : IsClosed[inst_3] s
hs : s ⊆ support (↑f : M → ℝ)
e : PartialEquiv M E := extChartAt I c
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑e : M → E) '' s)

Tactic:
have : IsClosed (e '' s) := f.isClosed_image_of_isClosed hsc hs
-- 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 → ℝ)
e : PartialEquiv M E := extChartAt I c
this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑e : M → E) '' s)
⊢ s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∧
    (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut

Tactic:
rw [support_eq_inter_preimage, subset_inter_iff, ← image_subset_iff] at hs

Premises used: Set.subset_inter_iff, SmoothBumpFunction.support_eq_inter_preimage, Set.image_subset_iff
-- 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 → ℝ)
e : PartialEquiv M E := extChartAt I c
this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑e : M → E) '' s)
hs₁ :
  s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∧
    (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
⊢ let e := extChartAt I c;
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑e : M → E) '' s)

Tactic:
rw [support_eq_inter_preimage, subset_inter_iff, ← image_subset_iff] at hs

Premises used: Set.subset_inter_iff, SmoothBumpFunction.support_eq_inter_preimage, Set.image_subset_iff
-- 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 ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∧
    (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
e : PartialEquiv M E := extChartAt I c
this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑e : M → E) '' s)
rcases :
  ∀ (r : ℝ) (hrR : r ∈ Ioo 0 f.rOut) (hr : (↑e : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) r),
    ∃ r ∈ Ioo 0 f.rOut,
      s ⊆
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
          (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) r
⊢ ∃ r ∈ Ioo 0 f.rOut,
    s ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
        (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) r

Tactic:
rcases exists_pos_lt_subset_ball f.rOut_pos this hs.2 with ⟨r, hrR, hr⟩

Premises used: SmoothBumpFunction.rOut_pos, exists_pos_lt_subset_ball, 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
inst_5 : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed[inst_3] s
hs :
  s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∧
    (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
e : PartialEquiv M E := extChartAt I c
this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑e : M → E) '' s)
r : ℝ
hrR : r ∈ Ioo 0 f.rOut
hr : (↑e : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) r
⊢ ∃ r ∈ Ioo 0 f.rOut,
    s ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
        (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) r

Tactic:
⟨r, hrR, subset_inter hs.1 (image_subset_iff.1 hr)⟩

Premises used: Set.subset_inter, And.left, And.intro, Exists.intro, Iff.mp, Set.image_subset_iff
-- 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 ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∧
    (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
e : PartialEquiv M E := extChartAt I c
this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑e : M → E) '' s)
r : ℝ
hrR : r ∈ Ioo 0 f.rOut
hr : (↑e : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) r
⊢ ∃ r ∈ Ioo 0 f.rOut,
    s ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
        (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) r

Tactic:
exact ⟨r, hrR, subset_inter hs.1 (image_subset_iff.1 hr)⟩
-- 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
r : ℝ
hr : r ∈ Ioo 0 f.rOut
⊢ support (↑(f.updateRIn r hr) : M → ℝ) = support (↑f : M → ℝ)

Tactic:
simp only [support_eq_inter_preimage, updateRIn_rOut]

Premises used: SmoothBumpFunction.support_eq_inter_preimage, SmoothBumpFunction.updateRIn_rOut
-- 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
⊢ Nonempty (SmoothBumpFunction I c)

Tactic:
nhdsWithin_range_basis.nonempty

Premises used: Filter.HasBasis.nonempty, SmoothBumpFunction.nhdsWithin_range_basis
-- 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
inst_6 : T2Space M
⊢ IsClosed[inst_3]
    ((↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E)))

Tactic:
f.isCompact_symm_image_closedBall.isClosed

Premises used: IsCompact.isClosed, SmoothBumpFunction.isCompact_symm_image_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
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
rw :
  closure[inst_3]
      ((↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))) ⊆
    (↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
⊢ tsupport (↑f : M → ℝ) ⊆
    (↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))

Tactic:
rw [tsupport, support_eq_symm_image]

Premises used: SmoothBumpFunction.support_eq_symm_image, tsupport
-- 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
inst_6 : T2Space M
⊢ closure[inst_3]
      ((↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))) ⊆
    (↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))

Tactic:
closure_minimal (image_mono <| inter_subset_inter_left _ ball_subset_closedBall)
    f.isClosed_symm_image_closedBall

Premises used: Metric.ball_subset_closedBall, closure_minimal, Set.image_mono, Set.inter_subset_inter_left, SmoothBumpFunction.isClosed_symm_image_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
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
⊢ closure[inst_3]
      ((↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))) ⊆
    (↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))

Tactic:
exact closure_minimal (image_mono <| inter_subset_inter_left _ ball_subset_closedBall)
    f.isClosed_symm_image_closedBall

Premises used: Metric.ball_subset_closedBall, closure_minimal, Set.image_mono, Set.inter_subset_inter_left, SmoothBumpFunction.isClosed_symm_image_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
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
⊢ tsupport (↑f : M → ℝ) ⊆ (extChartAt I c).source

Tactic:
calc
    tsupport f ⊆ (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I) :=
      f.tsupport_subset_symm_image_closedBall
    _ ⊆ (extChartAt I c).symm '' (extChartAt I c).target := image_mono f.closedBall_subset
    _ = (extChartAt I c).source := (extChartAt I c).symm_image_target_eq_source

Premises used: Trans.trans, extChartAt, PartialEquiv.symm_image_target_eq_source, Set.image_mono, SmoothBumpFunction.tsupport_subset_symm_image_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
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
⊢ tsupport (↑f : M → ℝ) ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source

Tactic:
simpa only [extChartAt_source] using f.tsupport_subset_extChartAt_source

Premises used: extChartAt_source, SmoothBumpFunction.tsupport_subset_extChartAt_source
-- 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
inst_6 : T2Space M
⊢ HasCompactSupport (↑f : M → ℝ)

Tactic:
f.isCompact_symm_image_closedBall.of_isClosed_subset isClosed_closure
    f.tsupport_subset_symm_image_closedBall

Premises used: SmoothBumpFunction.tsupport_subset_symm_image_closedBall, IsCompact.of_isClosed_subset, isClosed_closure, HasCompactSupport, SmoothBumpFunction.isCompact_symm_image_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
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
rw :
  (map (↑(extChartAt I c).symm : E → M) (𝓝[range (↑I : H → E)] (↑(extChartAt I c) : M → E) c)).HasBasis
    (fun (x : SmoothBumpFunction I c) ↦ True) fun (f : SmoothBumpFunction I c) ↦
    (↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
⊢ (𝓝 c).HasBasis (fun (x : SmoothBumpFunction I c) ↦ True) fun (f : SmoothBumpFunction I c) ↦
    (↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))

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

Premises used: map_extChartAt_symm_nhdsWithin_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
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
⊢ (map (↑(extChartAt I c).symm : E → M) (𝓝[range (↑I : H → E)] (↑(extChartAt I c) : M → E) c)).HasBasis
    (fun (x : SmoothBumpFunction I c) ↦ True) fun (f : SmoothBumpFunction I c) ↦
    (↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))

Tactic:
nhdsWithin_range_basis.map _

Premises used: Filter.HasBasis.map, SmoothBumpFunction.nhdsWithin_range_basis
-- 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
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
⊢ (map (↑(extChartAt I c).symm : E → M) (𝓝[range (↑I : H → E)] (↑(extChartAt I c) : M → E) c)).HasBasis
    (fun (x : SmoothBumpFunction I c) ↦ True) fun (f : SmoothBumpFunction I c) ↦
    (↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))

Tactic:
exact nhdsWithin_range_basis.map _

Premises used: Filter.HasBasis.map, SmoothBumpFunction.nhdsWithin_range_basis
-- 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
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
⊢ (𝓝 c).HasBasis (fun (x : SmoothBumpFunction I c) ↦ True) fun (f : SmoothBumpFunction I c) ↦
    (↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))

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 _
-- 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
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
this :
  (𝓝 c).HasBasis (fun (x : SmoothBumpFunction I c) ↦ True) fun (f : SmoothBumpFunction I c) ↦
    (↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
⊢ (𝓝 c).HasBasis (fun (x : SmoothBumpFunction I c) ↦ True) fun (f : SmoothBumpFunction I c) ↦ tsupport (↑f : M → ℝ)

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

Premises used: trivial, SmoothBumpFunction.tsupport_subset_symm_image_closedBall, SmoothBumpFunction.tsupport_mem_nhds, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis'
-- 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
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
this :
  (𝓝 c).HasBasis (fun (x : SmoothBumpFunction I c) ↦ True) fun (f : SmoothBumpFunction I c) ↦
    (↑(extChartAt I c).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
⊢ (𝓝 c).HasBasis (fun (x : SmoothBumpFunction I c) ↦ True) fun (f : SmoothBumpFunction I c) ↦ tsupport (↑f : M → ℝ)

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

Premises used: trivial, SmoothBumpFunction.tsupport_subset_symm_image_closedBall, SmoothBumpFunction.tsupport_mem_nhds, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis'
-- 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
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
s : Set M
hs : s ∈ 𝓝 c
⊢ (𝓝 c).HasBasis (fun (f : SmoothBumpFunction I c) ↦ tsupport (↑f : M → ℝ) ⊆ s) fun (f : SmoothBumpFunction I c) ↦
    support (↑f : M → ℝ)

Tactic:
((nhds_basis_tsupport c).restrict_subset hs).to_hasBasis'
    (fun f hf => ⟨f, hf.2, subset_closure⟩) fun f _ => f.support_mem_nhds

Premises used: subset_closure, SmoothBumpFunction.support_mem_nhds, Filter.HasBasis.restrict_subset, And.right, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis', SmoothBumpFunction.nhds_basis_tsupport
-- 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
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
⊢ ContMDiff I 𝓘(ℝ, ℝ) ∞ (↑f : M → ℝ)

Tactic:
contMDiff_of_tsupport fun x hx => ?_

Premises used: contMDiff_of_tsupport
-- 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
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
refine : ∀ (x : M) (hx : x ∈ tsupport (↑f : M → ℝ)), ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (↑f : M → ℝ) x
⊢ ContMDiff I 𝓘(ℝ, ℝ) ∞ (↑f : M → ℝ)

Tactic:
refine contMDiff_of_tsupport fun x hx => ?_

Premises used: contMDiff_of_tsupport
-- 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
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
x : M
hx : x ∈ tsupport (↑f : M → ℝ)
⊢ x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source

Tactic:
have : x ∈ (chartAt H c).source := f.tsupport_subset_chartAt_source 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
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
x : M
hx : x ∈ tsupport (↑f : M → ℝ)
this : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (↑f : M → ℝ) x

Tactic:
ContMDiffAt.congr_of_eventuallyEq ?_ <| f.eqOn_source.eventuallyEq_of_mem <|
    (chartAt H c).open_source.mem_nhds this

Premises used: chartAt, OpenPartialHomeomorph.open_source, SmoothBumpFunction.eqOn_source, Set.EqOn.eventuallyEq_of_mem, ContMDiffAt.congr_of_eventuallyEq, 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
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
x : M
hx : x ∈ tsupport (↑f : M → ℝ)
this : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
refine : ContMDiffAt I 𝓘(ℝ, ℝ) ∞ ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (↑f : M → ℝ) x

Tactic:
refine ContMDiffAt.congr_of_eventuallyEq ?_ <| f.eqOn_source.eventuallyEq_of_mem <|
    (chartAt H c).open_source.mem_nhds this

Premises used: chartAt, OpenPartialHomeomorph.open_source, SmoothBumpFunction.eqOn_source, Set.EqOn.eventuallyEq_of_mem, ContMDiffAt.congr_of_eventuallyEq, 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
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
x : M
hx : x ∈ tsupport (↑f : M → ℝ)
this : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ∞ ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x

Tactic:
f.contDiffAt.contMDiffAt.comp _ (contMDiffAt_extChartAt' this)

Premises used: ContDiffAt.contMDiffAt, SmoothBumpFunction.toContDiffBump, ContDiffBump.contDiffAt, contMDiffAt_extChartAt', ContMDiffAt.comp
-- 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
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
x : M
hx : x ∈ tsupport (↑f : M → ℝ)
this : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ∞ ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x

Tactic:
exact f.contDiffAt.contMDiffAt.comp _ (contMDiffAt_extChartAt' this)

Premises used: ContDiffAt.contMDiffAt, SmoothBumpFunction.toContDiffBump, ContDiffBump.contDiffAt, contMDiffAt_extChartAt', ContMDiffAt.comp
-- 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
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
x : M
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (↑f : M → ℝ) x

Tactic:
f.contMDiff.contMDiffAt

Premises used: SmoothBumpFunction.contMDiff, ContMDiff.contMDiffAt
-- 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
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
⊢ Continuous[inst_3, _] (↑f : M → ℝ)

Tactic:
f.contMDiff.continuous

Premises used: ContMDiff.continuous, SmoothBumpFunction.contMDiff