no goals
ι : Type ?u.60714
α : Type u_1
β : Type ?u.60720
π : ι → Type ?u.60725
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)
simp_rw [@inf_comm _ _ _ c, inf_symmDiff_distrib_left]