α : Type u_1
β : Type ?u.4614
γ : Type ?u.4617
inst✝ : BooleanRing α
a b : α
this : a + b = a + b + (a * b + b * a)
⊢ a * b + b * a = 0
α : Type u_1
β : Type ?u.4614
γ : Type ?u.4617
inst✝ : BooleanRing α
a b : α
⊢ a * b + b * a = 0
have : a + b = a + b + (a * b + b * a) :=
  calc
    a + b = (a + b) * (a + b) := by rw [mul_self]
    _ = a * a + a * b + (b * a + b * b) := by rw [add_mul, mul_add, mul_add]
    _ = a + a * b + (b * a + b) := by simp only [mul_self]
    _ = a + b + (a * b + b * a) := by abel
no goals
α : Type u_1
β : Type ?u.4614
γ : Type ?u.4617
inst✝ : BooleanRing α
a b : α
this : a + b = a + b + (a * b + b * a)
⊢ a * b + b * a = 0
rwa [self_eq_add_right] at this
no goals
α : Type u_1
β : Type ?u.4614
γ : Type ?u.4617
inst✝ : BooleanRing α
a b : α
⊢ a + b = (a + b) * (a + b)
rw [mul_self]
no goals
α : Type u_1
β : Type ?u.4614
γ : Type ?u.4617
inst✝ : BooleanRing α
a b : α
⊢ (a + b) * (a + b) = a * a + a * b + (b * a + b * b)
rw [add_mul, mul_add, mul_add]
no goals
α : Type u_1
β : Type ?u.4614
γ : Type ?u.4617
inst✝ : BooleanRing α
a b : α
⊢ a * a + a * b + (b * a + b * b) = a + a * b + (b * a + b)
simp only [mul_self]
no goals
α : Type u_1
β : Type ?u.4614
γ : Type ?u.4617
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + (b * a + b) = a + b + (a * b + b * a)
abel