awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rcases :
  ∀ (V : ι → Set X) (hVo : ∀ (i : ι), IsOpen[inst] (V i)) (hsV : s ⊆ ⋃ (i : ι), V i) (hVf : LocallyFinite V)
    (hVU : ∀ (i : ι), V i ⊆ U i), ∃ (f : BumpCovering ι X s), f.IsSubordinate (s := s) U
⊢ ∃ (f : BumpCovering ι X s), f.IsSubordinate (s := s) U

Tactic:
rcases precise_refinement_set hs _ ho hU with ⟨V, hVo, hsV, hVf, hVU⟩

Premises used: precise_refinement_set
-- 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
V : ι → Set X
hVo : ∀ (i : ι), IsOpen[inst] (V i)
hsV : s ⊆ ⋃ (i : ι), V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
rcases :
  ∀ (f : BumpCovering ι X s) (hf : f.IsSubordinate (s := s) V), ∃ (f : BumpCovering ι X s), f.IsSubordinate (s := s) U
⊢ ∃ (f : BumpCovering ι X s), f.IsSubordinate (s := s) U

Tactic:
rcases exists_isSubordinate_of_locallyFinite hs V hVo hVf hsV with ⟨f, hf⟩

Premises used: BumpCovering.exists_isSubordinate_of_locallyFinite
-- 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
V : ι → Set X
hVo : ∀ (i : ι), IsOpen[inst] (V i)
hsV : s ⊆ ⋃ (i : ι), V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
f : BumpCovering ι X s
hf : f.IsSubordinate (s := s) V
⊢ ∃ (f : BumpCovering ι X s), f.IsSubordinate (s := s) U

Tactic:
⟨f, hf.mono hVU⟩

Premises used: BumpCovering.IsSubordinate.mono, Exists.intro
-- 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
V : ι → Set X
hVo : ∀ (i : ι), IsOpen[inst] (V i)
hsV : s ⊆ ⋃ (i : ι), V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
f : BumpCovering ι X s
hf : f.IsSubordinate (s := s) V
⊢ ∃ (f : BumpCovering ι X s), f.IsSubordinate (s := s) U

Tactic:
exact ⟨f, hf.mono hVU⟩
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : LocallyCompactSpace X
inst_2 : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsCompact t →
        Disjoint s t →
          ∃ (f : C(X, ℝ)),
            p (⇑f : (a : X) → ℝ) ∧
              EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
                EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
                  ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
