awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
have refine : ∀ (x : X) (hx : x ∈ s), ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1
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)⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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 : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1
have rcases : ∀ (i : ι) (hi : x ∈ W i), ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1
Tactic: rcases mem_iUnion.1 (hsW hx) with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U
have 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
Tactic: rcases precise_refinement_set hs _ ho hU with ⟨V, hVo, hsV, hVf, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U
have 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
Tactic: rcases exists_isSubordinate_of_locallyFinite_of_prop p h01 hs V hVo hVf hsV with ⟨f, hfp, hf⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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 : BumpCovering ι X s), f.IsSubordinate (s := s) U
have 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
Tactic: rcases precise_refinement_set hs _ ho hU with ⟨V, hVo, hsV, hVf, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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), f.IsSubordinate (s := s) U
have rcases : ∀ (f : BumpCovering ι X s) (hf : f.IsSubordinate (s := s) V), ∃ (f : BumpCovering ι X s), f.IsSubordinate (s := s) U
Tactic: rcases exists_isSubordinate_of_locallyFinite hs V hVo hVf hsV with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ ∃ (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) → ℝ)
have 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) → ℝ)
Tactic: rcases exists_subset_iUnion_closure_subset_t2space hs ho (fun x _ => hf.point_finite x) hU with
    ⟨V, hsV, hVo, hVU, hcp⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (hypothesis)
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))
⊢ ∃ (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) → ℝ)
have hVU' : ∀ (i : ι), V i ⊆ U i
Tactic: have hVU' i : V i ⊆ U i := subset_closure.trans (hVU i)
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ ∃ (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) → ℝ)
have 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) → ℝ)
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⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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 : 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) → ℝ)
have 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) → ℝ)
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))
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (hypothesis)
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 : ℝ)
⊢ ∃ (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) → ℝ)
have hsupp : ∀ (i : ι), support (M := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ V i
Tactic: have hsupp i : support (f i) ⊆ V i := support_subset_iff'.2 (hf0 i)
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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) → ℝ)
have refine : ∀ (x : X) (hx : x ∈ s), ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1
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)⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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 : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1
have rcases : ∀ (i : ι) (hi : x ∈ W i), ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(f i) : (a : X) → ℝ) 1
Tactic: rcases mem_iUnion.1 (hsW hx) with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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 : ℝ)
⊢ f.toPOUFun (s := s) i x = 0
have 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
Tactic: rw [toPOUFun, h, zero_mul]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ f.toPOUFun (s := s) i x = 0
have rw₁ : HMul.hMul (α := ℝ) 0
    (∏ᶠ (j : ι) (_ : WellOrderingRel j i),
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) =
  0
Tactic: rw [toPOUFun, h, zero_mul]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ f.toPOUFun (s := s) i x = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [toPOUFun, h, zero_mul]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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 : ℝ) :
        ℝ)
have 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}
Tactic: refine congr_arg _ (finprod_cond_eq_prod_of_cond_iff _ fun {j} hj => ?_)
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (hypothesis)
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
⊢ WellOrderingRel j i ↔ j ∈ {j ∈ t | WellOrderingRel j i}
have hj₁ : ¬Eq (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rw [Ne, sub_eq_self] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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 : ¬Eq (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ WellOrderingRel j i ↔ j ∈ {j ∈ t | WellOrderingRel j i}
have rw : WellOrderingRel j i → j ∈ t
Tactic: rw [Finset.mem_filter, Iff.comm, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (hypothesis)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s_1 : Set X
f : BumpCovering ι X s_1
x : X
s : Finset ι :=
  ⋯.toFinset (s := {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)})
⊢ ∑ᶠ (i : ι), f.toPOUFun (s := s_1) i x =
    HSub.hSub (α := ℝ) 1
      (∏ᶠ (i : ι), HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ))
have hs : (↑s : Set ι) = {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
Tactic: have hs : (s : Set ι) = { i | f i x ≠ 0 } := Finite.coe_toFinset _