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 := inv_rel c (-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) = -q +ᵥ c (- -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) = -q +ᵥ c (- -q) (-q)
⊢ c (-q) q = -q +ᵥ c q (-q)
Tactic:
simp_all only [neg_neg]
State after:
no goals