no goals
ι : Type u_5
R : Type u_3
S : Type ?u.164559
M : ι → Type ?u.164564
N : Type u_4
dec_ι : DecidableEq ι
inst✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → Module R (M i)
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
β : ι → Type ?u.164654
β₁ : ι → Type u_1
β₂ : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommMonoid (β i)
inst✝⁶ : (i : ι) → AddCommMonoid (β₁ i)
inst✝⁵ : (i : ι) → AddCommMonoid (β₂ i)
inst✝⁴ : (i : ι) → Module R (β i)
inst✝³ : (i : ι) → Module R (β₁ i)
inst✝² : (i : ι) → Module R (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i →ₗ[R] β₂ i
h : (i : ι) → β₂ i →ₗ[R] N
l : Π₀ (i : ι), β₁ i
⊢ ↑(↑(lsum ℕ) h) (↑(mapRange.linearMap f) l) = ↑(↑(lsum ℕ) fun i => LinearMap.comp (h i) (f i)) l
simpa [Dfinsupp.sumAddHom_apply] using sum_mapRange_index fun i => by simp
no goals
ι : Type u_5
R : Type u_3
S : Type ?u.164559
M : ι → Type ?u.164564
N : Type u_4
dec_ι : DecidableEq ι
inst✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → Module R (M i)
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
β : ι → Type ?u.164654
β₁ : ι → Type u_1
β₂ : ι → Type u_2
inst✝⁷ : (i : ι) → AddCommMonoid (β i)
inst✝⁶ : (i : ι) → AddCommMonoid (β₁ i)
inst✝⁵ : (i : ι) → AddCommMonoid (β₂ i)
inst✝⁴ : (i : ι) → Module R (β i)
inst✝³ : (i : ι) → Module R (β₁ i)
inst✝² : (i : ι) → Module R (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i →ₗ[R] β₂ i
h : (i : ι) → β₂ i →ₗ[R] N
l : Π₀ (i : ι), β₁ i
i : ι
⊢ ↑(h i) 0 = 0
simp