awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (hypothesis)
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
hs : s ⊆ support (↑f : M → ℝ)
⊢ (↑(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
have hs₁ : s ⊆ (extChartAt I 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, ← extChartAt_source I, ← image_subset_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (hypothesis)
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
hs : s ⊆ (extChartAt I c).source ∧ (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
⊢ (↑(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
have hse : s ⊆ (extChartAt I c).source
Tactic: obtain ⟨hse, hsf⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (hypothesis)
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
hs : s ⊆ (extChartAt I c).source ∧ (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
hse : s ⊆ (extChartAt I c).source
⊢ (↑(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
have hsf : (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
Tactic: obtain ⟨hse, hsf⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ (↑(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
have h₁ : (↑(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
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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) : 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 =
    closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s
have h₂ : 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: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ (↑(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
have h₁ : (↑(extChartAt I c) : M → E) '' s ⊆ range (↑I : H → E)
Tactic: refine subset_inter (subset_inter (hsf.trans ball_subset_closedBall) ?_) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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) : M → E) '' s ⊆ range (↑I : H → E)
⊢ (↑(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
have h₂ : (↑(extChartAt I c) : M → E) '' s ⊆ (↑(extChartAt I c).symm : E → M) ⁻¹' s
Tactic: refine subset_inter (subset_inter (hsf.trans ball_subset_closedBall) ?_) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ (↑(extChartAt I c) : M → E) '' s ⊆ (↑(extChartAt I c).symm : E → M) ⁻¹' s
have h₁ : (extChartAt I c).target ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆ (↑(extChartAt I c).symm : E → M) ⁻¹' s
Tactic: rw [(extChartAt I c).image_eq_target_inter_inv_preimage hse]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
have h₂ : (extChartAt I c).target ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆ (↑(extChartAt I c) : M → E) '' s
Tactic: refine Subset.trans (inter_subset_inter_left _ f.closedBall_subset) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ (extChartAt I c).target ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆ (↑(extChartAt I c) : M → E) '' s
have h₂ : (extChartAt I c).target ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆
  (extChartAt I c).target ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s
Tactic: rw [(extChartAt I c).image_eq_target_inter_inv_preimage hse]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (hypothesis)
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
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) ((↑f : M → ℝ) x)
have this : (↑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 _ _ _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) ((↑f : M → ℝ) x)
have inl : ∀ (h : (↑f : M → ℝ) x = 0), Membership.mem (γ := Set ℝ) (Icc 0 1) ((↑f : M → ℝ) x)
Tactic: rcases this with h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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)
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) ((↑f : M → ℝ) x)
have inr : ∀ (h : (↑f : M → ℝ) x = ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x),
  Membership.mem (γ := Set ℝ) (Icc 0 1) ((↑f : M → ℝ) x)
Tactic: rcases this with h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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) ((↑f : M → ℝ) x)
have inl : Membership.mem (γ := Set ℝ) (Icc 0 1) 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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 : M → ℝ) x)
have inr : Membership.mem (γ := Set ℝ) (Icc 0 1) (((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ (↑f : M → ℝ) =ᶠ[𝓝 x] 1
have 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
Tactic: filter_upwards [IsOpen.mem_nhds (isOpen_extChartAt_preimage c isOpen_ball) ⟨hs, hd⟩]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ dist ((↑(extChartAt I c) : M → E) c) ((↑(extChartAt I c) : M → E) c) < f.rIn
have rw : 0 < f.rIn
Tactic: rw [dist_self]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ (↑f : M → ℝ) x ≠ 0
have rw : Ne (α := ℝ) (1 x) 0
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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)
have 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)
Tactic: refine ((nhdsWithin_hasBasis nhds_basis_closedBall _).restrict_subset
    (extChartAt_target_mem_nhdsWithin _)).to_hasBasis' ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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)
⊢ (𝓝[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)
have 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
Tactic: refine ((nhdsWithin_hasBasis nhds_basis_closedBall _).restrict_subset
    (extChartAt_target_mem_nhdsWithin _)).to_hasBasis' ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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] ((↑(extChartAt I c) : M → E) '' s)
have 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)
Tactic: rw [f.image_eq_inter_preimage_of_subset_support hs]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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)
have refine : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
Tactic: refine ContinuousOn.preimage_isClosed_of_isClosed
    ((continuousOn_extChartAt_symm _).mono f.closedBall_subset) ?_ hsc
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (hypothesis)
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
⊢ ∃ 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
have this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑e : M → E) '' s)
Tactic: have : IsClosed (e '' s) := f.isClosed_image_of_isClosed hsc hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (hypothesis)
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)
⊢ ∃ 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
have hs₁ : 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
Cleared hypotheses: hs, e, this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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 ∈ Ioo 0 f.rOut,
    s ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
        (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) r
have 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
Tactic: rcases exists_pos_lt_subset_ball f.rOut_pos this hs.2 with ⟨r, hrR, hr⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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).symm : E → M) '' (closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
have 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))
Tactic: rw [tsupport, support_eq_symm_image]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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))
have 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))
Tactic: rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (hypothesis)
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) ↦ tsupport (↑f : M → ℝ)
have 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))
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 _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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 → ℝ)
have refine : ∀ (x : M) (hx : x ∈ tsupport (↑f : M → ℝ)), ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (↑f : M → ℝ) x
Tactic: refine contMDiff_of_tsupport fun x hx => ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (hypothesis)
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 → ℝ)
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (↑f : M → ℝ) x
have this : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
Tactic: have : x ∈ (chartAt H c).source := f.tsupport_subset_chartAt_source hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
have refine : ContMDiffAt I 𝓘(ℝ, ℝ) ∞ ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) x
Tactic: refine ContMDiffAt.congr_of_eventuallyEq ?_ <| f.eqOn_source.eventuallyEq_of_mem <|
    (chartAt H c).open_source.mem_nhds this