no goals
F : Type u_3
α : Type u_2
β : Type u_1
γ : Type ?u.40368
δ : Type ?u.40371
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a b : α
⊢ ↑f (a ∆ b) = ↑f a ∆ ↑f b
simp_rw [symmDiff, map_sup, map_sdiff]