case w
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x✝ : ↑(of { x // x ∈ AddMonoidHom.ker f })
⊢ ↑((kernelIsoKer f).inv ≫ kernel.ι f) x✝ = ↑(AddSubgroup.subtype (AddMonoidHom.ker f)) x✝
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
⊢ (kernelIsoKer f).inv ≫ kernel.ι f = AddSubgroup.subtype (AddMonoidHom.ker f)
ext
no goals
case w
J : Type v
inst✝ : SmallCategory J
G H : AddCommGroupCat
f : G ⟶ H
x✝ : ↑(of { x // x ∈ AddMonoidHom.ker f })
⊢ ↑((kernelIsoKer f).inv ≫ kernel.ι f) x✝ = ↑(AddSubgroup.subtype (AddMonoidHom.ker f)) x✝
simp [kernelIsoKer]