no goals
α : Type u_1
β : Type ?u.35972
γ : Type ?u.35975
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ (a + b + a * b) * (1 + a * b) = a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b)
ring
no goals
α : Type u_1
β : Type ?u.35972
γ : Type ?u.35975
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b) = a + b
simp only [mul_self, add_self, add_zero]