case w
G H : AddCommGroupCat
f : G ⟶ H
x✝ : ↑G
⊢ ↑(factorThruImage f ≫ ι f) x✝ = ↑f x✝
G H : AddCommGroupCat
f : G ⟶ H
⊢ factorThruImage f ≫ ι f = f
ext
no goals
case w
G H : AddCommGroupCat
f : G ⟶ H
x✝ : ↑G
⊢ ↑(factorThruImage f ≫ ι f) x✝ = ↑f x✝
rfl