awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf :
  Set.Finite.{u} (α := ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          U).Nonempty}
y : X
hyU : y ∈ U
j : ι
h :
  WellOrderingRel j i →
    Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) y : ℝ) (0 : ℝ) →
      j ∈
        hf.toFinset (s :=
          {i : ι | (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ∩ U).Nonempty})
⊢ WellOrderingRel j i →
    Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) y : ℝ) (0 : ℝ) →
      j ∈
        hf.toFinset (s :=
          {i : ι | (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ∩ U).Nonempty})

Tactic:
_
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf :
  Set.Finite.{u} (α := ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          U).Nonempty}
y : X
hyU : y ∈ U
j : ι
h : WellOrderingRel j i
hj : Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) y : ℝ) (0 : ℝ)
⊢ j ∈
    hf.toFinset (s := {i : ι | (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ∩ U).Nonempty})

Tactic:
hf.mem_toFinset.2 ⟨y, ⟨hj, hyU⟩⟩

Premises used: Iff.mpr, Set.Mem, Set.Finite.mem_toFinset, setOf, And.intro, Exists.intro
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf :
  Set.Finite.{u} (α := ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          U).Nonempty}
y : X
hyU : y ∈ U
j : ι
h : WellOrderingRel j i
hj : Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) y : ℝ) (0 : ℝ)
⊢ j ∈
    hf.toFinset (s := {i : ι | (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ∩ U).Nonempty})

Tactic:
exact hf.mem_toFinset.2 ⟨y, ⟨hj, hyU⟩⟩

Premises used: Iff.mpr, Set.Finite.mem_toFinset, And.intro, Exists.intro
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i j : ι
h : WellOrderingRel j i
⊢ Continuous[inst, _] fun (x : X) ↦
    HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
refine :
  LocallyFinite.{u, v} (X := X) fun (i : ι) ↦
    mulSupport (M := ℝ) fun (x : X) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
⊢ Continuous[inst, _] (f.toPOUFun (s := s) i)

Tactic:
refine (map_continuous <| f i).mul <| continuous_finprod_cond (fun j _ => by fun_prop) ?_

Premises used: Continuous.mul, continuous_finprod_cond, ContinuousMapClass.map_continuous, DFunLike.coe
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
simp :
  LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
⊢ LocallyFinite.{u, v} (X := X) fun (i : ι) ↦
    mulSupport (M := ℝ) fun (x : X) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)

Tactic:
simp only [mulSupport_one_sub]

Premises used: Function.mulSupport_one_sub
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ 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
i : ι
⊢ LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
exact 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
x : X
hx : x ∈ s
simp :
  Eq (α := ℝ)
    (∏ᶠ (i : ι), HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) 0
