Theorem: AutAction.vadd_dist (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' : B}, a +ᵥ (b + b') = a +ᵥ b + (a +ᵥ b')
Tactic:
aesop (rule_sets [AutAction])
State after:
no goals