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