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
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 : ℝ)
rw : WellOrderingRel j i → j ∈ t
⊢ WellOrderingRel j i ↔ j ∈ {j ∈ t | WellOrderingRel j i}

Tactic:
rw [Finset.mem_filter, Iff.comm, and_iff_right_iff_imp]

Premises used: and_iff_right_iff_imp, Finset.mem_filter, Iff.comm
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht :
  ∀ (j : ι),
    WellOrderingRel j i → Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ) → j ∈ t
j : ι
hj : ¬Eq (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ WellOrderingRel j i → j ∈ t

Tactic:
flip (ht j) hj

Premises used: flip
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht :
  ∀ (j : ι),
    WellOrderingRel j i → Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ) → j ∈ t
j : ι
hj : ¬Eq (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ WellOrderingRel j i → j ∈ t

Tactic:
exact flip (ht j) hj

Premises used: flip
-- Module: Mathlib.Topology.PartitionOfUnity
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 : ℝ)})
⊢ (↑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 _
-- Module: Mathlib.Topology.PartitionOfUnity
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 : ℝ)}
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 : ℝ)}
⊢ (support (M := ℝ) fun (i : ι) ↦ f.toPOUFun (s := s_1) i x) ⊆ (↑s : Set ι)

Tactic:
rw [hs]
-- Module: Mathlib.Topology.PartitionOfUnity
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 : ℝ)}
⊢ 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:
fun i hi => f.support_toPOUFun_subset i hi

Premises used: BumpCovering.support_toPOUFun_subset, Set.Mem, setOf, Set.Subset, Function.support
-- Module: Mathlib.Topology.PartitionOfUnity
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 : ℝ)}
⊢ 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:
exact fun i hi => f.support_toPOUFun_subset i hi

Premises used: BumpCovering.support_toPOUFun_subset
-- Module: Mathlib.Topology.PartitionOfUnity
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 ι)

Tactic:
have A : (support fun i => toPOUFun f i x) ⊆ s := by
    rw [hs]
    exact fun i hi => f.support_toPOUFun_subset i hi
-- Module: Mathlib.Topology.PartitionOfUnity
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 ι)
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 : ℝ)}
⊢ (mulSupport (M := ℝ) fun (i : ι) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)) ⊆
    (↑s : Set ι)

Tactic:
rw [hs, mulSupport_one_sub]

Premises used: Function.mulSupport_one_sub
-- Module: Mathlib.Topology.PartitionOfUnity
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 ι)
⊢ 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:
fun i => id

Premises used: Set.Mem, setOf, id, Set.Subset, Function.support
-- Module: Mathlib.Topology.PartitionOfUnity
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 ι)
⊢ 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:
exact fun i => id

Premises used: id
-- Module: Mathlib.Topology.PartitionOfUnity
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 ι)

Tactic:
have B : (mulSupport fun i => 1 - f i x) ⊆ s := by
    rw [hs, mulSupport_one_sub]
    exact fun i => id
-- Module: Mathlib.Topology.PartitionOfUnity
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
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 : ℝ) :
          ℝ))
⊢ ∑ᶠ (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 : ℝ))

Tactic:
rw [finsum_eq_sum_of_support_subset _ A, finprod_eq_prod_of_mulSupport_subset _ B,
    Finset.prod_one_sub_ordered, sub_sub_cancel]

Premises used: Finset.prod_one_sub_ordered, sub_sub_cancel, finsum_eq_sum_of_support_subset, finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Topology.PartitionOfUnity
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 : ℝ) :
          ℝ))

Tactic:
Finset.sum_congr rfl fun i _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Topology.PartitionOfUnity
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
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 : ℝ) :
          ℝ)
⊢ 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:
refine Finset.sum_congr rfl fun i _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Topology.PartitionOfUnity
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 WellOrderingRel j i,
          HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) :
        ℝ)

Tactic:
f.toPOUFun_eq_mul_prod _ _ _ fun j _ hj => _

Premises used: BumpCovering.toPOUFun_eq_mul_prod
-- Module: Mathlib.Topology.PartitionOfUnity
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
convert_4 :
  ∀ (j : ι),
    WellOrderingRel j i →
      ∀ (hj : Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)), j ∈ 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:
convert! f.toPOUFun_eq_mul_prod _ _ _ fun j _ hj => _

Premises used: BumpCovering.toPOUFun_eq_mul_prod
-- Module: Mathlib.Topology.PartitionOfUnity
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 : ℝ)
convert_4 convert_4₁ convert_4₂ convert_4₃ :
  Membership.mem (γ := Set ι)
    {i : ι | Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)} j
⊢ j ∈ s

Tactic:
rwa [Finite.mem_toFinset]

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.Topology.PartitionOfUnity
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 : ℝ) :
          ℝ)
convert_4 :
  ∀ i ∈ s,
    ∀ (j : ι),
      WellOrderingRel j i →
        ∀ (hj : Ne (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) j : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)), j ∈ s
⊢ ∑ᶠ (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 : ℝ))

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]

Premises used: Finset.prod_one_sub_ordered, Set.Finite.mem_toFinset, sub_sub_cancel, finsum_eq_sum_of_support_subset, BumpCovering.toPOUFun_eq_mul_prod, Finset.sum_congr, finprod_eq_prod_of_mulSupport_subset, rfl
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
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) → ℝ)
⊢ ∃ (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⟩

Premises used: BumpCovering.locallyFinite
-- Module: Mathlib.Topology.PartitionOfUnity
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}
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) → ℝ)
⊢ ∃ (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:
use hf.toFinset

Premises used: Set.Finite.toFinset
-- Module: Mathlib.Topology.PartitionOfUnity
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}
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
⊢ 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:
filter_upwards [hU] with y hyU
-- Module: Mathlib.Topology.PartitionOfUnity
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
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 :
        ℝ)
⊢ 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:
simp only [ContinuousMap.coe_prod, Pi.mul_apply, Finset.prod_apply]

Premises used: Pi.mul_apply, Finset.prod_apply, ContinuousMap.coe_prod
-- Module: Mathlib.Topology.PartitionOfUnity
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
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})
⊢ 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:
apply toPOUFun_eq_mul_prod

Premises used: BumpCovering.toPOUFun_eq_mul_prod