case intro.intro
ι : 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 {i | Set.Nonempty ((fun i => support ↑(toFun s f i)) i ∩ U)}
⊢ ∃ t, toPouFun f i =ᶠ[𝓝 x] ↑(toFun s f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) t, (1 - toFun s f j))
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
⊢ ∃ t, toPouFun f i =ᶠ[𝓝 x] ↑(toFun s f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) t, (1 - toFun s f j))
rcases f.locallyFinite x with ⟨U, hU, hf⟩
case intro.intro
ι : 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 {i | Set.Nonempty ((fun i => support ↑(toFun s f i)) i ∩ U)}
⊢ toPouFun f i =ᶠ[𝓝 x]
    ↑(toFun s f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) (Finite.toFinset hf), (1 - toFun s f j))
case intro.intro
ι : 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 {i | Set.Nonempty ((fun i => support ↑(toFun s f i)) i ∩ U)}
⊢ ∃ t, toPouFun f i =ᶠ[𝓝 x] ↑(toFun s f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) t, (1 - toFun s f j))
use hf.toFinset
case h
ι : 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 {i | Set.Nonempty ((fun i => support ↑(toFun s f i)) i ∩ U)}
y : X
hyU : y ∈ U
⊢ toPouFun f i y =
    (↑(toFun s f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) (Finite.toFinset hf), (1 - toFun s f j))) y
case intro.intro
ι : 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 {i | Set.Nonempty ((fun i => support ↑(toFun s f i)) i ∩ U)}
⊢ toPouFun f i =ᶠ[𝓝 x]
    ↑(toFun s f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) (Finite.toFinset hf), (1 - toFun s f j))
filter_upwards [hU]with y hyU
case h
ι : 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 {i | Set.Nonempty ((fun i => support ↑(toFun s f i)) i ∩ U)}
y : X
hyU : y ∈ U
⊢ toPouFun f i y =
    ↑(toFun s f i) y * ∏ c in Finset.filter (fun j => WellOrderingRel j i) (Finite.toFinset hf), ↑(1 - toFun s f c) y
case h
ι : 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 {i | Set.Nonempty ((fun i => support ↑(toFun s f i)) i ∩ U)}
y : X
hyU : y ∈ U
⊢ toPouFun f i y =
    (↑(toFun s f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) (Finite.toFinset hf), (1 - toFun s f j))) y
simp only [ContinuousMap.coe_prod, Pi.mul_apply, Finset.prod_apply]
case h.ht
ι : 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 {i | Set.Nonempty ((fun i => support ↑(toFun s f i)) i ∩ U)}
y : X
hyU : y ∈ U
⊢ ∀ (j : ι), WellOrderingRel j i → ↑(toFun s f j) y ≠ 0 → j ∈ Finite.toFinset hf
case h
ι : 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 {i | Set.Nonempty ((fun i => support ↑(toFun s f i)) i ∩ U)}
y : X
hyU : y ∈ U
⊢ toPouFun f i y =
    ↑(toFun s f i) y * ∏ c in Finset.filter (fun j => WellOrderingRel j i) (Finite.toFinset hf), ↑(1 - toFun s f c) y
apply toPouFun_eq_mul_prod
case h.ht
ι : 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 {i | Set.Nonempty ((fun i => support ↑(toFun s f i)) i ∩ U)}
y : X
hyU : y ∈ U
j : ι
a✝ : WellOrderingRel j i
hj : ↑(toFun s f j) y ≠ 0
⊢ j ∈ Finite.toFinset hf
case h.ht
ι : 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 {i | Set.Nonempty ((fun i => support ↑(toFun s f i)) i ∩ U)}
y : X
hyU : y ∈ U
⊢ ∀ (j : ι), WellOrderingRel j i → ↑(toFun s f j) y ≠ 0 → j ∈ Finite.toFinset hf
intro j _ hj
no goals
case h.ht
ι : 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 {i | Set.Nonempty ((fun i => support ↑(toFun s f i)) i ∩ U)}
y : X
hyU : y ∈ U
j : ι
a✝ : WellOrderingRel j i
hj : ↑(toFun s f j) y ≠ 0
⊢ j ∈ Finite.toFinset hf
exact hf.mem_toFinset.2 ⟨y, ⟨hj, hyU⟩⟩