no goals
α : Type u_1
β : Type ?u.18933
γ : Type ?u.18936
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ (a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) +
      (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)
rw [le_sup_inf_aux, add_self, mul_self, zero_add]