rcases :
  ∀ (V : ι → Set X) (hsV : s ⊆ iUnion V) (hVo : ∀ (i : ι), IsOpen[inst] (V i))
    (hVU : ∀ (i : ι), closure[inst] (V i) ⊆ U i) (hcp : ∀ (i : ι), IsCompact (closure[inst] (V i))),
    ∃ (f : BumpCovering ι X s),
      (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧
        f.IsSubordinate (s := s) U ∧
          ∀ (i : ι), HasCompactSupport.{v, 0} (α := X) (β := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧
      f.IsSubordinate (s := s) U ∧
        ∀ (i : ι), HasCompactSupport.{v, 0} (α := X) (β := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
rcases exists_subset_iUnion_closure_subset_t2space hs ho (fun x _ => hf.point_finite x) hU with
    ⟨V, hsV, hVo, hVU, hcp⟩

Premises used: exists_subset_iUnion_closure_subset_t2space, LocallyFinite.point_finite
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : LocallyCompactSpace X
inst_2 : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsCompact t →
        Disjoint s t →
          ∃ (f : C(X, ℝ)),
            p (⇑f : (a : X) → ℝ) ∧
              EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
                EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
                  ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst] (V i)
hVU : ∀ (i : ι), closure[inst] (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure[inst] (V i))
⊢ ∀ (i : ι), V i ⊆ U i

Tactic:
have hVU' i : V i ⊆ U i := subset_closure.trans (hVU i)
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : LocallyCompactSpace X
inst_2 : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsCompact t →
        Disjoint s t →
          ∃ (f : C(X, ℝ)),
            p (⇑f : (a : X) → ℝ) ∧
              EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
                EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
                  ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst] (V i)
hVU : ∀ (i : ι), closure[inst] (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure[inst] (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
rcases :
  ∀ (W : ι → Set X) (hsW : s ⊆ iUnion W) (hWo : ∀ (i : ι), IsOpen[inst] (W i))
    (hWV : ∀ (i : ι), closure[inst] (W i) ⊆ V i) (hWc : ∀ (i : ι), IsCompact (closure[inst] (W i))),
    ∃ (f : BumpCovering ι X s),
      (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧
        f.IsSubordinate (s := s) U ∧
          ∀ (i : ι), HasCompactSupport.{v, 0} (α := X) (β := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧
      f.IsSubordinate (s := s) U ∧
        ∀ (i : ι), HasCompactSupport.{v, 0} (α := X) (β := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
rcases exists_subset_iUnion_closure_subset_t2space hs hVo
    (fun x _ => (hf.subset hVU').point_finite x) hsV with ⟨W, hsW, hWo, hWV, hWc⟩

Premises used: exists_subset_iUnion_closure_subset_t2space, LocallyFinite.subset, LocallyFinite.point_finite
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : LocallyCompactSpace X
inst_2 : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsCompact t →
        Disjoint s t →
          ∃ (f : C(X, ℝ)),
            p (⇑f : (a : X) → ℝ) ∧
              EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
                EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
                  ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst] (V i)
hVU : ∀ (i : ι), closure[inst] (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure[inst] (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen[inst] (W i)
hWV : ∀ (i : ι), closure[inst] (W i) ⊆ V i
hWc : ∀ (i : ι), IsCompact (closure[inst] (W i))
choose :
  ∀ (f : (i : ι) → C(X, ℝ)) (hfp : ∀ (i : ι), p (⇑(f i) : (a : X) → ℝ))
    (hf0 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 0 (V i)ᶜ)
    (hf1 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1 (closure[inst] (W i)))
    (hf01 : ∀ (i : ι) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)),
    ∃ (f : BumpCovering ι X s),
      (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧
        f.IsSubordinate (s := s) U ∧
          ∀ (i : ι), HasCompactSupport.{v, 0} (α := X) (β := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧
      f.IsSubordinate (s := s) U ∧
        ∀ (i : ι), HasCompactSupport.{v, 0} (α := X) (β := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
choose f hfp hf0 hf1 hf01 using fun i =>
    h01 _ _ (isClosed_compl_iff.2 <| hVo i) (hWc i)
      (disjoint_right.2 fun x hx => Classical.not_not.2 (hWV i hx))

Premises used: Iff.mpr, Classical.not_not, Compl.compl, Set.disjoint_right, closure, isClosed_compl_iff
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : LocallyCompactSpace X
inst_2 : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsCompact t →
        Disjoint s t →
          ∃ (f : C(X, ℝ)),
            p (⇑f : (a : X) → ℝ) ∧
              EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
                EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
                  ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst] (V i)
hVU : ∀ (i : ι), closure[inst] (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure[inst] (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen[inst] (W i)
hWV : ∀ (i : ι), closure[inst] (W i) ⊆ V i
hWc : ∀ (i : ι), IsCompact (closure[inst] (W i))
f : (i : ι) → C(X, ℝ)
hfp : ∀ (i : ι), p (⇑(f i) : (a : X) → ℝ)
hf0 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1 (closure[inst] (W i))
hf01 : ∀ (i : ι) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)
⊢ ∀ (i : ι), support (M := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ V i

Tactic:
have hsupp i : support (f i) ⊆ V i := support_subset_iff'.2 (hf0 i)
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : LocallyCompactSpace X
inst_2 : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsCompact t →
        Disjoint s t →
          ∃ (f : C(X, ℝ)),
            p (⇑f : (a : X) → ℝ) ∧
              EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
                EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
                  ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst] (V i)
hVU : ∀ (i : ι), closure[inst] (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure[inst] (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen[inst] (W i)
hWV : ∀ (i : ι), closure[inst] (W i) ⊆ V i
hWc : ∀ (i : ι), IsCompact (closure[inst] (W i))
f : (i : ι) → C(X, ℝ)
hfp : ∀ (i : ι), p (⇑(f i) : (a : X) → ℝ)
hf0 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1 (closure[inst] (W i))
hf01 : ∀ (i : ι) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)
hsupp : ∀ (i : ι), support (M := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ V i
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧
      f.IsSubordinate (s := s) U ∧
        ∀ (i : ι), HasCompactSupport.{v, 0} (α := X) (β := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
⟨⟨f, hf.subset fun i => Subset.trans (hsupp i) (hVU' i), fun i x => (hf01 i x).1,
      fun i x => (hf01 i x).2, fun x hx => ?_⟩,
    hfp, fun i => Subset.trans (closure_mono (hsupp i)) (hVU i),
    fun i => IsCompact.of_isClosed_subset (hcp i) isClosed_closure <| closure_mono (hsupp i)⟩

Premises used: Set.Subset.trans, LocallyFinite.subset, closure_mono, BumpCovering.mk, IsCompact.of_isClosed_subset, And.right, And.left, And.intro, Exists.intro, isClosed_closure
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : LocallyCompactSpace X
inst_2 : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsCompact t →
        Disjoint s t →
          ∃ (f : C(X, ℝ)),
            p (⇑f : (a : X) → ℝ) ∧
              EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
                EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
                  ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst] (V i)
hVU : ∀ (i : ι), closure[inst] (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure[inst] (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen[inst] (W i)
hWV : ∀ (i : ι), closure[inst] (W i) ⊆ V i
hWc : ∀ (i : ι), IsCompact (closure[inst] (W i))
f : (i : ι) → C(X, ℝ)
hfp : ∀ (i : ι), p (⇑(f i) : (a : X) → ℝ)
hf0 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1 (closure[inst] (W i))
hf01 : ∀ (i : ι) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)
hsupp : ∀ (i : ι), support (M := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ V i
refine : ∀ (x : X) (hx : x ∈ s), ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧
      f.IsSubordinate (s := s) U ∧
        ∀ (i : ι), HasCompactSupport.{v, 0} (α := X) (β := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
refine ⟨⟨f, hf.subset fun i => Subset.trans (hsupp i) (hVU' i), fun i x => (hf01 i x).1,
      fun i x => (hf01 i x).2, fun x hx => ?_⟩,
    hfp, fun i => Subset.trans (closure_mono (hsupp i)) (hVU i),
    fun i => IsCompact.of_isClosed_subset (hcp i) isClosed_closure <| closure_mono (hsupp i)⟩
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : LocallyCompactSpace X
inst_2 : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsCompact t →
        Disjoint s t →
          ∃ (f : C(X, ℝ)),
            p (⇑f : (a : X) → ℝ) ∧
              EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
                EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
                  ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst] (V i)
hVU : ∀ (i : ι), closure[inst] (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure[inst] (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen[inst] (W i)
hWV : ∀ (i : ι), closure[inst] (W i) ⊆ V i
hWc : ∀ (i : ι), IsCompact (closure[inst] (W i))
f : (i : ι) → C(X, ℝ)
hfp : ∀ (i : ι), p (⇑(f i) : (a : X) → ℝ)
hf0 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1 (closure[inst] (W i))
hf01 : ∀ (i : ι) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)
hsupp : ∀ (i : ι), support (M := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ V i
x : X
hx : x ∈ s
rcases : ∀ (i : ι) (hi : x ∈ W i), ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1
⊢ ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1

Tactic:
rcases mem_iUnion.1 (hsW hx) with ⟨i, hi⟩

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : LocallyCompactSpace X
inst_2 : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsCompact t →
        Disjoint s t →
          ∃ (f : C(X, ℝ)),
            p (⇑f : (a : X) → ℝ) ∧
              EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
                EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
                  ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst] (V i)
hVU : ∀ (i : ι), closure[inst] (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure[inst] (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen[inst] (W i)
hWV : ∀ (i : ι), closure[inst] (W i) ⊆ V i
hWc : ∀ (i : ι), IsCompact (closure[inst] (W i))
f : (i : ι) → C(X, ℝ)
hfp : ∀ (i : ι), p (⇑(f i) : (a : X) → ℝ)
hf0 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1 (closure[inst] (W i))
hf01 : ∀ (i : ι) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)
hsupp : ∀ (i : ι), support (M := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ V i
x : X
hx : x ∈ s
i : ι
hi : x ∈ W i
⊢ ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1

Tactic:
⟨i, ((hf1 i).mono subset_closure).eventuallyEq_of_mem ((hWo i).mem_nhds hi)⟩

Premises used: subset_closure, Set.EqOn.eventuallyEq_of_mem, IsOpen.mem_nhds, Exists.intro, Set.EqOn.mono
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : LocallyCompactSpace X
inst_2 : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsCompact t →
        Disjoint s t →
          ∃ (f : C(X, ℝ)),
            p (⇑f : (a : X) → ℝ) ∧
              EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
                EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
                  ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen[inst] (V i)
hVU : ∀ (i : ι), closure[inst] (V i) ⊆ U i
hcp : ∀ (i : ι), IsCompact (closure[inst] (V i))
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen[inst] (W i)
hWV : ∀ (i : ι), closure[inst] (W i) ⊆ V i
hWc : ∀ (i : ι), IsCompact (closure[inst] (W i))
f : (i : ι) → C(X, ℝ)
hfp : ∀ (i : ι), p (⇑(f i) : (a : X) → ℝ)
hf0 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1 (closure[inst] (W i))
hf01 : ∀ (i : ι) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)
hsupp : ∀ (i : ι), support (M := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ V i
x : X
hx : x ∈ s
i : ι
hi : x ∈ W i
⊢ ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1

Tactic:
exact ⟨i, ((hf1 i).mono subset_closure).eventuallyEq_of_mem ((hWo i).mem_nhds hi)⟩
-- 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 : BumpCovering ι X s),
    f.IsSubordinate (s := s) U ∧
      ∀ (i : ι), HasCompactSupport.{v, 0} (α := X) (β := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
simpa using
    exists_isSubordinate_of_locallyFinite_of_prop_t2space (fun _ => True)
      (fun _ _ ht hs hd =>
        (exists_continuous_zero_one_of_isCompact' hs ht hd.symm).imp fun _ hf => ⟨trivial, hf⟩)
      hs U ho hf hU

Premises used: trivial, exists_continuous_zero_one_of_isCompact', Exists.imp, BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop_t2space, Disjoint.symm, And.intro, True
-- 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
⊢ (𝓝 x).EventuallyEq (β := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) (f.ind (s := s) x hx) : C(X, ℝ)) : (a : X) → ℝ) 1

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

Premises used: Exists.choose_spec, BumpCovering.ind, BumpCovering.eventuallyEq_one'
-- 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
⊢ Eq (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) (f.ind (s := s) x hx) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
(f.eventuallyEq_one x hx).eq_of_nhds

Premises used: BumpCovering.eventuallyEq_one, Filter.EventuallyEq.eq_of_nhds
-- 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 : ℝ)
rw :
  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 : ℝ) :
        ℝ) =
    0
rw₁ :
  HMul.hMul (α := ℝ) 0
      (∏ᶠ (j : ι) (_ : WellOrderingRel j i),
        HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) =
    0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ f.toPOUFun (s := s) i x = 0

Tactic:
rw [toPOUFun, h, zero_mul]

Premises used: MulZeroClass.zero_mul, BumpCovering.toPOUFun
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ support (f.toPOUFun (s := s) i) ⊆ support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
fun _ => mt <| f.toPOUFun_zero_of_zero

Premises used: Set.Mem, setOf, mt, Set.Subset, Function.support, BumpCovering.toPOUFun_zero_of_zero, Not
-- 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.toPOUFun (s := s) i 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:
congr_arg _ (finprod_cond_eq_prod_of_cond_iff _ fun {j} hj => ?_)

Premises used: congr_arg, BumpCovering.toPOUFun, finprod_cond_eq_prod_of_cond_iff
-- 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
refine :
  ∀ {j : ι}
    (hj : HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ≠ 1),
    WellOrderingRel j i ↔ j ∈ {j ∈ t | WellOrderingRel j i}
⊢ f.toPOUFun (s := s) i 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:
refine congr_arg _ (finprod_cond_eq_prod_of_cond_iff _ fun {j} hj => ?_)

Premises used: congr_arg, finprod_cond_eq_prod_of_cond_iff
-- 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
j : ι
hj : HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ≠ 1
⊢ ¬Eq (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rw [Ne, sub_eq_self] at hj

Premises used: Ne, sub_eq_self