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
⊢ LE.le (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
f.le_one' i x

Premises used: BumpCovering.le_one'
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s_1 : Set X
f : BumpCovering ι X s_1
i : ι
s : Set X
x : X
⊢ ∃ t ∈ 𝓝 x,
    Set.Finite.{u} (α := ι)
      {i_1 : ι |
        ((fun (i_2 : ι) ↦
                (support (M := ℝ)
                    (⇑(Pi.single (M := fun (a : ι) ↦ C(X, ℝ)) i (1 : C(X, ℝ)) i_2 : C(X, ℝ)) : (a : X) → ℝ) :
                  Set X))
              i_1 ∩
            t).Nonempty}

Tactic:
⟨univ, univ_mem, (finite_singleton i).subset ?_⟩

Premises used: Set.univ, Set.Finite.subset, And.intro, Exists.intro, Filter.univ_mem, Set.finite_singleton
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s_1 : Set X
f : BumpCovering ι X s_1
i : ι
s : Set X
x : X
refine :
  Subset (α := Set ι)
    {i_1 : ι |
      Set.Nonempty.{v} (α := X)
        ((fun (i_2 : ι) ↦
              (support (M := ℝ)
                  (⇑(Pi.single (M := fun (a : ι) ↦ C(X, ℝ)) i (1 : C(X, ℝ)) i_2 : C(X, ℝ)) : (a : X) → ℝ) :
                Set X))
            i_1 ∩
          univ)}
    {i}
⊢ ∃ t ∈ 𝓝 x,
    Set.Finite.{u} (α := ι)
      {i_1 : ι |
        ((fun (i_2 : ι) ↦
                (support (M := ℝ)
                    (⇑(Pi.single (M := fun (a : ι) ↦ C(X, ℝ)) i (1 : C(X, ℝ)) i_2 : C(X, ℝ)) : (a : X) → ℝ) :
                  Set X))
              i_1 ∩
            t).Nonempty}

Tactic:
refine ⟨univ, univ_mem, (finite_singleton i).subset ?_⟩
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s_1 : Set X
f : BumpCovering ι X s_1
i : ι
s : Set X
x_1 : X
j : ι
x : X
hx :
  Membership.mem (γ := Set X)
    ((fun (i_1 : ι) ↦
        (support (M := ℝ) (⇑(Pi.single (M := fun (a : ι) ↦ C(X, ℝ)) i (1 : C(X, ℝ)) i_1 : C(X, ℝ)) : (a : X) → ℝ) :
          Set X))
      j)
    x
contrapose! :
  ∀ (hx : j ∉ {i}),
    x ∉ support (M := ℝ) (⇑(Pi.single (M := fun (a : ι) ↦ C(X, ℝ)) i (1 : C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ)
⊢ Membership.mem (γ := Set ι) {i} j

Tactic:
contrapose! hx
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s_1 : Set X
f : BumpCovering ι X s_1
i : ι
s : Set X
x_1 : X
j : ι
x : X
hx : j ∉ {i}
⊢ ¬j = i

Tactic:
rw [mem_singleton_iff] at hx

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s_1 : Set X
f : BumpCovering ι X s_1
i : ι
s : Set X
x_1 : X
j : ι
x : X
hx : ¬j = i
⊢ x ∉ support (M := ℝ) (⇑(Pi.single (M := fun (a : ι) ↦ C(X, ℝ)) i (1 : C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
simp [hx]
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s_1 : Set X
f : BumpCovering ι X s_1
i : ι
s : Set X
x : X
h : x ∈ s
rw : (𝓝 x).EventuallyEq (β := ℝ) (⇑1 : (a : X) → ℝ) 1
rw₁ rw₂ : (𝓝 x).EventuallyEq (β := ℝ) 1 1
⊢ (𝓝 x).EventuallyEq (β := ℝ) (⇑(Pi.single (M := fun (a : ι) ↦ C(X, ℝ)) i (1 : C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) 1

Tactic:
rw [Pi.single_eq_same, ContinuousMap.coe_one]

Premises used: ContinuousMap.coe_one, Pi.single_eq_same
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
i : ι
s : Set X
⊢ Eq (α := (a : ι) → C(X, ℝ)) (⇑(BumpCovering.single i s) : (a : ι) → C(X, ℝ))
    (Pi.single (M := fun (j : ι) ↦ C(X, ℝ)) i 1)

Tactic:
rfl
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
U V : ι → Set X
hU : f.IsSubordinate (s := s) U
hV : ∀ (i : ι), U i ⊆ V i
⊢ f.IsSubordinate (s := s) V

Tactic:
fun i => Subset.trans (hU i) (hV i)

Premises used: Set.Subset.trans, BumpCovering.IsSubordinate
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : IsClosed[inst] 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),
    ∃ (f : BumpCovering ι X s),
      (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U

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

Premises used: exists_subset_iUnion_closure_subset, LocallyFinite.point_finite
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : IsClosed[inst] 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
⊢ ∀ (i : ι), V i ⊆ U i

Tactic:
have hVU' : ∀ i, V i ⊆ U i := fun i => Subset.trans subset_closure (hVU i)
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : IsClosed[inst] 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
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),
    ∃ (f : BumpCovering ι X s),
      (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U

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

Premises used: exists_subset_iUnion_closure_subset, LocallyFinite.subset, LocallyFinite.point_finite
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : IsClosed[inst] 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
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
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
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U

Tactic:
choose f hfp hf0 hf1 hf01 using fun i =>
    h01 _ _ (isClosed_compl_iff.2 <| hVo i) isClosed_closure
      (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_closure, isClosed_compl_iff
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : IsClosed[inst] 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
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
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 := fun 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 : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : IsClosed[inst] 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
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
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

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)⟩

Premises used: Set.Subset.trans, LocallyFinite.subset, closure_mono, BumpCovering.mk, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : IsClosed[inst] 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
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
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

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)⟩
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : IsClosed[inst] 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
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
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 : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : IsClosed[inst] 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
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
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 : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : IsClosed[inst] 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
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
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 : NormalSpace X
hs : IsClosed[inst] 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

Tactic:
let ⟨f, _, hfU⟩ :=
    exists_isSubordinate_of_locallyFinite_of_prop (fun _ => True)
      (fun _ _ hs ht hd =>
        (exists_continuous_zero_one_of_isClosed hs ht hd).imp fun _ hf => ⟨trivial, hf⟩)
      hs U ho hf hU
  ⟨f, hfU⟩

Premises used: trivial, exists_continuous_zero_one_of_isClosed, BumpCovering.IsSubordinate, Exists, Exists.imp, And.intro, True, Exists.intro, BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop, _private.0.BumpCovering.exists_isSubordinate_of_locallyFinite.match_1
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : NormalSpace X
inst_2 : ParacompactSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : 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),
      (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ 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
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : 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) (hfp : ∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))
    (hf : f.IsSubordinate (s := s) V),
    ∃ (f : BumpCovering ι X s),
      (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U

Tactic:
rcases exists_isSubordinate_of_locallyFinite_of_prop p h01 hs V hVo hVf hsV with ⟨f, hfp, hf⟩

Premises used: BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
inst_1 : NormalSpace X
inst_2 : ParacompactSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : 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
hfp : ∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
hf : f.IsSubordinate (s := s) V
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U

Tactic:
⟨f, hfp, hf.mono hVU⟩

Premises used: BumpCovering.IsSubordinate.mono, And.intro, 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
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst] s →
      IsClosed[inst] 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 : 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
hfp : ∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
hf : f.IsSubordinate (s := s) V
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U

Tactic:
exact ⟨f, hfp, hf.mono hVU⟩