no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.16844
V : Set (α × α)
⊢ SymmetricRel (symmetrizeRel V)
simp [SymmetricRel, symmetrizeRel, preimage_inter, inter_comm, ← preimage_comp]