no goals
M : Type u_3
N : Type ?u.1873
P : Type ?u.1876
α : Type u_1
β : Type u_2
γ : Type ?u.1885
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul N α
inst✝ : SMul N β
a : M
b : α
c : β
x : α ⊕ β
⊢ swap (a • x) = a • swap x
cases x <;> rfl