aesop (rule_sets [Metabelian]) (add norm [MonoidHom.mem_mker])
case h.mk
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
fst✝ : K
snd✝ : Q
⊢ (fst✝, snd✝) ∈ MonoidHom.mrange (Kernel.inclusion c) ↔ (fst✝, snd✝) ∈ MonoidHom.mker (Quotient.projection c)
no goals