awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht :
  Set.Finite.{u} (α := ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          t).Nonempty}
i : ι
hi :
  Membership.mem (γ := Set ι)
    {i : ι | Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀}
    i
simp :
  Membership.mem (γ := Set ι)
    {i : ι | (t ∩ support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)).Nonempty} i
⊢ Membership.mem (γ := Set ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          t).Nonempty}
    i

Tactic:
simp only [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht :
  Set.Finite.{u} (α := ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          t).Nonempty}
i : ι
hi :
  Membership.mem (γ := Set ι)
    {i : ι | Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀}
    i
⊢ Membership.mem (γ := Set ι)
    {i : ι | (t ∩ support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)).Nonempty} i

Tactic:
mem_closure_iff_nhds.mp hi t t_in

Premises used: mem_closure_iff_nhds, Set.Mem, setOf, Set.Nonempty, Iff.mp
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht :
  Set.Finite.{u} (α := ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          t).Nonempty}
i : ι
hi :
  Membership.mem (γ := Set ι)
    {i : ι | Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀}
    i
⊢ Membership.mem (γ := Set ι)
    {i : ι | (t ∩ support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)).Nonempty} i

Tactic:
exact mem_closure_iff_nhds.mp hi t t_in

Premises used: mem_closure_iff_nhds, Iff.mp
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
⊢ i ∈ ρ.fintsupport (s := s) x₀ ↔
    Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀

Tactic:
Finite.mem_toFinset _

Premises used: Set.Mem, Set.Finite.mem_toFinset, setOf, tsupport, closure, Set.sInter
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
apply :
  ∀ (x : X),
    Subset.{u} (α := Set ι)
        {i : ι |
          Membership.mem (γ := Set X)
            (closure[inst] (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))) x}
        {i : ι |
          Membership.mem (γ := Set X)
            (closure[inst] (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))) x₀} →
      ρ.fintsupport (s := s) x ⊆ ρ.fintsupport (s := s) x₀
⊢ ∀ᶠ (y : X) in 𝓝 x₀, ρ.fintsupport (s := s) y ⊆ ρ.fintsupport (s := s) x₀

Tactic:
apply (ρ.locallyFinite.closure.eventually_subset (fun _ ↦ isClosed_closure) x₀).mono

Premises used: PartitionOfUnity.locallyFinite, LocallyFinite.closure, Filter.Eventually.mono, isClosed_closure, LocallyFinite.eventually_subset
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ y : X
hy :
  Subset.{u} (α := Set ι)
    {i : ι |
      Membership.mem (γ := Set X)
        (closure[inst] (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))) y}
    {i : ι |
      Membership.mem (γ := Set X)
        (closure[inst] (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))) x₀}
z : ι
hz : z ∈ ρ.fintsupport (s := s) y
rw :
  ∀ (hz : Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) z : C(X, ℝ)) : (a : X) → ℝ)) y),
    Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) z : C(X, ℝ)) : (a : X) → ℝ)) x₀
⊢ z ∈ ρ.fintsupport (s := s) x₀

Tactic:
rw [PartitionOfUnity.mem_fintsupport_iff] at *

Premises used: PartitionOfUnity.mem_fintsupport_iff
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ y : X
hy :
  Subset.{u} (α := Set ι)
    {i : ι |
      Membership.mem (γ := Set X)
        (closure[inst] (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))) y}
    {i : ι |
      Membership.mem (γ := Set X)
        (closure[inst] (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))) x₀}
z : ι
hz : Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) z : C(X, ℝ)) : (a : X) → ℝ)) y
⊢ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) z : C(X, ℝ)) : (a : X) → ℝ)) x₀

Tactic:
hy hz

Premises used: Set.Mem, setOf, tsupport, closure, Set.sInter
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ y : X
hy :
  Subset.{u} (α := Set ι)
    {i : ι |
      Membership.mem (γ := Set X)
        (closure[inst] (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))) y}
    {i : ι |
      Membership.mem (γ := Set X)
        (closure[inst] (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))) x₀}
