fix(order/filter/filter_product): remove useless .sets

src/order/filter/filter_product.lean

@@ -6,11 +6,11 @@ universes u v
 variables {α : Type u} (β : Type v) (φ : filter α)
 local attribute [instance] classical.prop_decidable
 
-def bigly_equal : setoid (α → β) := 
-⟨ λ a b, {n | a n = b n} ∈ φ.sets,
-  λ a, by simp only [eq_self_iff_true, (set.univ_def).symm, univ_sets], 
-  λ a b ab, by simpa only [eq_comm], 
-  λ a b c ab bc, sets_of_superset φ (inter_sets φ ab bc) 
+def bigly_equal : setoid (α → β) :=
+⟨ λ a b, {n | a n = b n} ∈ φ,
+  λ a, by simp only [eq_self_iff_true, (set.univ_def).symm, univ_sets],
+  λ a b ab, by simpa only [eq_comm],
+  λ a b c ab bc, sets_of_superset φ (inter_sets φ ab bc)
     (λ n (r : a n = b n ∧ b n = c n), eq.trans r.1 r.2)⟩
 
 def filterprod := quotient (bigly_equal β φ)
@@ -40,15 +40,15 @@ instance am [add_monoid β] : add_monoid β* :=
 { add := has_add.add,
   add_assoc := add_semigroup.add_assoc,
   zero := 0,
-  zero_add := λ x, quotient.induction_on' x 
+  zero_add := λ x, quotient.induction_on' x
     (λ a, quotient.sound'(by simp only [zero_add]; apply (setoid.iseqv _).1)),
-  add_zero := λ x, quotient.induction_on' x 
+  add_zero := λ x, quotient.induction_on' x
     (λ a, quotient.sound'(by simp only [add_zero]; apply (setoid.iseqv _).1)) }
 
 instance acs [add_comm_semigroup β] : add_comm_semigroup β* :=
 { add := has_add.add,
   add_assoc := add_semigroup.add_assoc,
-  add_comm := λ x y, quotient.induction_on₂' x y 
+  add_comm := λ x y, quotient.induction_on₂' x y
     (λ a b, quotient.sound' (by simp only [add_comm]; apply (setoid.iseqv _).1)) }
 
 instance acm [add_comm_monoid β] : add_comm_monoid β* := {..acs β φ, ..am β φ }
@@ -59,9 +59,9 @@ instance ag [add_group β] : add_group β* :=
   zero := 0,
   zero_add := add_monoid.zero_add,
   add_zero := add_monoid.add_zero,
-  neg := λ x, (quotient.lift_on' x (λ a, (quotient.mk' (λ n, - a n) : β*))) 
+  neg := λ x, (quotient.lift_on' x (λ a, (quotient.mk' (λ n, - a n) : β*)))
     (λ a b rab, quotient.sound' (by show _ ∈ _; simpa only [neg_inj'])),
-  add_left_neg := λ x, quotient.induction_on' x 
+  add_left_neg := λ x, quotient.induction_on' x
     (λ a, quotient.sound' (by simp only [add_left_neg]; apply (setoid.iseqv _).1)) }
 
 instance acg [add_comm_group β] : add_comm_group β* := {..acm β φ, ..ag β φ}
@@ -82,15 +82,15 @@ instance m [monoid β] : monoid β* :=
 { mul := has_mul.mul,
   mul_assoc := semigroup.mul_assoc,
   one := 1,
-  one_mul := λ x, quotient.induction_on' x 
+  one_mul := λ x, quotient.induction_on' x
     (λ a, quotient.sound'(by simp only [one_mul]; apply (setoid.iseqv _).1)),
-  mul_one := λ x, quotient.induction_on' x 
+  mul_one := λ x, quotient.induction_on' x
     (λ a, quotient.sound'(by simp only [mul_one]; apply (setoid.iseqv _).1)) }
 
 instance cs [comm_semigroup β] : comm_semigroup β* :=
 { mul := has_mul.mul,
   mul_assoc := semigroup.mul_assoc,
-  mul_comm := λ x y, quotient.induction_on₂' x y 
+  mul_comm := λ x y, quotient.induction_on₂' x y
     (λ a b, quotient.sound' (by simp only [mul_comm]; apply (setoid.iseqv _).1)) }
 
 instance cm [comm_monoid β] : comm_monoid β* := {..cs β φ, ..m β φ }
@@ -101,27 +101,27 @@ instance g [group β] : group β* :=
   one := 1,
   one_mul := monoid.one_mul,
   mul_one := monoid.mul_one,
-  inv := λ x, (quotient.lift_on' x (λ a, (quotient.mk' (λ n, (a n)⁻¹) : β*))) 
+  inv := λ x, (quotient.lift_on' x (λ a, (quotient.mk' (λ n, (a n)⁻¹) : β*)))
     (λ a b rab, quotient.sound' (by show _ ∈ _; simpa only [inv_inj'])),
