no goals
ι : Type ?u.60196
α : Type u_1
β : Type ?u.60202
π : ι → Type ?u.60207
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)
rw [symmDiff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left,
  symmDiff_eq_sup_sdiff_inf]