case h.h
α : Type u_4
M : Type u_1
N : Type ?u.445605
P : Type ?u.445608
R : Type u_2
S : Type ?u.445614
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_3
M' : Type ?u.445709
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
f : α' → α
a✝ : α'
⊢ ↑(comp (Finsupp.total α' M R (v ∘ f)) (lsingle a✝)) 1 =
    ↑(comp (comp (Finsupp.total α M R v) (lmapDomain R R f)) (lsingle a✝)) 1
α : Type u_4
M : Type u_1
N : Type ?u.445605
P : Type ?u.445608
R : Type u_2
S : Type ?u.445614
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_3
M' : Type ?u.445709
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
f : α' → α
⊢ Finsupp.total α' M R (v ∘ f) = comp (Finsupp.total α M R v) (lmapDomain R R f)
ext
no goals
case h.h
α : Type u_4
M : Type u_1
N : Type ?u.445605
P : Type ?u.445608
R : Type u_2
S : Type ?u.445614
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_3
M' : Type ?u.445709
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
f : α' → α
a✝ : α'
⊢ ↑(comp (Finsupp.total α' M R (v ∘ f)) (lsingle a✝)) 1 =
    ↑(comp (comp (Finsupp.total α M R v) (lmapDomain R R f)) (lsingle a✝)) 1
simp [total_apply]