no goals
F : Type u_3
ι : Type ?u.36141
α : Type u_2
β : Type u_1
γ : Type ?u.36150
δ : Type ?u.36153
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ ↑f (a \ b) = ↑f a \ ↑f b
rw [sdiff_eq, sdiff_eq, map_inf, map_compl']