⊢ Eq (α := ℝ) (∑ᶠ (i : ι), ({ toFun := f.toPOUFun (s := s) i, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x) 1

Tactic:
simp only [ContinuousMap.coe_mk, sum_toPOUFun_eq, sub_eq_self]

Premises used: sub_eq_self, ContinuousMap.coe_mk, BumpCovering.sum_toPOUFun_eq
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
hx₁ :
  HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ)
      ((((f : (a : ι) → C(X, ℝ)) (f.ind (s := s) x hx) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) =
    0
hf :
  HasFiniteMulSupport (M := ℝ) fun (i : ι) ↦
    HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
⊢ Eq (α := ℝ)
    (∏ᶠ (i : ι), HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) 0

Tactic:
apply finprod_eq_zero (fun i => 1 - f i x) (f.ind x hx)

Premises used: BumpCovering.ind, HSub.hSub, finprod_eq_zero, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ)
      ((((f : (a : ι) → C(X, ℝ)) (f.ind (s := s) x hx) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) =
    0

Tactic:
simp only [f.ind_apply x hx, sub_self]

Premises used: sub_self, BumpCovering.ind_apply
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
hf : Set.Finite.{u} (α := ι) (support (M := ℝ) fun (i : ι) ↦ (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
⊢ HasFiniteMulSupport (M := ℝ) fun (i : ι) ↦
    HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)

Tactic:
rw [HasFiniteMulSupport, mulSupport_one_sub]

Premises used: Function.mulSupport_one_sub, Function.HasFiniteMulSupport
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ Set.Finite.{u} (α := ι) (support (M := ℝ) fun (i : ι) ↦ (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)

Tactic:
f.point_finite x

Premises used: BumpCovering.point_finite, setOf, Function.support
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ Set.Finite.{u} (α := ι) (support (M := ℝ) fun (i : ι) ↦ (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)

Tactic:
exact f.point_finite x

Premises used: BumpCovering.point_finite
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
simp :
  LE.le (α := ℝ) 0
    (∏ᶠ (i : ι), HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ))
⊢ LE.le (α := ℝ) (∑ᶠ (i : ι), ({ toFun := f.toPOUFun (s := s) i, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x) 1

Tactic:
simp only [ContinuousMap.coe_mk, sum_toPOUFun_eq, sub_le_self_iff]

Premises used: ContinuousMap.coe_mk, sub_le_self_iff, BumpCovering.sum_toPOUFun_eq
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
⊢ LE.le (α := ℝ) 0
    (∏ᶠ (i : ι), HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ))

Tactic:
finprod_nonneg fun i => sub_nonneg.2 <| f.le_one i x

Premises used: Iff.mpr, finprod_nonneg, BumpCovering.le_one, sub_nonneg
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
⊢ LE.le (α := ℝ) 0
    (∏ᶠ (i : ι), HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ))

Tactic:
exact finprod_nonneg fun i => sub_nonneg.2 <| f.le_one i x

Premises used: Iff.mpr, finprod_nonneg, BumpCovering.le_one, sub_nonneg
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
⊢ (((f.toPartitionOfUnity (s := s) : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x =
    HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
      (∏ᶠ (j : ι) (_ : WellOrderingRel j i),
          HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) :
        ℝ)

Tactic:
rfl

Premises used: BumpCovering.toPOUFun, rfl
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht :
  ∀ (j : ι),
    WellOrderingRel j i → Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ) → j ∈ t
⊢ (((f.toPartitionOfUnity (s := s) : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x =
    HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
      (∏ j ∈ t with WellOrderingRel j i,
          HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) :
        ℝ)

Tactic:
f.toPOUFun_eq_mul_prod i x t ht

Premises used: BumpCovering.toPOUFun, BumpCovering.toPOUFun_eq_mul_prod
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
⊢ ∃ (t : Finset ι),
    (⇑((f.toPartitionOfUnity (s := s) : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) =ᶠ[𝓝 x]
      HMul.hMul (α := (a : X) → ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
        (⇑(∏ j ∈ t with WellOrderingRel j i,
              HSub.hSub (α := C(X, ℝ)) (β := C(X, ℝ)) (1 : C(X, ℝ)) ((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ))) :
          (a : X) → ℝ)

Tactic:
f.exists_finset_toPOUFun_eventuallyEq i x

Premises used: BumpCovering.toPOUFun, BumpCovering.exists_finset_toPOUFun_eventuallyEq
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
h : Eq (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((((f.toPartitionOfUnity (s := s) : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
f.toPOUFun_zero_of_zero h

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

Tactic:
f.support_toPOUFun_subset i

Premises used: BumpCovering.support_toPOUFun_subset, BumpCovering.toPOUFun
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
⊢ ∑ᶠ (i : ι), (((f.toPartitionOfUnity (s := s) : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x =
    HSub.hSub (α := ℝ) 1
      (∏ᶠ (i : ι), HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ))

Tactic:
f.sum_toPOUFun_eq x

Premises used: BumpCovering.toPOUFun, BumpCovering.sum_toPOUFun_eq
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
U : ι → Set X
h : f.IsSubordinate (s := s) U
⊢ f.toPartitionOfUnity (s := s).IsSubordinate (s := s) U

Tactic:
fun i => Subset.trans (closure_mono <| f.support_toPartitionOfUnity_subset i) (h i)

Premises used: Set.Subset.trans, closure_mono, PartitionOfUnity.IsSubordinate, BumpCovering.support_toPartitionOfUnity_subset
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : NormalSpace X
hs : IsClosed[inst] s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ (f : PartitionOfUnity ι X s), f.IsSubordinate (s := s) U

Tactic:
let ⟨f, hf⟩ := BumpCovering.exists_isSubordinate_of_locallyFinite hs U ho hf hU
  ⟨f.toPartitionOfUnity, hf.toPartitionOfUnity⟩

Premises used: _private.0.PartitionOfUnity.exists_isSubordinate_of_locallyFinite.match_1, Exists, PartitionOfUnity.IsSubordinate, BumpCovering.IsSubordinate.toPartitionOfUnity, Exists.intro, BumpCovering.exists_isSubordinate_of_locallyFinite, BumpCovering.toPartitionOfUnity
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : NormalSpace X
inst_2 : ParacompactSpace X
hs : IsClosed[inst] s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ (f : PartitionOfUnity ι X s), f.IsSubordinate (s := s) U

Tactic:
let ⟨f, hf⟩ := BumpCovering.exists_isSubordinate hs U ho hU
  ⟨f.toPartitionOfUnity, hf.toPartitionOfUnity⟩

Premises used: _private.0.PartitionOfUnity.exists_isSubordinate_of_locallyFinite.match_1, Exists, PartitionOfUnity.IsSubordinate, BumpCovering.IsSubordinate.toPartitionOfUnity, Exists.intro, BumpCovering.toPartitionOfUnity, BumpCovering.exists_isSubordinate
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : LocallyCompactSpace X
inst_2 : T2Space X
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ (f : PartitionOfUnity ι X s),
    f.IsSubordinate (s := s) U ∧
      ∀ (i : ι), HasCompactSupport.{v, 0} (α := X) (β := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
let ⟨f, hfsub, hfcp⟩ :=
    BumpCovering.exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space hs U ho hf hU
  ⟨f.toPartitionOfUnity, hfsub.toPartitionOfUnity, fun i => IsCompact.of_isClosed_subset (hfcp i)
    isClosed_closure <| closure_mono (f.support_toPartitionOfUnity_subset i)⟩

Premises used: Exists, closure_mono, PartitionOfUnity.IsSubordinate, And, IsCompact.of_isClosed_subset, BumpCovering.IsSubordinate.toPartitionOfUnity, And.intro, Exists.intro, BumpCovering.toPartitionOfUnity, isClosed_closure, _private.0.PartitionOfUnity.exists_isSubordinate_of_locallyFinite_t2space.match_1, BumpCovering.exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space, BumpCovering.support_toPartitionOfUnity_subset
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ (i : Fin n), s i
obtain :
  ∀ (f : PartitionOfUnity (Fin n) X t) (hfsub : f.IsSubordinate (s := t) s)
    (hfcp :
      ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)),
    ∃ (f : Fin n → C(X, ℝ)),
      (∀ (i : Fin n), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ s i) ∧
        EqOn (β := ℝ) (∑ i : Fin n, (⇑(f i) : (a : X) → ℝ)) 1 t ∧
          (∀ (i : Fin n) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)) ∧
            ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)
⊢ ∃ (f : Fin n → C(X, ℝ)),
    (∀ (i : Fin n), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ s i) ∧
      EqOn (β := ℝ) (∑ i : Fin n, (⇑(f i) : (a : X) → ℝ)) 1 t ∧
        (∀ (i : Fin n) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)) ∧
          ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)

Tactic:
obtain ⟨f, hfsub, hfcp⟩ := PartitionOfUnity.exists_isSubordinate_of_locallyFinite_t2space htcp s
    hs (locallyFinite_of_finite _) hst

Premises used: locallyFinite_of_finite, PartitionOfUnity.exists_isSubordinate_of_locallyFinite_t2space
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ (i : Fin n), s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate (s := t) s
hfcp : ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
h :
  (∀ (i : Fin n), tsupport (α := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ⊆ s i) ∧
    EqOn (β := ℝ) (∑ i : Fin n, (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) 1 t ∧
      (∀ (i : Fin n) (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
            ((((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
⊢ ∃ (f : Fin n → C(X, ℝ)),
    (∀ (i : Fin n), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ s i) ∧
      EqOn (β := ℝ) (∑ i : Fin n, (⇑(f i) : (a : X) → ℝ)) 1 t ∧
        (∀ (i : Fin n) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)) ∧
          ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)

Tactic:
use f
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ (i : Fin n), s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate (s := t) s
hfcp : ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
⊢ (∀ (i : Fin n), tsupport (α := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ⊆ s i) ∧
    EqOn (β := ℝ) (∑ i : Fin n, (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) 1 t ∧
      (∀ (i : Fin n) (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
            ((((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
⟨fun i ↦ hfsub i, ?_, ?_, fun i => hfcp i⟩

Premises used: And.intro
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ (i : Fin n), s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate (s := t) s
hfcp : ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
h : EqOn (β := ℝ) (∑ i : Fin n, (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) 1 t
h₁ :
  ∀ (i : Fin n) (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
⊢ (∀ (i : Fin n), tsupport (α := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ⊆ s i) ∧
    EqOn (β := ℝ) (∑ i : Fin n, (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) 1 t ∧
      (∀ (i : Fin n) (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
            ((((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
refine ⟨fun i ↦ hfsub i, ?_, ?_, fun i => hfcp i⟩
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ (i : Fin n), s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate (s := t) s
hfcp : ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
x : X
hx : x ∈ t
h : Eq (α := ℝ) (∑ c : Fin n, (((f : (a : Fin n) → C(X, ℝ)) c : C(X, ℝ)) : (a : X) → ℝ) x) 1
⊢ Eq (α := ℝ) ((∑ i : Fin n, (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x) (1 x)

Tactic:
simp only [Finset.sum_apply, Pi.one_apply]

Premises used: Pi.one_apply, Finset.sum_apply
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ (i : Fin n), s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate (s := t) s
hfcp : ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
x : X
hx : x ∈ t
⊢ Eq (α := ℝ) (∑ᶠ (i : Fin n), (f.toFun (s := t) i : (a : X) → ℝ) x) 1

Tactic:
have h := f.sum_eq_one' x hx
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ (i : Fin n), s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate (s := t) s
hfcp : ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
x : X
hx : x ∈ t
h : Eq (α := ℝ) (∑ᶠ (i : Fin n), (f.toFun (s := t) i : (a : X) → ℝ) x) 1
⊢ Eq (α := ℝ)
    (∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : Fin n) ↦ (f.toFun (s := t) i : (a : X) → ℝ) x) ⋯,
      (f.toFun (s := t) i : (a : X) → ℝ) x)
    1

Tactic:
rw [finsum_eq_sum (fun i => (f.toFun i) x)
      (Finite.subset finite_univ (subset_univ (support fun i ↦ (f.toFun i) x)))] at h

Premises used: finsum_eq_sum, Set.subset_univ, Set.Finite.subset, Set.finite_univ, Function.support, PartitionOfUnity.toFun, DFunLike.coe
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ (i : Fin n), s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate (s := t) s
hfcp : ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
x : X
hx : x ∈ t
h :
  Eq (α := ℝ)
    (∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : Fin n) ↦ (f.toFun (s := t) i : (a : X) → ℝ) x) ⋯,
      (f.toFun (s := t) i : (a : X) → ℝ) x)
    1
⊢ ∀ (i : Fin n),
    Ne (α := ℝ) ((f.toFun (s := t) i : (a : X) → ℝ) x : ℝ) (0 : ℝ) →
      Membership.mem (γ := Finset (Fin n))
        (Finite.toFinset (s := support (M := ℝ) fun (i : Fin n) ↦ (f.toFun (s := t) i : (a : X) → ℝ) x) ⋯) i

Tactic:
simp
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ (i : Fin n), s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate (s := t) s
hfcp : ∀ (i : Fin n), HasCompactSupport (α := X) (β := ℝ) (⇑((f : (a : Fin n) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
x : X
hx : x ∈ t
h :
  Eq (α := ℝ)
    (∑ i ∈ Finite.toFinset (s := support (M := ℝ) fun (i : Fin n) ↦ (f.toFun (s := t) i : (a : X) → ℝ) x) ⋯,
      (f.toFun (s := t) i : (a : X) → ℝ) x)
    1
h₁ h₂ h₃ h₄ :
  ∀ (h : Eq (α := ℝ) (∑ i : Fin n, (f.toFun (s := t) i : (a : X) → ℝ) x) 1),
    Eq (α := ℝ) (∑ c : Fin n, (((f : (a : Fin n) → C(X, ℝ)) c : C(X, ℝ)) : (a : X) → ℝ) x) 1
⊢ Eq (α := ℝ) (∑ c : Fin n, (((f : (a : Fin n) → C(X, ℝ)) c : C(X, ℝ)) : (a : X) → ℝ) x) 1

Tactic:
rwa [Fintype.sum_subset (by simp)] at h

Premises used: Fintype.sum_subset