α : Type u
β : Type v
γ : Type w
s s₁✝ s₂✝ : Finset α
a : α
b : β
f g : α → β
inst✝ : NonUnitalNonAssocSemiring β
ι₁ : Type u_1
ι₂ : Type u_2
s₁ : Finset ι₁
s₂ : Finset ι₂
f₁ : ι₁ → β
f₂ : ι₂ → β
⊢ ∀ (x : ι₁), x ∈ s₁ → f₁ x * ∑ x₂ in s₂, f₂ x₂ = ∑ y in s₂, f₁ (x, y).fst * f₂ (x, y).snd
α : Type u
β : Type v
γ : Type w
s s₁✝ s₂✝ : Finset α
a : α
b : β
f g : α → β
inst✝ : NonUnitalNonAssocSemiring β
ι₁ : Type u_1
ι₂ : Type u_2
s₁ : Finset ι₁
s₂ : Finset ι₂
f₁ : ι₁ → β
f₂ : ι₂ → β
⊢ (∑ x₁ in s₁, f₁ x₁) * ∑ x₂ in s₂, f₂ x₂ = ∑ p in s₁ ×ˢ s₂, f₁ p.fst * f₂ p.snd
rw [sum_product, sum_mul, sum_congr rfl]
α : Type u
β : Type v
γ : Type w
s s₁✝ s₂✝ : Finset α
a : α
b : β
f g : α → β
inst✝ : NonUnitalNonAssocSemiring β
ι₁ : Type u_1
ι₂ : Type u_2
s₁ : Finset ι₁
s₂ : Finset ι₂
f₁ : ι₁ → β
f₂ : ι₂ → β
x✝ : ι₁
a✝ : x✝ ∈ s₁
⊢ f₁ x✝ * ∑ x₂ in s₂, f₂ x₂ = ∑ y in s₂, f₁ (x✝, y).fst * f₂ (x✝, y).snd
α : Type u
β : Type v
γ : Type w
s s₁✝ s₂✝ : Finset α
a : α
b : β
f g : α → β
inst✝ : NonUnitalNonAssocSemiring β
ι₁ : Type u_1
ι₂ : Type u_2
s₁ : Finset ι₁
s₂ : Finset ι₂
f₁ : ι₁ → β
f₂ : ι₂ → β
⊢ ∀ (x : ι₁), x ∈ s₁ → f₁ x * ∑ x₂ in s₂, f₂ x₂ = ∑ y in s₂, f₁ (x, y).fst * f₂ (x, y).snd
intros
no goals
α : Type u
β : Type v
γ : Type w
s s₁✝ s₂✝ : Finset α
a : α
b : β
f g : α → β
inst✝ : NonUnitalNonAssocSemiring β
ι₁ : Type u_1
ι₂ : Type u_2
s₁ : Finset ι₁
s₂ : Finset ι₂
f₁ : ι₁ → β
f₂ : ι₂ → β
x✝ : ι₁
a✝ : x✝ ∈ s₁
⊢ f₁ x✝ * ∑ x₂ in s₂, f₂ x₂ = ∑ y in s₂, f₁ (x✝, y).fst * f₂ (x✝, y).snd
rw [mul_sum]