-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
@[to_additive]
lemma HasProd.sum {α β M : Type*} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M]
    {f : α ⊕ β → M} {a b : M}
    (h₁ : HasProd (f ∘ Sum.inl) a) (h₂ : HasProd (f ∘ Sum.inr) b) : HasProd f (a * b)

Proof state:
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Tendsto ((fun x => ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) (Filter.map (⇑sumEquiv) atTop) (𝓝 (a * b))

Tactic:
rw [Finset.sumEquiv.map_atTop, ← prod_atTop_atTop_eq]

Result:
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Tendsto ((fun x => ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) (atTop ×ˢ atTop) (𝓝 (a * b))

Proof state:
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Tendsto ((fun x => ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) (atTop ×ˢ atTop) (𝓝 (a * b))

Tactic:
convert (tendsto_mul.comp (nhds_prod_eq (x := a) (y := b) ▸ Tendsto.prod_map h₁ h₂))

Result:
case h.e'_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ (fun x => ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm =
    (fun p => p.1 * p.2) ∘ Prod.map (fun s => ∏ b ∈ s, (f ∘ Sum.inl) b) fun s => ∏ b ∈ s, (f ∘ Sum.inr) b

Proof state:
case h.e'_3.h
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
s : Finset α × Finset β
⊢ ((fun x => ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) s =
    ((fun p => p.1 * p.2) ∘ Prod.map (fun s => ∏ b ∈ s, (f ∘ Sum.inl) b) fun s => ∏ b ∈ s, (f ∘ Sum.inr) b) s

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ (fun x => ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm =
    (fun p => p.1 * p.2) ∘ Prod.map (fun s => ∏ b ∈ s, (f ∘ Sum.inl) b) fun s => ∏ b ∈ s, (f ∘ Sum.inr) b

Tactic:
ext s

Result:
case h.e'_3.h
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
s : Finset α × Finset β
⊢ ((fun x => ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) s =
    ((fun p => p.1 * p.2) ∘ Prod.map (fun s => ∏ b ∈ s, (f ∘ Sum.inl) b) fun s => ∏ b ∈ s, (f ∘ Sum.inr) b) s

Proof state:
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
this : Tendsto ((fun x => ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) (Filter.map (⇑sumEquiv) atTop) (𝓝 (a * b))
⊢ HasProd f (a * b)

Tactic:
simpa [Tendsto, ← Filter.map_map] using this

Result:
no goals