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
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ∀ᶠ (y : X) in 𝓝 x₀, ρ.fintsupport (s := s) y ⊆ ρ.fintsupport (s := s) x₀
have apply : ∀ (x : X),
  Subset.{u} (α := Set ι)
      {i : ι |
        Membership.mem (γ := Set X)
          (closure[inst] (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))) x}
      {i : ι |
        Membership.mem (γ := Set X)
          (closure[inst] (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))) x₀} →
    ρ.fintsupport (s := s) x ⊆ ρ.fintsupport (s := s) x₀
Tactic: apply (ρ.locallyFinite.closure.eventually_subset (fun _ ↦ isClosed_closure) x₀).mono
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ y : X
hy :
  Subset.{u} (α := Set ι)
    {i : ι |
      Membership.mem (γ := Set X)
        (closure[inst] (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))) y}
    {i : ι |
      Membership.mem (γ := Set X)
        (closure[inst] (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ))) x₀}
z : ι
hz : z ∈ ρ.fintsupport (s := s) y
⊢ z ∈ ρ.fintsupport (s := s) x₀
have rw : ∀ (hz : Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) z : C(X, ℝ)) : (a : X) → ℝ)) y),
  Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) z : C(X, ℝ)) : (a : X) → ℝ)) x₀
Tactic: rw [PartitionOfUnity.mem_fintsupport_iff] at *
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport (s := s) x₀
⊢ i ∈ ρ.fintsupport (s := s) x₀
have rw : Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀
Tactic: rw [ρ.mem_fintsupport_iff]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport (s := s) x₀
⊢ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀
have a : Membership.mem (γ := Set X) (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀
Tactic: apply subset_closure
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ∃ (I : Finset ι),
    (∀ᶠ (x : X) in 𝓝[s] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
      ∀ᶠ (x : X) in 𝓝 x₀,
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
have rcases : ∀ (I : Finset ι)
  (hI :
    ∀ᶠ (x : X) in 𝓝 x₀,
      (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)),
  ∃ (I : Finset ι),
    (∀ᶠ (x : X) in 𝓝[s] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
      ∀ᶠ (x : X) in 𝓝 x₀,
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
Tactic: rcases ρ.locallyFinite.exists_finset_support x₀ with ⟨I, hI⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI :
  ∀ᶠ (x : X) in 𝓝 x₀,
    (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
⊢ ∃ (I : Finset ι),
    (∀ᶠ (x : X) in 𝓝[s] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
      ∀ᶠ (x : X) in 𝓝 x₀,
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
have refine : ∀ (x : X) (hx : (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι))
  (x_in : x ∈ s), Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
Tactic: refine ⟨I, eventually_nhdsWithin_iff.mpr (hI.mono fun x hx x_in ↦ ?_), hI⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (hypothesis)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI :
  ∀ᶠ (x : X) in 𝓝 x₀,
    (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
x : X
hx : (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
x_in : x ∈ s
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
have this : Eq (α := ℝ) (∑ᶠ (i : ι), (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
  (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
Tactic: have : ∑ᶠ i : ι, ρ i x = ∑ i ∈ I, ρ i x := finsum_eq_sum_of_support_subset _ hx
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI :
  ∀ᶠ (x : X) in 𝓝 x₀,
    (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
x : X
hx : (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
x_in : x ∈ s
this :
  Eq (α := ℝ) (∑ᶠ (i : ι), (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
    (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
have rwa : ∀
  (this :
    Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
      (∑ᶠ (i : ι), (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)),
  Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
Tactic: rwa [eq_comm, ρ.sum_eq_one x_in] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI :
  ∀ᶠ (x : X) in 𝓝 x₀,
    (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
x : X
hx : (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
x_in : x ∈ s
this :
  Eq (α := ℝ) (∑ᶠ (i : ι), (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
    (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
rwa :
  ∀
    (this :
      Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
        (∑ᶠ (i : ι), (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)),
    Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
have rwa₁ : ∀ (this : Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1),
  Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
Tactic: rwa [eq_comm, ρ.sum_eq_one x_in] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
⊢ ∃ (I : Finset ι),
    ∀ᶠ (x : X) in 𝓝 x₀,
      Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
have rcases : ∀ (I : Finset ι)
  (H :
    (∀ᶠ (x : X) in 𝓝[univ] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
      ∀ᶠ (x : X) in 𝓝 x₀,
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)),
  ∃ (I : Finset ι),
    ∀ᶠ (x : X) in 𝓝 x₀,
      Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
Tactic: rcases ρ.exists_finset_nhds' x₀ with ⟨I, H⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
I : Finset ι
H :
  (∀ᶠ (x : X) in 𝓝[univ] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
    ∀ᶠ (x : X) in 𝓝 x₀,
      (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
⊢ ∃ (I : Finset ι),
    ∀ᶠ (x : X) in 𝓝 x₀,
      Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
have h : ∀ᶠ (x : X) in 𝓝 x₀,
  Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
    (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
Tactic: use I
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
I : Finset ι
H :
  (∀ᶠ (x : X) in 𝓝[univ] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
    ∀ᶠ (x : X) in 𝓝 x₀,
      (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
⊢ ∀ᶠ (x : X) in 𝓝 x₀,
    Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
      (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
have h : ∀
  (H :
    (∀ᶠ (x : X) in 𝓝 x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
      ∀ᶠ (x : X) in 𝓝 x₀,
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)),
  ∀ᶠ (x : X) in 𝓝 x₀,
    Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
      (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
Tactic: rwa [nhdsWithin_univ, ← eventually_and] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
I : Finset ι
H :
  (∀ᶠ (x : X) in 𝓝[univ] x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
    ∀ᶠ (x : X) in 𝓝 x₀,
      (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
h :
  ∀
    (H :
      (∀ᶠ (x : X) in 𝓝 x₀, Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1) ∧
        ∀ᶠ (x : X) in 𝓝 x₀,
          (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)),
    ∀ᶠ (x : X) in 𝓝 x₀,
      Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
⊢ ∀ᶠ (x : X) in 𝓝 x₀,
    Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
      (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
have h₁ : ∀
  (H :
    ∀ᶠ (x : X) in 𝓝 x₀,
      Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
        (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)),
  ∀ᶠ (x : X) in 𝓝 x₀,
    Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1 ∧
      (support (M := ℝ) fun (x_1 : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) x_1 : C(X, ℝ)) : (a : X) → ℝ) x) ⊆ (↑I : Set ι)
Tactic: rwa [nhdsWithin_univ, ← eventually_and] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f_1 f g : BumpCovering ι X s
h : f.toFun (s := s) = g.toFun (s := s)
⊢ f = g
have mk : ∀ (toFun : ι → C(X, ℝ))
  (locallyFinite' : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : X) → ℝ))
  (nonneg' : 0 ≤ toFun) (le_one' : toFun ≤ 1)
  (eventuallyEq_one' : ∀ x ∈ s, ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(toFun i) : (a : X) → ℝ) 1)
  (h : (mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one').toFun (s := s) = g.toFun (s := s)),
  mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one' = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f g : BumpCovering ι X s
toFun : ι → C(X, ℝ)
locallyFinite' : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : X) → ℝ)
nonneg' : 0 ≤ toFun
le_one' : toFun ≤ 1
eventuallyEq_one' : ∀ x ∈ s, ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(toFun i) : (a : X) → ℝ) 1
h : (mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one').toFun (s := s) = g.toFun (s := s)
⊢ mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one' = g
have mk : ∀ (toFun_1 : ι → C(X, ℝ))
  (locallyFinite'_1 : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun_1 i) : (a : X) → ℝ))
  (nonneg'_1 : 0 ≤ toFun_1) (le_one'_1 : toFun_1 ≤ 1)
  (eventuallyEq_one'_1 : ∀ x ∈ s, ∃ (i : ι), (𝓝 x).EventuallyEq (β := ℝ) (⇑(toFun_1 i) : (a : X) → ℝ) 1)
  (h :
    (mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one').toFun (s := s) =
      (mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 le_one'_1 eventuallyEq_one'_1).toFun (s := s)),
  mk (s := s) toFun locallyFinite' nonneg' le_one' eventuallyEq_one' =
    mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 le_one'_1 eventuallyEq_one'_1
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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}
have 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}
Tactic: refine ⟨univ, univ_mem, (finite_singleton i).subset ?_⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ Membership.mem (γ := Set ι) {i} j
have contrapose! : ∀ (hx : j ∉ {i}),
  x ∉ support (M := ℝ) (⇑(Pi.single (M := fun (a : ι) ↦ C(X, ℝ)) i (1 : C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ)
Tactic: contrapose! hx
Cleared hypotheses: hx
-- 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
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) → ℝ)
have hx₁ : ¬j = i
Tactic: rw [mem_singleton_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ (𝓝 x).EventuallyEq (β := ℝ) (⇑(Pi.single (M := fun (a : ι) ↦ C(X, ℝ)) i (1 : C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) 1
have rw : (𝓝 x).EventuallyEq (β := ℝ) (⇑1 : (a : X) → ℝ) 1
Tactic: rw [Pi.single_eq_same, ContinuousMap.coe_one]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ (𝓝 x).EventuallyEq (β := ℝ) (⇑(Pi.single (M := fun (a : ι) ↦ C(X, ℝ)) i (1 : C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) 1
have rw₁ : (𝓝 x).EventuallyEq (β := ℝ) 1 1
Tactic: rw [Pi.single_eq_same, ContinuousMap.coe_one]
-- 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
⊢ ∃ (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) (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
Tactic: rcases exists_subset_iUnion_closure_subset hs ho (fun x _ => hf.point_finite x) hU with
    ⟨V, hsV, hVo, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (hypothesis)
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
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U
have hVU' : ∀ (i : ι), V i ⊆ U i
Tactic: have hVU' : ∀ i, V i ⊆ U i := fun i => Subset.trans subset_closure (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
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U
have 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
Tactic: rcases exists_subset_iUnion_closure_subset hs hVo (fun x _ => (hf.subset hVU').point_finite x)
      hsV with
    ⟨W, hsW, hWo, hWV⟩
-- 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 : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U
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
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))
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (hypothesis)
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 : ℝ)
⊢ ∃ (f : BumpCovering ι X s),
    (∀ (i : ι), p (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) ∧ f.IsSubordinate (s := s) U
have hsupp : ∀ (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)