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

State before:
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''))
Tactic:
aesop (rule_sets [Metabelian, Cocycle, AutAction]) 
    (options := {terminal := false, warnOnNonterminal := false})
State after:
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'')

State before:
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'')
Tactic:
simp only [add_assoc, add_left_cancel_iff]
State after:
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
⊢ c q q' + (↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + c (q + q') q'') =
    ↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + (↑(Cocycle.α c q) (c q' q'') + c q (q' + q''))

State before:
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
⊢ c q q' + (↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + c (q + q') q'') =
    ↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + (↑(Cocycle.α c q) (c q' q'') + c q (q' + q''))
Tactic:
rw [add_left_comm, add_left_cancel_iff]
State after:
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
⊢ c q q' + c (q + q') q'' = ↑(Cocycle.α c q) (c q' q'') + c q (q' + q'')

State before:
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
⊢ c q q' + c (q + q') q'' = ↑(Cocycle.α c q) (c q' q'') + c q (q' + q'')
Tactic:
exact ccl.cocycle_condition q q' q''
State after:
no goals

State before:
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'')
Tactic:
apply add_assoc
State after:
no goals