awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
inst_5 : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst_6 : T2Space M
inst_7 : SigmaCompactSpace M
hs : IsClosed[inst_3] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
hB :
  ∀ (x : M) (hx : x ∈ s),
    (𝓝 x).HasBasis (fun (f : SmoothBumpFunction I x) ↦ tsupport (↑f : M → ℝ) ⊆ U x) fun (f : SmoothBumpFunction I x) ↦
      support (↑f : M → ℝ)
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst_3] (V i)
hVf : ∀ (i : ι), V i ⊆ support (↑(f i) : M → ℝ)
r : (i : ι) → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (c i))).source ∩
        (↑(extChartAt I (c i)) : M → E) ⁻¹' Metric.ball ((↑(extChartAt I (c i)) : M → E) (c i)) (r i)
x : M
hx : x ∈ s
⊢ ∃ (i : ι), (↑((fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) i) : M → ℝ) =ᶠ[𝓝 x] 1

Tactic:
(mem_iUnion.1 <| hsV hx).imp fun i hi => ?_

Premises used: Set.mem_iUnion, Exists.imp, Iff.mp
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
inst_5 : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst_6 : T2Space M
inst_7 : SigmaCompactSpace M
hs : IsClosed[inst_3] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
hB :
  ∀ (x : M) (hx : x ∈ s),
    (𝓝 x).HasBasis (fun (f : SmoothBumpFunction I x) ↦ tsupport (↑f : M → ℝ) ⊆ U x) fun (f : SmoothBumpFunction I x) ↦
      support (↑f : M → ℝ)
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst_3] (V i)
hVf : ∀ (i : ι), V i ⊆ support (↑(f i) : M → ℝ)
r : (i : ι) → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (c i))).source ∩
        (↑(extChartAt I (c i)) : M → E) ⁻¹' Metric.ball ((↑(extChartAt I (c i)) : M → E) (c i)) (r i)
x : M
hx : x ∈ s
refine_2 : ∀ (i : ι) (hi : x ∈ V i), (↑((fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) i) : M → ℝ) =ᶠ[𝓝 x] 1
⊢ ∃ (i : ι), (↑((fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) i) : M → ℝ) =ᶠ[𝓝 x] 1

Tactic:
refine (mem_iUnion.1 <| hsV hx).imp fun i hi => ?_

Premises used: Set.mem_iUnion, Exists.imp, Iff.mp
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
inst_5 : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst_6 : T2Space M
inst_7 : SigmaCompactSpace M
hs : IsClosed[inst_3] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
hB :
  ∀ (x : M) (hx : x ∈ s),
    (𝓝 x).HasBasis (fun (f : SmoothBumpFunction I x) ↦ tsupport (↑f : M → ℝ) ⊆ U x) fun (f : SmoothBumpFunction I x) ↦
      support (↑f : M → ℝ)
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst_3] (V i)
hVf : ∀ (i : ι), V i ⊆ support (↑(f i) : M → ℝ)
r : (i : ι) → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (c i))).source ∩
        (↑(extChartAt I (c i)) : M → E) ⁻¹' Metric.ball ((↑(extChartAt I (c i)) : M → E) (c i)) (r i)
x : M
hx : x ∈ s
i : ι
hi : x ∈ V i
⊢ (↑((fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) i) : M → ℝ) =ᶠ[𝓝 x] 1

Tactic:
((f i).updateRIn _ _).eventuallyEq_one_of_dist_lt
      ((f i).support_subset_source <| hVf _ hi) (hr i hi).2

Premises used: And.right, SmoothBumpFunction.updateRIn, SmoothBumpFunction.eventuallyEq_one_of_dist_lt, SmoothBumpFunction.support_subset_source
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
inst_5 : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst_6 : T2Space M
inst_7 : SigmaCompactSpace M
hs : IsClosed[inst_3] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
hB :
  ∀ (x : M) (hx : x ∈ s),
    (𝓝 x).HasBasis (fun (f : SmoothBumpFunction I x) ↦ tsupport (↑f : M → ℝ) ⊆ U x) fun (f : SmoothBumpFunction I x) ↦
      support (↑f : M → ℝ)
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst_3] (V i)
hVf : ∀ (i : ι), V i ⊆ support (↑(f i) : M → ℝ)
r : (i : ι) → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (c i))).source ∩
        (↑(extChartAt I (c i)) : M → E) ⁻¹' Metric.ball ((↑(extChartAt I (c i)) : M → E) (c i)) (r i)
x : M
hx : x ∈ s
i : ι
hi : x ∈ V i
⊢ (↑((fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) i) : M → ℝ) =ᶠ[𝓝 x] 1

Tactic:
exact ((f i).updateRIn _ _).eventuallyEq_one_of_dist_lt
      ((f i).support_subset_source <| hVf _ hi) (hr i hi).2