z : ι
hz : Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) z : C(X, ℝ)) : (a : X) → ℝ)) y
⊢ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) z : C(X, ℝ)) : (a : X) → ℝ)) x₀

Tactic:
exact hy hz
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport (s := s) x₀
rw : Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀
⊢ i ∈ ρ.fintsupport (s := s) x₀

Tactic:
rw [ρ.mem_fintsupport_iff]

Premises used: PartitionOfUnity.mem_fintsupport_iff
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport (s := s) x₀
a : Membership.mem (γ := Set X) (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀
⊢ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀

Tactic:
apply subset_closure

Premises used: subset_closure
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport (s := s) x₀
⊢ Membership.mem (γ := Set X) (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀

Tactic:
(ρ.mem_finsupport x₀).mp hi

Premises used: Set.Mem, setOf, Function.support, Iff.mp, PartitionOfUnity.mem_finsupport
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport (s := s) x₀
⊢ Membership.mem (γ := Set X) (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀

Tactic:
exact (ρ.mem_finsupport x₀).mp hi

Premises used: Iff.mp, PartitionOfUnity.mem_finsupport
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ∀ᶠ (y : X) in 𝓝 x₀, ρ.finsupport (s := s) y ⊆ ρ.fintsupport (s := s) x₀

Tactic:
(ρ.eventually_fintsupport_subset x₀).mono
    fun y hy ↦ (ρ.finsupport_subset_fintsupport y).trans hy

Premises used: PartitionOfUnity.eventually_fintsupport_subset, HasSubset.Subset.trans, Filter.Eventually.mono, PartitionOfUnity.finsupport_subset_fintsupport
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
E : Type u_1
inst_1 : AddCommMonoid E
inst_2 : SMulWithZero ℝ E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
g : X → E
i : ι
hg :
  ∀ (x : X),
    Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x →
      ContinuousAt g x
⊢ Continuous[inst, inst_3] fun (x : X) ↦
    HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (g x)

Tactic:
continuous_of_tsupport fun x hx =>
    ((f i).continuousAt x).smul <| hg x <| tsupport_smul_subset_left _ _ hx

Premises used: continuous_of_tsupport, ContinuousAt.smul, DFunLike.coe, ContinuousMap.continuousAt, tsupport_smul_subset_left
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
E : Type u_1
inst_1 : AddCommMonoid E
inst_2 : SMulWithZero ℝ E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
inst_5 : ContinuousAdd E
g : ι → X → E
hg :
  ∀ (i : ι) (x : X),
    Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x →
      ContinuousAt (g i) x
⊢ Continuous[inst, inst_3] fun (x : X) ↦
    ∑ᶠ (i : ι), HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (g i x)

Tactic:
(continuous_finsum fun i => f.continuous_smul (hg i)) <|
    f.locallyFinite.subset fun _ => support_smul_subset_left _ _

Premises used: continuous_finsum, Function.support_smul_subset_left, PartitionOfUnity.locallyFinite, LocallyFinite.subset, DFunLike.coe, PartitionOfUnity.continuous_smul
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
rcases :
  ∀ (I : Finset ι)
    (hI :
      ∀ᶠ (x : X) in 𝓝 x₀,
        (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)),
    ∃ (I : Finset ι),
      (∀ᶠ (x : X) in 𝓝[s] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
        ∀ᶠ (x : X) in 𝓝 x₀,
          (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
⊢ ∃ (I : Finset ι),
    (∀ᶠ (x : X) in 𝓝[s] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
      ∀ᶠ (x : X) in 𝓝 x₀,
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)

Tactic:
rcases ρ.locallyFinite.exists_finset_support x₀ with ⟨I, hI⟩

Premises used: PartitionOfUnity.locallyFinite, LocallyFinite.exists_finset_support
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI :
  ∀ᶠ (x : X) in 𝓝 x₀,
    (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
⊢ ∃ (I : Finset ι),
    (∀ᶠ (x : X) in 𝓝[s] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
      ∀ᶠ (x : X) in 𝓝 x₀,
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)

Tactic:
⟨I, eventually_nhdsWithin_iff.mpr (hI.mono fun x hx x_in ↦ ?_), hI⟩

Premises used: Iff.mpr, Filter.Eventually.mono, eventually_nhdsWithin_iff, And.intro, Exists.intro
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI :
  ∀ᶠ (x : X) in 𝓝 x₀,
    (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
refine :
  ∀ (x : X)
    (hx : (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι))
    (x_in : x ∈ s), Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
⊢ ∃ (I : Finset ι),
    (∀ᶠ (x : X) in 𝓝[s] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
      ∀ᶠ (x : X) in 𝓝 x₀,
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)

Tactic:
refine ⟨I, eventually_nhdsWithin_iff.mpr (hI.mono fun x hx x_in ↦ ?_), hI⟩
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI :
  ∀ᶠ (x : X) in 𝓝 x₀,
    (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
x : X
hx : (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
x_in : x ∈ s
⊢ Eq (α := ℝ) (∑ᶠ (i : ι), (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
    (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)

Tactic:
have : ∑ᶠ i : ι, ρ i x = ∑ i ∈ I, ρ i x := finsum_eq_sum_of_support_subset _ hx
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI :
  ∀ᶠ (x : X) in 𝓝 x₀,
    (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
x : X
hx : (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
x_in : x ∈ s
this :
  Eq (α := ℝ) (∑ᶠ (i : ι), (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
    (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
rwa :
  ∀
    (this :
      Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
        (∑ᶠ (i : ι), (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)),
    Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1),
    Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1

Tactic:
rwa [eq_comm, ρ.sum_eq_one x_in] at this

Premises used: PartitionOfUnity.sum_eq_one, eq_comm
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
rcases :
  ∀ (I : Finset ι)
    (H :
      (∀ᶠ (x : X) in 𝓝[univ] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
        ∀ᶠ (x : X) in 𝓝 x₀,
          (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)),
    ∃ (I : Finset ι),
      ∀ᶠ (x : X) in 𝓝 x₀,
        Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
          (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
⊢ ∃ (I : Finset ι),
    ∀ᶠ (x : X) in 𝓝 x₀,
      Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)

Tactic:
rcases ρ.exists_finset_nhds' x₀ with ⟨I, H⟩

Premises used: PartitionOfUnity.exists_finset_nhds'
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
I : Finset ι
H :
  (∀ᶠ (x : X) in 𝓝[univ] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
    ∀ᶠ (x : X) in 𝓝 x₀,
      (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
h :
  ∀ᶠ (x : X) in 𝓝 x₀,
    Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
      (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
⊢ ∃ (I : Finset ι),
    ∀ᶠ (x : X) in 𝓝 x₀,
      Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)

Tactic:
use I
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
I : Finset ι
H :
  (∀ᶠ (x : X) in 𝓝[univ] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
    ∀ᶠ (x : X) in 𝓝 x₀,
      (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
h :
  ∀
    (H :
      (∀ᶠ (x : X) in 𝓝 x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
        ∀ᶠ (x : X) in 𝓝 x₀,
          (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)),
    ∀ᶠ (x : X) in 𝓝 x₀,
      Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
h₁ h₂ h₃ h₄ :
  ∀
    (H :
      ∀ᶠ (x : X) in 𝓝 x₀,
        Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
          (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)),
    ∀ᶠ (x : X) in 𝓝 x₀,
      Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
⊢ ∀ᶠ (x : X) in 𝓝 x₀,
    Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
      (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)

Tactic:
rwa [nhdsWithin_univ, ← eventually_and] at H

Premises used: Filter.eventually_and, nhdsWithin_univ
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
U : ι → Set X
hso : f.IsSubordinate (s := s) U
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
⊢ ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x,
      n ⊆ ⋂ i ∈ is, U i ∧
        ∀ z ∈ n,
          (support (M := ℝ) fun (x : ι) ↦ (((f : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) z) ⊆ (↑is : Set ι)

Tactic:
f.locallyFinite.exists_finset_nhds_support_subset hso ho x

Premises used: PartitionOfUnity.locallyFinite, LocallyFinite.exists_finset_nhds_support_subset
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
E : Type u_1
inst_1 : AddCommMonoid E
inst_2 : SMulWithZero ℝ E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
inst_5 : ContinuousAdd E
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : f.IsSubordinate (s := s) U
g : ι → X → E
hg : ∀ (i : ι), ContinuousOn (g i) (U i)
⊢ Continuous[inst, inst_3] fun (x : X) ↦
    ∑ᶠ (i : ι), HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (g i x)

Tactic:
f.continuous_finsum_smul fun i _ hx => (hg i).continuousAt <| (ho i).mem_nhds <| hf i hx

Premises used: PartitionOfUnity.continuous_finsum_smul, IsOpen.mem_nhds, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f_1 f g : BumpCovering ι X s
h : f.toFun (s := s) = g.toFun (s := s)
mk :
  ∀ (toFun : ι → C(X, ℝ))
    (locallyFinite' : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : X) → ℝ))
    (nonneg' : 0 ≤ toFun) (le_one' : toFun ≤ 1)
    (eventuallyEq_one' : ∀ x ∈ s, ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(toFun i) : (a : X) → ℝ) 1)
    (h :
      (BumpCovering.mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one').toFun (s := s) =
        g.toFun (s := s)),
    BumpCovering.mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one' = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f g : BumpCovering ι X s
toFun : ι → C(X, ℝ)
locallyFinite' : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : X) → ℝ)
nonneg' : 0 ≤ toFun
le_one' : toFun ≤ 1
eventuallyEq_one' : ∀ x ∈ s, ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(toFun i) : (a : X) → ℝ) 1
h : (BumpCovering.mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one').toFun (s := s) = g.toFun (s := s)
mk :
  ∀ (toFun_1 : ι → C(X, ℝ))
    (locallyFinite'_1 : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun_1 i) : (a : X) → ℝ))
    (nonneg'_1 : 0 ≤ toFun_1) (le_one'_1 : toFun_1 ≤ 1)
    (eventuallyEq_one'_1 : ∀ x ∈ s, ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(toFun_1 i) : (a : X) → ℝ) 1)
    (h :
      (BumpCovering.mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one').toFun (s := s) =
        (BumpCovering.mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 le_one'_1 eventuallyEq_one'_1).toFun (s := s)),
    BumpCovering.mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one' =
      BumpCovering.mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 le_one'_1 eventuallyEq_one'_1
⊢ BumpCovering.mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one' = g

Tactic:
cases g
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
toFun : ι → C(X, ℝ)
locallyFinite' : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : X) → ℝ)
nonneg' : 0 ≤ toFun
le_one' : toFun ≤ 1
eventuallyEq_one' : ∀ x ∈ s, ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(toFun i) : (a : X) → ℝ) 1
toFun_1 : ι → C(X, ℝ)
locallyFinite'_1 : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun_1 i) : (a : X) → ℝ)
nonneg'_1 : 0 ≤ toFun_1
le_one'_1 : toFun_1 ≤ 1
eventuallyEq_one'_1 : ∀ x ∈ s, ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(toFun_1 i) : (a : X) → ℝ) 1
h :
  (mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one').toFun (s := s) =
    (mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 le_one'_1 eventuallyEq_one'_1).toFun (s := s)
⊢ mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one' =
    mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 le_one'_1 eventuallyEq_one'_1

Tactic:
congr
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
⊢ f.toFun (s := s) = (⇑f : (a : ι) → C(X, ℝ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
⊢ LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
f.locallyFinite'

Premises used: BumpCovering.locallyFinite'
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
⊢ LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ tsupport (α := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
f.locallyFinite.closure

Premises used: LocallyFinite.closure, tsupport, BumpCovering.locallyFinite
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
⊢ Set.Finite.{u} (α := ι) {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}

Tactic:
f.locallyFinite.point_finite x

Premises used: Set.Mem, setOf, BumpCovering.locallyFinite, LocallyFinite.point_finite, Function.support, Not
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
⊢ LE.le (α := ℝ) (0 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)

Tactic:
f.nonneg' i x

Premises used: BumpCovering.nonneg'