case mk
ι : Type u_2
α : Type u_1
X : Type ?u.408366
M : Type u_3
N : Type ?u.408372
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
l : List ι
⊢ (∀ (i : ι), i ∈ Quot.mk Setoid.r l → Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b => Multiset.prod (Multiset.map (fun c => f c b) (Quot.mk Setoid.r l))) x
      (𝓝 (Multiset.prod (Multiset.map a (Quot.mk Setoid.r l))))
ι : Type u_2
α : Type u_1
X : Type ?u.408366
M : Type u_3
N : Type ?u.408372
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
⊢ (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b => Multiset.prod (Multiset.map (fun c => f c b) s)) x (𝓝 (Multiset.prod (Multiset.map a s)))
rcases s with ⟨l⟩
no goals
case mk
ι : Type u_2
α : Type u_1
X : Type ?u.408366
M : Type u_3
N : Type ?u.408372
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
l : List ι
⊢ (∀ (i : ι), i ∈ Quot.mk Setoid.r l → Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b => Multiset.prod (Multiset.map (fun c => f c b) (Quot.mk Setoid.r l))) x
      (𝓝 (Multiset.prod (Multiset.map a (Quot.mk Setoid.r l))))
simpa using tendsto_list_prod l