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