-  mul_left_inv := λ x, quotient.induction_on' x 
+  mul_left_inv := λ x, quotient.induction_on' x
     (λ a, quotient.sound' (by simp only [mul_left_inv]; apply (setoid.iseqv _).1)) }
 
 instance [comm_group β] : comm_group β* := {..cm β φ, ..g β φ}
 
 instance d [distrib β] : distrib β* :=
 { add := has_add.add,
   mul := has_mul.mul,
-  left_distrib := λ x y z, quotient.induction_on₃' x y z 
+  left_distrib := λ x y z, quotient.induction_on₃' x y z
     (λ x y z, quotient.sound' (by simp only [left_distrib]; apply (setoid.iseqv _).1)),
-  right_distrib := λ x y z, quotient.induction_on₃' x y z 
+  right_distrib := λ x y z, quotient.induction_on₃' x y z
     (λ x y z, quotient.sound' (by simp only [right_distrib]; apply (setoid.iseqv _).1)) }
 
 instance mz [mul_zero_class β] : mul_zero_class β* :=
 { mul := has_mul.mul,
   zero := 0,
-  zero_mul := λ x, quotient.induction_on' x 
+  zero_mul := λ x, quotient.induction_on' x
     (λ a, quotient.sound' (by simp only [zero_mul]; apply (setoid.iseqv _).1)),
-  mul_zero := λ x, quotient.induction_on' x 
+  mul_zero := λ x, quotient.induction_on' x
     (λ a, quotient.sound' (by simp only [mul_zero]; apply (setoid.iseqv _).1)) }
 
 instance sr [semiring β] : semiring β* := { ..acm β φ, ..m β φ, ..d β φ, ..mz β φ }
@@ -138,7 +138,7 @@ variable {U : is_ultrafilter φ} include U
 theorem to_filterprod_inj : function.injective (to_filterprod β φ) :=
 begin
   intros r s rs, by_contra N,
-  rw [to_filterprod, seq_to_filterprod, quotient.eq', bigly_equal] at rs, 
+  rw [to_filterprod, seq_to_filterprod, quotient.eq', bigly_equal] at rs,
   simp only [N, set.set_of_false, empty_in_sets_eq_bot] at rs,
   exact U.1 rs
 end
@@ -147,9 +147,9 @@ instance [zero_ne_one_class β] : zero_ne_one_class β* :=
 { zero := 0,
   one := 1,
   zero_ne_one := by
-  { intro c, have c' : _ := quotient.exact' c, 
-    change _ ∈ _ at c', 
-    simp only [set.set_of_false, zero_ne_one, empty_in_sets_eq_bot] at c', 
+  { intro c, have c' : _ := quotient.exact' c,
+    change _ ∈ _ at c',
+    simp only [set.set_of_false, zero_ne_one, empty_in_sets_eq_bot] at c',
     apply U.1 c' } }
 
 end ultraproduct