Oh don't need to intro either

Changes

1 changed files (+2/-4)

• Set.lean
  • @@ -39,13 +39,11 @@ example : CommRing (Set α) where
    add_comm := by simp only [add_def] grind - left_distrib := by - intro a b c + left_distrib a b c := by ext x simp [symmDiff_def] grind - right_distrib := by - intro a b c + right_distrib a b c := by ext x simp [symmDiff_def] grind