[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a + a = 0
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a + a = (a + a) * (a + a)
[PROOFSTEP]
rw [mul_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ (a + a) * (a + a) = a * a + a * a + (a * a + a * a)
[PROOFSTEP]
rw [add_mul, mul_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a * a + a * a + (a * a + a * a) = a + a + (a + a)
[PROOFSTEP]
rw [mul_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
this : a + a = a + a + (a + a)
⊢ a + a = 0
[PROOFSTEP]
rwa [self_eq_add_left] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ -a = -a + 0
[PROOFSTEP]
rw [add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ -a + 0 = -a + -a + a
[PROOFSTEP]
rw [← neg_add_self, add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ -a + -a + a = a
[PROOFSTEP]
rw [add_self, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a = -b ↔ a = b
[PROOFSTEP]
rw [neg_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a * b + b * a = 0
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a + b = (a + b) * (a + b)
[PROOFSTEP]
rw [mul_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ (a + b) * (a + b) = a * a + a * b + (b * a + b * b)
[PROOFSTEP]
rw [add_mul, mul_add, mul_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a * a + a * b + (b * a + b * b) = a + a * b + (b * a + b)
[PROOFSTEP]
simp only [mul_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + (b * a + b) = a + b + (a * b + b * a)
[PROOFSTEP]
abel
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + (b * a + b) = a + b + (a * b + b * a)
[PROOFSTEP]
abel
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
this : a + b = a + b + (a * b + b * a)
⊢ a * b + b * a = 0
[PROOFSTEP]
rwa [self_eq_add_right] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a - b = a + b
[PROOFSTEP]
rw [sub_eq_add_neg, add_right_inj, neg_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a b : α
⊢ a * (1 + a) = 0
[PROOFSTEP]
rw [mul_add, mul_one, mul_self, add_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a✝ b✝ : α
src✝ : BooleanRing α := inferInstance
a b : α
⊢ a * b = b * a
[PROOFSTEP]
rw [← add_eq_zero', mul_add_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a ⊔ b = b ⊔ a
[PROOFSTEP]
dsimp only [(· ⊔ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a + b + a * b = b + a + b * a
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a ⊓ b = b ⊓ a
[PROOFSTEP]
dsimp only [(· ⊓ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a * b = b * a
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
[PROOFSTEP]
dsimp only [(· ⊔ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ a + b + a * b + c + (a + b + a * b) * c = a + (b + c + b * c) + a * (b + c + b * c)
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
[PROOFSTEP]
dsimp only [(· ⊓ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ a * b * c = a * (b * c)
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a ⊔ a ⊓ b = a
[PROOFSTEP]
dsimp only [(· ⊔ ·), (· ⊓ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a + a * b + a * (a * b) = a
[PROOFSTEP]
rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a ⊓ (a ⊔ b) = a
[PROOFSTEP]
dsimp only [(· ⊔ ·), (· ⊓ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a * (a + b + a * b) = a
[PROOFSTEP]
rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ (a + b + a * b) * (a + c + a * c) =
    a * a + b * c + a * (b * c) + (a * b + a * a * b) + (a * c + a * a * c) + (a * b * c + a * a * b * c)
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ a * a + b * c + a * (b * c) + (a * b + a * a * b) + (a * c + a * a * c) + (a * b * c + a * a * b * c) =
    a + b * c + a * (b * c)
[PROOFSTEP]
simp only [mul_self, add_self, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = a ⊔ b ⊓ c
[PROOFSTEP]
dsimp only [(· ⊔ ·), (· ⊓ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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)
[PROOFSTEP]
rw [le_sup_inf_aux, add_self, mul_self, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
src✝ : Lattice α :=
  Lattice.mk' (_ : ∀ (a b : α), a ⊔ b = b ⊔ a) (_ : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (_ : ∀ (a b : α), a ⊓ b = b ⊓ a) (_ : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (_ : ∀ (a b : α), a ⊔ a ⊓ b = a)
    (_ : ∀ (a b : α), a ⊓ (a ⊔ b) = a)
a : α
⊢ a * (1 + a) + 0 + a * (1 + a) * 0 = 0
[PROOFSTEP]
norm_num [mul_add, mul_self, add_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
src✝ : Lattice α :=
  Lattice.mk' (_ : ∀ (a b : α), a ⊔ b = b ⊔ a) (_ : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (_ : ∀ (a b : α), a ⊓ b = b ⊓ a) (_ : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (_ : ∀ (a b : α), a ⊔ a ⊓ b = a)
    (_ : ∀ (a b : α), a ⊓ (a ⊔ b) = a)
a : α
⊢ ⊤ ≤ a ⊔ aᶜ
[PROOFSTEP]
change 1 + (a + (1 + a) + a * (1 + a)) + 1 * (a + (1 + a) + a * (1 + a)) = a + (1 + a) + a * (1 + a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
src✝ : Lattice α :=
  Lattice.mk' (_ : ∀ (a b : α), a ⊔ b = b ⊔ a) (_ : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (_ : ∀ (a b : α), a ⊓ b = b ⊓ a) (_ : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (_ : ∀ (a b : α), a ⊔ a ⊓ b = a)
    (_ : ∀ (a b : α), a ⊓ (a ⊔ b) = a)
a : α
⊢ 1 + (a + (1 + a) + a * (1 + a)) + 1 * (a + (1 + a) + a * (1 + a)) = a + (1 + a) + a * (1 + a)
[PROOFSTEP]
norm_num [mul_add, mul_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
src✝ : Lattice α :=
  Lattice.mk' (_ : ∀ (a b : α), a ⊔ b = b ⊔ a) (_ : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (_ : ∀ (a b : α), a ⊓ b = b ⊓ a) (_ : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (_ : ∀ (a b : α), a ⊔ a ⊓ b = a)
    (_ : ∀ (a b : α), a ⊓ (a ⊔ b) = a)
a : α
⊢ 1 + (a + (1 + a)) = 0
[PROOFSTEP]
rw [← add_assoc, add_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
src✝ : Lattice α :=
  Lattice.mk' (_ : ∀ (a b : α), a ⊔ b = b ⊔ a) (_ : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (_ : ∀ (a b : α), a ⊓ b = b ⊓ a) (_ : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (_ : ∀ (a b : α), a ⊔ a ⊓ b = a)
    (_ : ∀ (a b : α), a ⊓ (a ⊔ b) = a)
a : α
⊢ a + 1 + a * 1 = 1
[PROOFSTEP]
rw [mul_one, (add_comm a 1), add_assoc, add_self, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
src✝ : Lattice α :=
  Lattice.mk' (_ : ∀ (a b : α), a ⊔ b = b ⊔ a) (_ : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
    (_ : ∀ (a b : α), a ⊓ b = b ⊓ a) (_ : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (_ : ∀ (a b : α), a ⊔ a ⊓ b = a)
    (_ : ∀ (a b : α), a ⊓ (a ⊔ b) = a)
a : α
⊢ 0 + a + 0 * a = a
[PROOFSTEP]
rw [zero_mul, zero_add, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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)
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : α
⊢ a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b) = a + b
[PROOFSTEP]
simp only [mul_self, add_self, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : AsBoolAlg α
⊢ ↑ofBoolAlg (a ∆ b) = ↑ofBoolAlg a + ↑ofBoolAlg b
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a b : AsBoolAlg α
⊢ ↑ofBoolAlg ((a ⊔ b) \ (a ⊓ b)) = ↑ofBoolAlg a + ↑ofBoolAlg b
[PROOFSTEP]
exact of_boolalg_symmDiff_aux _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
f : α →+* β
a b : AsBoolAlg α
⊢ (↑toBoolAlg ∘ ↑f ∘ ↑ofBoolAlg) (a ⊔ b) = (↑toBoolAlg ∘ ↑f ∘ ↑ofBoolAlg) a ⊔ (↑toBoolAlg ∘ ↑f ∘ ↑ofBoolAlg) b
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
f : α →+* β
a b : AsBoolAlg α
⊢ ↑toBoolAlg (↑f (↑ofBoolAlg a + ↑ofBoolAlg b + ↑ofBoolAlg a * ↑ofBoolAlg b)) =
    ↑toBoolAlg (↑f (↑ofBoolAlg a)) ⊔ ↑toBoolAlg (↑f (↑ofBoolAlg b))
[PROOFSTEP]
simp_rw [map_add f, map_mul f, toBoolAlg_add_add_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : Bool
⊢ a * 0 = 0
[PROOFSTEP]
cases a
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ false * 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ true * 0 = 0
[PROOFSTEP]
rfl
