fix(data/setoid/partition): make def more readable (#8951)

If we change the statement of `partition.order_iso` from `setoid α ≃o subtype (@is_partition α)` to `setoid α ≃o {C : set (set α) // is_partition C}` then this doesn't change anything up to defeq and it's much easier for a beginner to read, as well as avoiding the `@`. I also change some variable names. Why? I want to show this part of this file to undergraduates and I want to make it look as easy and nice as possible.

src/data/setoid/partition.lean

@@ -191,15 +191,16 @@ instance partition.partial_order : partial_order (subtype (@is_partition α)) :=
 
 variables (α)
 
-/-- The order-preserving bijection between equivalence relations and partitions of sets. -/
+/-- The order-preserving bijection between equivalence relations on a type `α`, and
+  partitions of `α` into subsets. -/
 protected def partition.order_iso :
-  setoid α ≃o subtype (@is_partition α) :=
+  setoid α ≃o {C : set (set α) // is_partition C} :=
 { to_fun := λ r, ⟨r.classes, empty_not_mem_classes, classes_eqv_classes⟩,
-  inv_fun := λ x, mk_classes x.1 x.2.2,
+  inv_fun := λ C, mk_classes C.1 C.2.2,
   left_inv := mk_classes_classes,
-  right_inv := λ x, by rw [subtype.ext_iff_val, ←classes_mk_classes x.1 x.2],
-  map_rel_iff' := λ x y,
-    by { conv_rhs { rw [←mk_classes_classes x, ←mk_classes_classes y] }, refl } }
+  right_inv := λ C, by rw [subtype.ext_iff_val, ←classes_mk_classes C.1 C.2],
+  map_rel_iff' := λ r s,
+    by { conv_rhs { rw [←mk_classes_classes r, ←mk_classes_classes s] }, refl } }
 
 variables {α}