case h
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ ↑(F.map f ≫ coconeMorphism F j') x✝ = ↑(coconeMorphism F j) x✝
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j
ext
case h.a
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j' (↑(F.map f) x✝)) (Prequotient.of j x✝)
case h
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ ↑(F.map f ≫ coconeMorphism F j') x✝ = ↑(coconeMorphism F j) x✝
apply Quot.sound
no goals
case h.a
R : Type u
inst✝¹ : Ring R
J : Type w
inst✝ : Category J
F : J ⥤ ModuleCat R
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ Setoid.r (Prequotient.of j' (↑(F.map f) x✝)) (Prequotient.of j x✝)
apply ModuleCat.Colimits.Relation.map