Premises used: And.right, SmoothBumpFunction.updateRIn, SmoothBumpFunction.eventuallyEq_one_of_dist_lt, SmoothBumpFunction.support_subset_source
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
inst_5 : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst_6 : T2Space M
inst_7 : SigmaCompactSpace M
hs : IsClosed[inst_3] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
hB :
  ∀ (x : M) (hx : x ∈ s),
    (𝓝 x).HasBasis (fun (f : SmoothBumpFunction I x) ↦ tsupport (↑f : M → ℝ) ⊆ U x) fun (f : SmoothBumpFunction I x) ↦
      support (↑f : M → ℝ)
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst_3] (V i)
hVf : ∀ (i : ι), V i ⊆ support (↑(f i) : M → ℝ)
r : (i : ι) → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (c i))).source ∩
        (↑(extChartAt I (c i)) : M → E) ⁻¹' Metric.ball ((↑(extChartAt I (c i)) : M → E) (c i)) (r i)
i : ι
⊢ tsupport (↑(toFun (s := s) (mk (s := s) c (fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) hcs ⋯ ⋯) i) : M → ℝ) ⊆
    U
      (SmoothBumpCovering.c.{uM, uE, uH, uM} (E := E) (H := H) (I := I) (s := s)
        (mk (s := s) c (fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) hcs ⋯ ⋯) i)

Tactic:
simpa only [SmoothBumpFunction.support_updateRIn, tsupport] using hfU i

Premises used: tsupport, SmoothBumpFunction.support_updateRIn
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
⊢ LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (↑(fs.toFun (s := s) i) : M → ℝ)

Tactic:
fs.locallyFinite'

Premises used: SmoothBumpCovering.locallyFinite'
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
x : M
⊢ Set.Finite.{uι} (α := ι) {i : ι | (↑(fs.toFun (s := s) i) : M → ℝ) x ≠ 0}

Tactic:
fs.locallyFinite.point_finite x

Premises used: Set.Mem, setOf, LocallyFinite.point_finite, Function.support, SmoothBumpCovering.locallyFinite, Not
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ (↑(fs.toFun (s := s) (fs.ind (s := s) x hx)) : M → ℝ) =ᶠ[𝓝 x] 1

Tactic:
(fs.eventuallyEq_one' x hx).choose_spec

Premises used: Exists.choose_spec, SmoothBumpCovering.eventuallyEq_one', SmoothBumpCovering.ind
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ (↑(fs.toFun (s := s) (fs.ind (s := s) x hx)) : M → ℝ) x = 1

Tactic:
(fs.eventuallyEq_one x hx).eq_of_nhds

Premises used: Filter.EventuallyEq.eq_of_nhds, SmoothBumpCovering.eventuallyEq_one
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ x ∈ support (↑(fs.toFun (s := s) (fs.ind (s := s) x hx)) : M → ℝ)

Tactic:
simp [fs.apply_ind x hx]

Premises used: SmoothBumpCovering.apply_ind
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : (↑(fs.toFun (s := s) i) : M → ℝ) x = 1
⊢ x ∈ support (↑(fs.toFun (s := s) i) : M → ℝ)

Tactic:
simp [h]
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : (↑(fs.toFun (s := s) i) : M → ℝ) x = 1
rw : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (fs.c (s := s) i))).source
⊢ x ∈ (extChartAt I (fs.c (s := s) i)).source

Tactic:
rw [extChartAt_source]

Premises used: extChartAt_source
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : (↑(fs.toFun (s := s) i) : M → ℝ) x = 1
⊢ x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (fs.c (s := s) i))).source

Tactic:
fs.mem_chartAt_source_of_eq_one h

Premises used: SmoothBumpCovering.mem_chartAt_source_of_eq_one
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : (↑(fs.toFun (s := s) i) : M → ℝ) x = 1
⊢ x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (fs.c (s := s) i))).source

Tactic:
exact fs.mem_chartAt_source_of_eq_one h

Premises used: SmoothBumpCovering.mem_chartAt_source_of_eq_one
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (fs.c (s := s) (fs.ind (s := s) x hx)))).source

Tactic:
fs.mem_chartAt_source_of_eq_one (fs.apply_ind x hx)

Premises used: SmoothBumpCovering.apply_ind, SmoothBumpCovering.mem_chartAt_source_of_eq_one
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ x ∈ (extChartAt I (fs.c (s := s) (fs.ind (s := s) x hx))).source

Tactic:
fs.mem_extChartAt_source_of_eq_one (fs.apply_ind x hx)

Premises used: SmoothBumpCovering.mem_extChartAt_source_of_eq_one, SmoothBumpCovering.apply_ind
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
f : SmoothBumpCovering ι I M s
U : M → Set M
⊢ (f.toBumpCovering (s := s).IsSubordinate (s := s) fun (i : ι) ↦ U (f.c (s := s) i)) ↔ f.IsSubordinate (s := s) U

Tactic:
Iff.rfl

