Theorem: AutAction.act_neg_act (UnitConjecture/Cocycle.lean)

State before:
A : Type u_2
B : Type u_1
inst✝² : AddGroup A
inst✝¹ : AddGroup B
α : A → B →+ B
inst✝ : AutAction α
a : A
b : B
⊢ ↑(α a) (↑(α (-a)) b) = b
Tactic:
rw [compatibility']
State after:
A : Type u_2
B : Type u_1
inst✝² : AddGroup A
inst✝¹ : AddGroup B
α : A → B →+ B
inst✝ : AutAction α
a : A
b : B
⊢ ↑(α (a + -a)) b = b

State before:
A : Type u_2
B : Type u_1
inst✝² : AddGroup A
inst✝¹ : AddGroup B
α : A → B →+ B
inst✝ : AutAction α
a : A
b : B
⊢ ↑(α (a + -a)) b = b
Tactic:
aesop (erase compatibility) (rule_sets [AutAction])
State after:
no goals