Remove useless junk in Set.lean

Changes

1 changed files (+0/-17)

• Set.lean
  • @@ -2,23 +2,6 @@ import Mathlib
    open symmDiff - -- open Set - - -- #eval {1, 2, 3} ∆ {3, 6} - - example [Monoid M] (N : Submonoid M) : Monoid N where - mul := fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨x*y, N.mul_mem hx hy⟩ - mul_assoc := by grind - one := ⟨1, N.one_mem⟩ - one_mul := fun ⟨x, _⟩ ↦ SetCoe.ext (one_mul x) - mul_one := fun ⟨x, _⟩ ↦ SetCoe.ext (mul_one x) - - #check Set.symmDiff_def - - #synth Add ℕ - - -- #synth symmDiff (Set ℕ) (Set ℕ) - instance : Add (Set α) := ⟨fun a b ↦ a ∆ b⟩ @[simp]