case hs
ι : Type u_3
α : Type ?u.447147
X✝ : Type ?u.447150
M✝ : Type ?u.447153
N : Type ?u.447156
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_1
M : Type u_2
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ (i : ι), i ∈ s → f i =ᶠ[l] g i
⊢ ∀ᶠ (x : X) in l, ∀ (i : ι), i ∈ s → f i x = g i x

ι : Type u_3
α : Type ?u.447147
X✝ : Type ?u.447150
M✝ : Type ?u.447153
N : Type ?u.447156
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_1
M : Type u_2
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ (i : ι), i ∈ s → f i x = g i x
⊢ ∏ i in s, f i =ᶠ[l] ∏ i in s, g i
ι : Type u_3
α : Type ?u.447147
X✝ : Type ?u.447150
M✝ : Type ?u.447153
N : Type ?u.447156
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_1
M : Type u_2
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ (i : ι), i ∈ s → f i =ᶠ[l] g i
⊢ ∏ i in s, f i =ᶠ[l] ∏ i in s, g i
replace hs : ∀ᶠ x in l, ∀ i ∈ s, f i x = g i x
case h
ι : Type u_3
α : Type ?u.447147
X✝ : Type ?u.447150
M✝ : Type ?u.447153
N : Type ?u.447156
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_1
M : Type u_2
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ (i : ι), i ∈ s → f i x = g i x
x : X
hx : ∀ (i : ι), i ∈ s → f i x = g i x
⊢ Finset.prod s (fun i => f i) x = Finset.prod s (fun i => g i) x
ι : Type u_3
α : Type ?u.447147
X✝ : Type ?u.447150
M✝ : Type ?u.447153
N : Type ?u.447156
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_1
M : Type u_2
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ (i : ι), i ∈ s → f i x = g i x
⊢ ∏ i in s, f i =ᶠ[l] ∏ i in s, g i
filter_upwards [hs]with x hx
no goals
case h
ι : Type u_3
α : Type ?u.447147
X✝ : Type ?u.447150
M✝ : Type ?u.447153
N : Type ?u.447156
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_1
M : Type u_2
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ (i : ι), i ∈ s → f i x = g i x
x : X
hx : ∀ (i : ι), i ∈ s → f i x = g i x
⊢ Finset.prod s (fun i => f i) x = Finset.prod s (fun i => g i) x
simp only [Finset.prod_apply, Finset.prod_congr rfl hx]
no goals
case hs
ι : Type u_3
α : Type ?u.447147
X✝ : Type ?u.447150
M✝ : Type ?u.447153
N : Type ?u.447156
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_1
M : Type u_2
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ (i : ι), i ∈ s → f i =ᶠ[l] g i
⊢ ∀ᶠ (x : X) in l, ∀ (i : ι), i ∈ s → f i x = g i x
rwa [eventually_all_finset]