no goals
F : Type u_3
ι : Type ?u.39178
α : Type u_2
β : Type u_1
γ : Type ?u.39187
δ : Type ?u.39190
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ ↑f (a ∆ b) = ↑f a ∆ ↑f b
rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']