awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : Set M
ρ : SmoothPartitionOfUnity ι I M s
x₀ : M
A : Type u_1
inst_5 : AddCommGroup A
inst_6 : Module ℝ A
φ : ι → M → A
⊢ Eq.{u_1 + 1} (α := A)
    (∑ i ∈ ρ.finsupport (s := s) x₀,
      HSMul.hSMul (α := ℝ) ((((ρ : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x₀ : ℝ)
        (φ i x₀))
    (∑ᶠ (i : ι),
      HSMul.hSMul (α := ℝ) ((((ρ : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x₀ : ℝ)
        (φ i x₀))

Tactic:
ρ.toPartitionOfUnity.sum_finsupport_smul_eq_finsum φ

Premises used: SmoothPartitionOfUnity.toPartitionOfUnity, PartitionOfUnity.sum_finsupport_smul_eq_finsum, SmoothPartitionOfUnity.finsupport
-- 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
s : Set M
ρ : SmoothPartitionOfUnity ι I M s
x₀ : M
⊢ Set.Finite.{uι} (α := ι)
    {i : ι |
      Membership.mem (γ := Set M)
        (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x₀}

Tactic:
ρ.toPartitionOfUnity.finite_tsupport _

Premises used: Set.Mem, setOf, SmoothPartitionOfUnity.toPartitionOfUnity, PartitionOfUnity.finite_tsupport
-- 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
s : Set M
ρ : SmoothPartitionOfUnity ι I M s
x₀ : M
i : ι
⊢ i ∈ ρ.fintsupport (s := s) x₀ ↔
    Membership.mem (γ := Set M)
      (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x₀

Tactic:
Finite.mem_toFinset _

Premises used: Set.Mem, Set.Finite.mem_toFinset, setOf, tsupport, closure, Set.sInter
-- 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
s : Set M
ρ : SmoothPartitionOfUnity ι I M s
x₀ : M
⊢ ∀ᶠ (y : M) in 𝓝 x₀, ρ.fintsupport (s := s) y ⊆ ρ.fintsupport (s := s) x₀

Tactic:
ρ.toPartitionOfUnity.eventually_fintsupport_subset _

Premises used: Set.Mem, PartitionOfUnity.eventually_fintsupport_subset, setOf, SmoothPartitionOfUnity.toPartitionOfUnity
-- 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
s : Set M
ρ : SmoothPartitionOfUnity ι I M s
x₀ : M
⊢ ρ.finsupport (s := s) x₀ ⊆ ρ.fintsupport (s := s) x₀

Tactic:
ρ.toPartitionOfUnity.finsupport_subset_fintsupport x₀

Premises used: Set.Mem, setOf, SmoothPartitionOfUnity.toPartitionOfUnity, PartitionOfUnity.finsupport_subset_fintsupport
-- 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
s : Set M
ρ : SmoothPartitionOfUnity ι I M s
x₀ : M
⊢ ∀ᶠ (y : M) in 𝓝 x₀, ρ.finsupport (s := s) y ⊆ ρ.fintsupport (s := s) x₀

Tactic:
ρ.toPartitionOfUnity.eventually_finsupport_subset x₀

Premises used: Set.Mem, setOf, SmoothPartitionOfUnity.toPartitionOfUnity, PartitionOfUnity.eventually_finsupport_subset
-- 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
s : Set M
f : SmoothPartitionOfUnity ι I M s
U : ι → Set M
⊢ f.toPartitionOfUnity (s := s).IsSubordinate (s := s) U ↔ f.IsSubordinate (s := s) U

Tactic:
Iff.rfl

Premises used: Iff.rfl, PartitionOfUnity.IsSubordinate, SmoothPartitionOfUnity.IsSubordinate
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type uF
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type uH
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
U : ι → Set M
g : ι → M → F
hf : f.IsSubordinate (s := s) U
ho : ∀ (i : ι), IsOpen[inst_5] (U i)
hg : ∀ (i : ι), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) (g i) (U i)
⊢ ContMDiff I 𝓘(ℝ, F) (M' := F) (↑n : ℕ∞ω) fun (x : M) ↦
    ∑ᶠ (i : ι),
      HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g i x)

Tactic:
f.contMDiff_finsum_smul fun i _ hx ↦ (hg i).contMDiffAt <| (ho i).mem_nhds (hf i hx)

Premises used: ContMDiffOn.contMDiffAt, IsOpen.mem_nhds, SmoothPartitionOfUnity.contMDiff_finsum_smul
-- 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
s : Set M
f : BumpCovering ι M s
hf :
  ∀ (i : ι),
    ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
      (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)
i : ι
simp :
  LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (M := ℝ) (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)
⊢ LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦
    mulSupport (M := ℝ) fun (x : M) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ) x : ℝ)

Tactic:
simp only [mulSupport_one_sub]

Premises used: Function.mulSupport_one_sub
-- 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
s : Set M
f : BumpCovering ι M s
hf :
  ∀ (i : ι),
    ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
      (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)
i : ι
⊢ LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (M := ℝ) (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)

Tactic:
f.locallyFinite

Premises used: BumpCovering.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
s : Set M
f : BumpCovering ι M s
hf :
  ∀ (i : ι),
    ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
      (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)
i : ι
⊢ LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (M := ℝ) (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)

Tactic:
exact f.locallyFinite

Premises used: BumpCovering.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
s : Set M
f : BumpCovering ι M s
hf :
  ∀ (i : ι),
    ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
      (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)
⊢ (f.toSmoothPartitionOfUnity (s := s) hf).toPartitionOfUnity (s := s) = f.toPartitionOfUnity (s := s)

Tactic:
rfl

Premises used: SmoothPartitionOfUnity.toPartitionOfUnity, toContinuousMap, BumpCovering.toPOUFun, BumpCovering.toPartitionOfUnity, rfl
-- 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
s : Set M
f : BumpCovering ι M s
hf :
  ∀ (i : ι),
    ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
      (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)
i : ι
⊢ Eq.{uM + 1} (α := (a : M) → ℝ)
    (⇑((f.toSmoothPartitionOfUnity (s := s) hf : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) :
      (a : M) → ℝ)
    (⇑((f.toPartitionOfUnity (s := s) : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)

Tactic:
rfl

Premises used: BumpCovering.toPOUFun, rfl
-- 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
s : Set M
f : BumpCovering ι M s
U : ι → Set M
h : f.IsSubordinate (s := s) U
hf :
  ∀ (i : ι),
    ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
      (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)
⊢ (f.toSmoothPartitionOfUnity (s := s) hf).IsSubordinate (s := s) U

Tactic:
h.toPartitionOfUnity

Premises used: 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
U : M → Set M
h : fs.IsSubordinate (s := s) U
i : ι
⊢ support (↑(fs.toFun (s := s) i) : M → ℝ) ⊆ U (fs.c (s := s) i)

Tactic:
Subset.trans subset_closure (h i)

Premises used: Set.Subset.trans, subset_closure
-- 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
⊢ LocallyCompactSpace H

Tactic:
haveI : LocallyCompactSpace H := I.locallyCompactSpace
-- 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 : LocallyCompactSpace H
⊢ LocallyCompactSpace M

Tactic:
haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
-- 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
⊢ ∀ (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 → ℝ)

Tactic:
have hB := fun x hx => SmoothBumpFunction.nhds_basis_support (I := I) (hU x 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
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 → ℝ)
rcases :
  ∀ (ι : Type uM) (c : ι → M) (f : (a : ι) → SmoothBumpFunction I (c a))
    (hf : ∀ (a : ι), c a ∈ s ∧ tsupport (↑(f a) : M → ℝ) ⊆ U (c a)) (hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ))
    (hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)),
    ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U

Tactic:
rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs hB with
    ⟨ι, c, f, hf, hsub', hfin⟩

Premises used: SmoothBumpCovering.c, refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set
-- 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)
hf : ∀ (a : ι), c a ∈ s ∧ tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
⊢ ∀ (a : ι), c a ∈ s

Tactic:
choose hcs hfU using hf
-- 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)
hf : ∀ (a : ι), c a ∈ s ∧ tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
⊢ ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)

Tactic:
choose hcs hfU using hf
-- 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)
rcases :
  ∀ (V : ι → Set M) (hsV : s ⊆ iUnion V) (hVc : ∀ (i : ι), IsClosed[inst_3] (V i))
    (hVf : ∀ (i : ι), V i ⊆ support (↑(f i) : M → ℝ)),
    ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U

Tactic:
rcases exists_subset_iUnion_closed_subset hs (fun i => (f i).isOpen_support)
    (fun x _ => hfin.point_finite x) hsub' with ⟨V, hsV, hVc, hVf⟩

Premises used: exists_subset_iUnion_closed_subset, LocallyFinite.point_finite, SmoothBumpFunction.isOpen_support
-- 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 → ℝ)
choose :
  ∀ (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)),
    ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U

