no goals
α : Type u_1
β : Type ?u.14060
γ : Type ?u.14063
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a + a * b + a * (a * b) = a
rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]