case h.h
α : Type u_4
M : Type u_2
N : Type ?u.336034
P : Type ?u.336037
R : Type u_1
S : Type ?u.336043
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type u_5
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
f : α → α'
g : M →ₗ[R] M'
h : ∀ (i : α), ↑g (v i) = v' (f i)
l : α
⊢ ↑(comp (comp (Finsupp.total α' M' R v') (lmapDomain R R f)) (lsingle l)) 1 =
    ↑(comp (comp g (Finsupp.total α M R v)) (lsingle l)) 1
α : Type u_4
M : Type u_2
N : Type ?u.336034
P : Type ?u.336037
R : Type u_1
S : Type ?u.336043
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type u_5
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
f : α → α'
g : M →ₗ[R] M'
h : ∀ (i : α), ↑g (v i) = v' (f i)
⊢ comp (Finsupp.total α' M' R v') (lmapDomain R R f) = comp g (Finsupp.total α M R v)
ext l
no goals
case h.h
α : Type u_4
M : Type u_2
N : Type ?u.336034
P : Type ?u.336037
R : Type u_1
S : Type ?u.336043
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type u_5
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
f : α → α'
g : M →ₗ[R] M'
h : ∀ (i : α), ↑g (v i) = v' (f i)
l : α
⊢ ↑(comp (comp (Finsupp.total α' M' R v') (lmapDomain R R f)) (lsingle l)) 1 =
    ↑(comp (comp g (Finsupp.total α M R v)) (lsingle l)) 1
simp [total_apply, Finsupp.sum_mapDomain_index, add_smul, h]