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_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 : ℝ)})
hs : (↑s : Set ι) = {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
⊢ (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x) ⊆ (↑s : Set ι)
have rw : Subset.{u} (α := Set ι) (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x)
  {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
Tactic: rw [hs]
-- 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 : ℝ)})
hs : (↑s : Set ι) = {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 A : (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x) ⊆ (↑s : Set ι)
Tactic: have A : (support fun i => toPOUFun f i x) ⊆ s := by
    rw [hs]
    exact fun i hi => f.support_toPOUFun_subset i hi
-- 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
x : X
s : Finset ι :=
  ⋯.toFinset (s := {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)})
hs : (↑s : Set ι) = {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
A : (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x) ⊆ (↑s : Set ι)
⊢ (mulSupport (M := ℝ) fun (i : ι) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ⊆
    (↑s : Set ι)
have rw : Subset.{u} (α := Set ι) (support (M := ℝ) fun (i : ι) ↦ (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
  {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
Tactic: rw [hs, mulSupport_one_sub]
-- 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 : ℝ)})
hs : (↑s : Set ι) = {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
A : (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x) ⊆ (↑s : Set ι)
⊢ ∑ᶠ (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 B : (mulSupport (M := ℝ) fun (i : ι) ↦
    HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ⊆
  (↑s : Set ι)
Tactic: have B : (mulSupport fun i => 1 - f i x) ⊆ s := by
    rw [hs, mulSupport_one_sub]
    exact fun i => id
-- 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
x : X
s : Finset ι :=
  ⋯.toFinset (s := {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)})
hs : (↑s : Set ι) = {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
A : (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x) ⊆ (↑s : Set ι)
B :
  (mulSupport (M := ℝ) fun (i : ι) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ⊆
    (↑s : Set ι)
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ ∑ᶠ (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 rw : Eq (α := ℝ) (∑ i ∈ s, f.toPOUFun (s := s_1) i x)
  (∑ i ∈ s,
    HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
      (∏ j ∈ s with j < i,
          HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) :
        ℝ))
Tactic: rw [finsum_eq_sum_of_support_subset _ A, finprod_eq_prod_of_mulSupport_subset _ B,
    Finset.prod_one_sub_ordered, sub_sub_cancel]
-- 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
x : X
s : Finset ι :=
  ⋯.toFinset (s := {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)})
hs : (↑s : Set ι) = {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
A : (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x) ⊆ (↑s : Set ι)
B :
  (mulSupport (M := ℝ) fun (i : ι) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ⊆
    (↑s : Set ι)
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ Eq (α := ℝ) (∑ i ∈ s, f.toPOUFun (s := s_1) i x)
    (∑ i ∈ s,
      HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
        (∏ j ∈ s with j < i,
            HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) :
          ℝ))
have refine : ∀ i ∈ s,
  f.toPOUFun (s := s_1) i x =
    HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
      (∏ j ∈ s with j < i,
          HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) :
        ℝ)
Tactic: refine Finset.sum_congr rfl fun i _ => ?_
-- 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
x : X
s : Finset ι :=
  ⋯.toFinset (s := {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)})
hs : (↑s : Set ι) = {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
A : (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x) ⊆ (↑s : Set ι)
B :
  (mulSupport (M := ℝ) fun (i : ι) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ⊆
    (↑s : Set ι)
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
h : i ∈ s
⊢ f.toPOUFun (s := s_1) i x =
    HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
      (∏ j ∈ s with j < i,
          HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) :
        ℝ)
have convert_4 : ∀ (j : ι),
  WellOrderingRel j i →
    ∀ (hj : Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)), j ∈ s
Tactic: convert! f.toPOUFun_eq_mul_prod _ _ _ fun j _ hj => _
-- 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
x : X
s : Finset ι :=
  ⋯.toFinset (s := {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)})
hs : (↑s : Set ι) = {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
A : (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x) ⊆ (↑s : Set ι)
B :
  (mulSupport (M := ℝ) fun (i : ι) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ⊆
    (↑s : Set ι)
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
h : i ∈ s
j : ι
h_1 : WellOrderingRel j i
hj : Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ j ∈ s
have convert_4 : Membership.mem (γ := Set ι) {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
  j
Tactic: rwa [Finite.mem_toFinset]
-- 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
x : X
s : Finset ι :=
  ⋯.toFinset (s := {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)})
hs : (↑s : Set ι) = {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
A : (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x) ⊆ (↑s : Set ι)
B :
  (mulSupport (M := ℝ) fun (i : ι) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ⊆
    (↑s : Set ι)
letI letI₁ letI₂ :
  ∑ᶠ (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 : ℝ))
⊢ ∑ᶠ (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 letI₃ : let this : LinearOrder ι := linearOrderOfSTO WellOrderingRel;
Eq (α := ℝ) (∑ i ∈ s, f.toPOUFun (s := s_1) i x)
  (∑ i ∈ s,
    HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
      (∏ j ∈ s with j < i,
          HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) :
        ℝ))
Tactic: classical
  letI : LinearOrder ι := linearOrderOfSTO WellOrderingRel
  rw [finsum_eq_sum_of_support_subset _ A, finprod_eq_prod_of_mulSupport_subset _ B,
    Finset.prod_one_sub_ordered, sub_sub_cancel]
  refine Finset.sum_congr rfl fun i _ => ?_
  convert! f.toPOUFun_eq_mul_prod _ _ _ fun j _ hj => _
  rwa [Finite.mem_toFinset]
-- 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
x : X
s : Finset ι :=
  ⋯.toFinset (s := {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)})
hs : (↑s : Set ι) = {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
A : (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x) ⊆ (↑s : Set ι)
B :
  (mulSupport (M := ℝ) fun (i : ι) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ⊆
    (↑s : Set ι)
letI letI₁ letI₂ :
  ∑ᶠ (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 : ℝ))
letI₃ :
  let this : LinearOrder ι := linearOrderOfSTO WellOrderingRel;
  Eq (α := ℝ) (∑ i ∈ s, f.toPOUFun (s := s_1) i x)
    (∑ i ∈ s,
      HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
        (∏ j ∈ s with j < i,
            HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) :
          ℝ))
⊢ ∑ᶠ (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 letI₄ : let this : LinearOrder ι := linearOrderOfSTO WellOrderingRel;
∀ i ∈ s,
  f.toPOUFun (s := s_1) i x =
    HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
      (∏ j ∈ s with j < i,
          HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) :
        ℝ)
Tactic: classical
  letI : LinearOrder ι := linearOrderOfSTO WellOrderingRel
  rw [finsum_eq_sum_of_support_subset _ A, finprod_eq_prod_of_mulSupport_subset _ B,
    Finset.prod_one_sub_ordered, sub_sub_cancel]
  refine Finset.sum_congr rfl fun i _ => ?_
  convert! f.toPOUFun_eq_mul_prod _ _ _ fun j _ hj => _
  rwa [Finite.mem_toFinset]
-- 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
x : X
s : Finset ι :=
  ⋯.toFinset (s := {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)})
hs : (↑s : Set ι) = {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)}
A : (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x) ⊆ (↑s : Set ι)
B :
  (mulSupport (M := ℝ) fun (i : ι) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ⊆
    (↑s : Set ι)
letI letI₁ letI₂ :
  ∑ᶠ (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 : ℝ))
letI₃ :
  let this : LinearOrder ι := linearOrderOfSTO WellOrderingRel;
  Eq (α := ℝ) (∑ i ∈ s, f.toPOUFun (s := s_1) i x)
    (∑ i ∈ s,
      HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
        (∏ j ∈ s with j < i,
            HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) :
          ℝ))
letI₄ :
  let this : LinearOrder ι := linearOrderOfSTO WellOrderingRel;
  ∀ i ∈ s,
    f.toPOUFun (s := s_1) i x =
      HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
        (∏ j ∈ s with j < i,
            HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) :
          ℝ)
⊢ ∑ᶠ (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 convert_4 : ∀ i ∈ s,
  ∀ (j : ι),
    WellOrderingRel j i →
      ∀ (hj : Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)), j ∈ s
Tactic: classical
  letI : LinearOrder ι := linearOrderOfSTO WellOrderingRel
  rw [finsum_eq_sum_of_support_subset _ A, finprod_eq_prod_of_mulSupport_subset _ B,
    Finset.prod_one_sub_ordered, sub_sub_cancel]
  refine Finset.sum_congr rfl fun i _ => ?_
  convert! f.toPOUFun_eq_mul_prod _ _ _ fun j _ hj => _
  rwa [Finite.mem_toFinset]
-- 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 ι),
    f.toPOUFun (s := s) i =ᶠ[𝓝 x]
      HMul.hMul (α := (a : X) → ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
        (⇑(∏ j ∈ t with WellOrderingRel j i,
              HSub.hSub (α := C(X, ℝ)) (β := C(X, ℝ)) (1 : C(X, ℝ)) ((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ))) :
          (a : X) → ℝ)
have rcases : ∀ (U : Set X) (hU : U ∈ 𝓝 x)
  (hf :
    Set.Finite.{u} (α := ι)
      {i : ι |
        ((fun (i : ι) ↦ (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
            U).Nonempty}),
  ∃ (t : Finset ι),
    f.toPOUFun (s := s) i =ᶠ[𝓝 x]
      HMul.hMul (α := (a : X) → ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
        (⇑(∏ j ∈ t with WellOrderingRel j i,
              HSub.hSub (α := C(X, ℝ)) (β := C(X, ℝ)) (1 : C(X, ℝ)) ((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ))) :
          (a : X) → ℝ)
Tactic: rcases f.locallyFinite x with ⟨U, hU, hf⟩
-- 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
U : Set X
hU : U ∈ 𝓝 x
hf :
  Set.Finite.{u} (α := ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          U).Nonempty}
⊢ ∃ (t : Finset ι),
    f.toPOUFun (s := s) i =ᶠ[𝓝 x]
      HMul.hMul (α := (a : X) → ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
        (⇑(∏ j ∈ t with WellOrderingRel j i,
              HSub.hSub (α := C(X, ℝ)) (β := C(X, ℝ)) (1 : C(X, ℝ)) ((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ))) :
          (a : X) → ℝ)
have h : f.toPOUFun (s := s) i =ᶠ[𝓝 x]
  HMul.hMul (α := (a : X) → ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
    (⇑(∏
          j ∈
            hf.toFinset (s :=
              {i : ι |
                ((fun (i : ι) ↦ (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
                    U).Nonempty}) with
          WellOrderingRel j i,
          HSub.hSub (α := C(X, ℝ)) (β := C(X, ℝ)) (1 : C(X, ℝ)) ((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ))) :
      (a : X) → ℝ)
Tactic: use hf.toFinset
-- 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
U : Set X
hU : U ∈ 𝓝 x
hf :
  Set.Finite.{u} (α := ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          U).Nonempty}
⊢ f.toPOUFun (s := s) i =ᶠ[𝓝 x]
    HMul.hMul (α := (a : X) → ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
      (⇑(∏
            j ∈
              hf.toFinset (s :=
                {i : ι |
                  ((fun (i : ι) ↦ (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
                      U).Nonempty}) with
            WellOrderingRel j i,
            HSub.hSub (α := C(X, ℝ)) (β := C(X, ℝ)) (1 : C(X, ℝ)) ((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ))) :
        (a : X) → ℝ)
have h : ∀ (y : X) (hyU : y ∈ U),
  f.toPOUFun (s := s) i y =
    HMul.hMul (α := (a : X) → ℝ) (β := (a : X) → ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
      (⇑(∏
            j ∈
              hf.toFinset (s :=
                {i : ι | (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ∩ U).Nonempty}) with
            WellOrderingRel j i,
            HSub.hSub (α := C(X, ℝ)) (β := C(X, ℝ)) (1 : C(X, ℝ)) ((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ))) :
        (a : X) → ℝ)
      y
Tactic: filter_upwards [hU] with y hyU
-- 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
U : Set X
hU : U ∈ 𝓝 x
hf :
  Set.Finite.{u} (α := ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          U).Nonempty}
y : X
hyU : y ∈ U
⊢ f.toPOUFun (s := s) i y =
    HMul.hMul (α := (a : X) → ℝ) (β := (a : X) → ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
      (⇑(∏
            j ∈
              hf.toFinset (s :=
                {i : ι | (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ∩ U).Nonempty}) with
            WellOrderingRel j i,
            HSub.hSub (α := C(X, ℝ)) (β := C(X, ℝ)) (1 : C(X, ℝ)) ((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ))) :
        (a : X) → ℝ)
      y
have h : f.toPOUFun (s := s) i y =
  HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) y : ℝ)
    (∏
        c ∈
          hf.toFinset (s :=
            {i : ι | (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ∩ U).Nonempty}) with
        WellOrderingRel c i,
        (HSub.hSub (α := C(X, ℝ)) (β := C(X, ℝ)) (1 : C(X, ℝ)) ((f : (a : ι) → C(X, ℝ)) c : C(X, ℝ)) : (a : X) → ℝ) y :
      ℝ)
Tactic: simp only [ContinuousMap.coe_prod, Pi.mul_apply, Finset.prod_apply]
-- 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
U : Set X
hU : U ∈ 𝓝 x
hf :
  Set.Finite.{u} (α := ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          U).Nonempty}
y : X
hyU : y ∈ U
⊢ f.toPOUFun (s := s) i y =
    HMul.hMul (α := ℝ) (β := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) y : ℝ)
      (∏
          c ∈
            hf.toFinset (s :=
              {i : ι | (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ∩ U).Nonempty}) with
          WellOrderingRel c i,
          (HSub.hSub (α := C(X, ℝ)) (β := C(X, ℝ)) (1 : C(X, ℝ)) ((f : (a : ι) → C(X, ℝ)) c : C(X, ℝ)) : (a : X) → ℝ)
            y :
        ℝ)
have h : ∀ (j : ι),
  WellOrderingRel j i →
    Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) y : ℝ) (0 : ℝ) →
      j ∈
        hf.toFinset (s :=
          {i : ι | (support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) ∩ U).Nonempty})
Tactic: apply toPOUFun_eq_mul_prod
-- 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 : ι
⊢ Continuous[inst, _] (f.toPOUFun (s := s) i)
have refine : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦
  mulSupport (M := ℝ) fun (x : X) ↦
    HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
Tactic: refine (map_continuous <| f i).mul <| continuous_finprod_cond (fun j _ => by fun_prop) ?_
-- 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 : ι
⊢ LocallyFinite.{u, v} (X := X) fun (i : ι) ↦
    mulSupport (M := ℝ) fun (x : X) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
have simp : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)
Tactic: simp only [mulSupport_one_sub]
-- 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
x : X
hx : x ∈ s
⊢ Eq (α := ℝ) (∑ᶠ (i : ι), ({ toFun := f.toPOUFun (s := s) i, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x) 1
have simp : Eq (α := ℝ)
  (∏ᶠ (i : ι), HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) 0
Tactic: simp only [ContinuousMap.coe_mk, sum_toPOUFun_eq, sub_eq_self]
-- 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
x : X
hx : x ∈ s
⊢ Eq (α := ℝ)
    (∏ᶠ (i : ι), HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) 0
have hx₁ : HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) (f.ind (s := s) x hx) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) =
  0
Tactic: apply finprod_eq_zero (fun i => 1 - f i x) (f.ind x hx)
-- 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
x : X
hx : x ∈ s
hx₁ :
  HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ)
      ((((f : (a : ι) → C(X, ℝ)) (f.ind (s := s) x hx) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) =
    0
⊢ Eq (α := ℝ)
    (∏ᶠ (i : ι), HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) 0
have hf : HasFiniteMulSupport (M := ℝ) fun (i : ι) ↦
  HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
Tactic: apply finprod_eq_zero (fun i => 1 - f i x) (f.ind x hx)
-- 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
x : X
hx : x ∈ s
⊢ HasFiniteMulSupport (M := ℝ) fun (i : ι) ↦
    HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
have hf : Set.Finite.{u} (α := ι) (support (M := ℝ) fun (i : ι) ↦ (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)
Tactic: rw [HasFiniteMulSupport, mulSupport_one_sub]
-- 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
x : X
⊢ LE.le (α := ℝ) (∑ᶠ (i : ι), ({ toFun := f.toPOUFun (s := s) i, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x) 1
have simp : LE.le (α := ℝ) 0
  (∏ᶠ (i : ι), HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ))
Tactic: simp only [ContinuousMap.coe_mk, sum_toPOUFun_eq, sub_le_self_iff]