Theorem: MetabelianGroup.exact_seq (UnitConjecture/MetabelianGroup.lean)

State before:
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
⊢ MonoidHom.mrange (Kernel.inclusion c) = MonoidHom.mker (Quotient.projection c)
Tactic:
ext ⟨_, _⟩
State after:
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)

State before:
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)
Tactic:
aesop (rule_sets [Metabelian]) (add norm [MonoidHom.mem_mker])
State after:
no goals