Theorem: MetabelianGroup.left_inv (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
⊢ mul c (inv c (k, q)) (k, q) = e
Tactic:
have := Cocycle.inv_rel' c q
State after:
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
this : c (-q) q = -q +ᵥ c q (-q)
⊢ mul c (inv c (k, q)) (k, q) = e

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
this : c (-q) q = -q +ᵥ c q (-q)
⊢ mul c (inv c (k, q)) (k, q) = e
Tactic:
aesop (rule_sets [Metabelian, Cocycle, AutAction])
State after:
no goals