aesop (rule_sets [Metabelian, Cocycle, AutAction]) 
    (options := {terminal := false, warnOnNonterminal := false})
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ mul c (mul c (k, q) (k', q')) (k'', q'') = mul c (k, q) (mul c (k', q') (k'', q''))
case left
Q : Type u_2
K : Type u_1
inst : AddGroup Q
inst_1 : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ k + ↑(Cocycle.α c q) k' + c q q' + ↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + c (q + q') q'' =
    k + (↑(Cocycle.α c q) k' + ↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + ↑(Cocycle.α c q) (c q' q'')) + c q (q' + q'')

case right
Q : Type u_2
K : Type u_1
inst : AddGroup Q
inst_1 : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ q + q' + q'' = q + (q' + q'')