ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.16262
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
x : (i : ι) → Ms i
⊢ (Finset.sum Finset.univ fun d =>
      ↑(comp (mapQ (p d) q (f d) (_ : p d ≤ comap (f d) q)) (proj d)) fun i => Quotient.mk (x i)) =
    Finset.sum Finset.univ fun x_1 => ↑(mkQ q) (↑(comp (f x_1) (proj x_1)) x)
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.16262
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
x : (i : ι) → Ms i
⊢ (↑(piQuotientLift p q f hf) fun i => Quotient.mk (x i)) = Quotient.mk (↑(↑(lsum R (fun i => Ms i) R) f) x)
rw [piQuotientLift, lsum_apply, sum_apply, ← mkQ_apply, lsum_apply, sum_apply, _root_.map_sum]
no goals
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type ?u.16262
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
x : (i : ι) → Ms i
⊢ (Finset.sum Finset.univ fun d =>
      ↑(comp (mapQ (p d) q (f d) (_ : p d ≤ comap (f d) q)) (proj d)) fun i => Quotient.mk (x i)) =
    Finset.sum Finset.univ fun x_1 => ↑(mkQ q) (↑(comp (f x_1) (proj x_1)) x)
simp only [coe_proj, mapQ_apply, mkQ_apply, comp_apply]