Theorem: Cocycle.inv_rel (UnitConjecture/Cocycle.lean)

State before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
⊢ c q (-q) = q +ᵥ c (-q) q
Tactic:
have := ccl.cocycle_condition q (-q) q
State after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q (-q) + c (q + -q) q = q +ᵥ c (-q) q + c q (-q + q)
⊢ c q (-q) = q +ᵥ c (-q) q

State before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q (-q) + c (q + -q) q = q +ᵥ c (-q) q + c q (-q + q)
⊢ c q (-q) = q +ᵥ c (-q) q
Tactic:
simp_all only [add_right_neg, left_id, add_zero, AutAction.vadd_eq, add_left_neg, right_id]
State after:
no goals