case h.h
ι : Type u_3
R : Type u_1
S : Type ?u.550551
M : ι → Type ?u.550556
N : Type u_2
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : (m : R) → Decidable (m ≠ 0)
p : ι → Submodule R N
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
a✝ : ι
⊢ ↑(LinearMap.comp
          (LinearMap.comp (↑(lsum ℕ) fun i => Submodule.subtype (p i))
            (LinearMap.comp
              (mapRange.linearMap fun i =>
                LinearMap.toSpanSingleton R { x // x ∈ p i } { val := v i, property := (_ : v i ∈ p i) })
              ↑(finsuppLequivDfinsupp R)))
          (Finsupp.lsingle a✝))
      1 =
    ↑(LinearMap.comp (Finsupp.total ι N R v) (Finsupp.lsingle a✝)) 1
ι : Type u_3
R : Type u_1
S : Type ?u.550551
M : ι → Type ?u.550556
N : Type u_2
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : (m : R) → Decidable (m ≠ 0)
p : ι → Submodule R N
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
⊢ LinearMap.comp (↑(lsum ℕ) fun i => Submodule.subtype (p i))
      (LinearMap.comp
        (mapRange.linearMap fun i =>
          LinearMap.toSpanSingleton R { x // x ∈ p i } { val := v i, property := (_ : v i ∈ p i) })
        ↑(finsuppLequivDfinsupp R)) =
    Finsupp.total ι N R v
ext
no goals
case h.h
ι : Type u_3
R : Type u_1
S : Type ?u.550551
M : ι → Type ?u.550556
N : Type u_2
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : (m : R) → Decidable (m ≠ 0)
p : ι → Submodule R N
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
a✝ : ι
⊢ ↑(LinearMap.comp
          (LinearMap.comp (↑(lsum ℕ) fun i => Submodule.subtype (p i))
            (LinearMap.comp
              (mapRange.linearMap fun i =>
                LinearMap.toSpanSingleton R { x // x ∈ p i } { val := v i, property := (_ : v i ∈ p i) })
              ↑(finsuppLequivDfinsupp R)))
          (Finsupp.lsingle a✝))
      1 =
    ↑(LinearMap.comp (Finsupp.total ι N R v) (Finsupp.lsingle a✝)) 1
simp