Tactic:
choose r hrR hr using fun i => (f i).exists_r_pos_lt_subset_ball (hVc i) (hVf i)

Premises used: SmoothBumpFunction.exists_r_pos_lt_subset_ball
-- 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)
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U

Tactic:
⟨ι, ⟨c, fun i => (f i).updateRIn (r i) (hrR i), hcs, ?_, fun x hx => ?_⟩, fun i => ?_⟩

Premises used: SmoothBumpCovering.mk, SmoothBumpFunction.updateRIn, Exists.intro
-- 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)
refine_1 : LocallyFinite (X := M) fun (i : ι) ↦ support (↑((fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) i) : M → ℝ)
refine_2 : ∀ (x : M) (hx : x ∈ s), ∃ (i : ι), (↑((fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) i) : M → ℝ) =ᶠ[𝓝 x] 1
refine_3 :
  ∀ (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)
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U

Tactic:
refine ⟨ι, ⟨c, fun i => (f i).updateRIn (r i) (hrR i), hcs, ?_, fun x hx => ?_⟩, fun i => ?_⟩
-- 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)
⊢ LocallyFinite (X := M) fun (i : ι) ↦ support (↑((fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) i) : M → ℝ)

Tactic:
simpa only [SmoothBumpFunction.support_updateRIn]

Premises used: SmoothBumpFunction.support_updateRIn