Premises used: Set.indicator, BumpCovering.IsSubordinate, Iff.rfl, SmoothBumpFunction.toFun, SmoothBumpCovering.IsSubordinate, ite
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
i : ι
x : M
⊢ (((fs.toSmoothPartitionOfUnity (s := s) : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)
      x =
    (↑(fs.toFun (s := s) i) : M → ℝ) x * ∏ᶠ (j : ι) (_ : WellOrderingRel j i), (1 - (↑(fs.toFun (s := s) j) : M → ℝ) x)

Tactic:
rfl

Premises used: Set.indicator, SmoothBumpFunction.toFun, BumpCovering.toPOUFun, rfl, ite
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
i : ι
x : M
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (↑(fs.toFun (s := s) j) : M → ℝ) x ≠ 0 → j ∈ t
⊢ (((fs.toSmoothPartitionOfUnity (s := s) : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)
      x =
    (↑(fs.toFun (s := s) i) : M → ℝ) x * ∏ j ∈ t with WellOrderingRel j i, (1 - (↑(fs.toFun (s := s) j) : M → ℝ) x)

Tactic:
fs.toBumpCovering.toPartitionOfUnity_eq_mul_prod i x t ht

Premises used: Set.indicator, BumpCovering.toPartitionOfUnity_eq_mul_prod, SmoothBumpFunction.toFun, BumpCovering.toPOUFun, SmoothBumpCovering.toBumpCovering, ite
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
i : ι
x : M
⊢ ∃ (t : Finset ι),
    (⇑((fs.toSmoothPartitionOfUnity (s := s) : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) :
        (a : M) → ℝ) =ᶠ[𝓝 x]
      (↑(fs.toFun (s := s) i) : M → ℝ) * ∏ j ∈ t with WellOrderingRel j i, (1 - (↑(fs.toFun (s := s) j) : M → ℝ))

Tactic:
simpa using fs.toBumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq i x

Premises used: BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq, SmoothBumpCovering.toBumpCovering
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
i : ι
x : M
h : (↑(fs.toFun (s := s) i) : M → ℝ) x = 0
⊢ Eq (α := ℝ)
    ((((fs.toSmoothPartitionOfUnity (s := s) : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) :
          (a : M) → ℝ)
        x :
      ℝ)
    (0 : ℝ)

Tactic:
fs.toBumpCovering.toPartitionOfUnity_zero_of_zero h

Premises used: BumpCovering.toPartitionOfUnity_zero_of_zero, BumpCovering.toPOUFun, SmoothBumpCovering.toBumpCovering
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
i : ι
⊢ support (M := ℝ)
      (⇑((fs.toSmoothPartitionOfUnity (s := s) : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) :
        (a : M) → ℝ) ⊆
    support (↑(fs.toFun (s := s) i) : M → ℝ)

Tactic:
fs.toBumpCovering.support_toPartitionOfUnity_subset i

Premises used: Set.indicator, SmoothBumpFunction.toFun, BumpCovering.toPOUFun, SmoothBumpCovering.toBumpCovering, BumpCovering.support_toPartitionOfUnity_subset, ite
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
f : SmoothBumpCovering ι I M s
U : M → Set M
h : f.IsSubordinate (s := s) U
⊢ f.toSmoothPartitionOfUnity (s := s).IsSubordinate (s := s) fun (i : ι) ↦ U (f.c (s := s) i)

Tactic:
h.toBumpCovering.toPartitionOfUnity

Premises used: SmoothBumpCovering.IsSubordinate.toBumpCovering, PartitionOfUnity.IsSubordinate, BumpCovering.toPOUFun, BumpCovering.IsSubordinate.toPartitionOfUnity, SmoothPartitionOfUnity.IsSubordinate
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
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
inst_5 : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
x : M
⊢ ∑ᶠ (i : ι),
      (((fs.toSmoothPartitionOfUnity (s := s) : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) :
          (a : M) → ℝ)
        x =
    HSub.hSub (α := ℝ) 1 (∏ᶠ (i : ι), (1 - (↑(fs.toFun (s := s) i) : M → ℝ) x))

Tactic:
fs.toBumpCovering.sum_toPartitionOfUnity_eq x

Premises used: Set.indicator, SmoothBumpFunction.toFun, BumpCovering.toPOUFun, BumpCovering.sum_toPartitionOfUnity_eq, SmoothBumpCovering.toBumpCovering, ite
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
n : ℕ∞
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
⊢ ∀ x ∈ t, sᶜ ∈ 𝓝 x

Tactic:
have : ∀ x ∈ t, sᶜ ∈ 𝓝 x := fun x hx => hs.isOpen_compl.mem_nhds (disjoint_right.1 hd hx)
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
n : ℕ∞
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
rcases :
  ∀ (ι : Type uM) (f : SmoothBumpCovering ι I M t) (hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ),
    ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
      EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
        EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
          ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
      EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)

Tactic:
rcases SmoothBumpCovering.exists_isSubordinate I ht this with ⟨ι, f, hf⟩

Premises used: SmoothBumpCovering.exists_isSubordinate
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
n : ℕ∞
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity (s := t)
⊢ (↑n : ℕ∞ω) ≤ ∞

Tactic:
simp