chore(topology/algebra/semigroup): golf file (#14957)

src/topology/algebra/semigroup.lean

@@ -25,50 +25,44 @@ lemma exists_idempotent_of_compact_t2_of_continuous_mul_left {M} [nonempty M] [s
 begin
 /- We apply Zorn's lemma to the poset of nonempty closed subsemigroups of `M`. It will turn out that
 any minimal element is `{m}` for an idempotent `m : M`. -/
-  let S : set (set M) := { N : set M | is_closed N ∧ N.nonempty ∧ ∀ m m' ∈ N, m * m' ∈ N },
+  let S : set (set M) := {N | is_closed N ∧ N.nonempty ∧ ∀ m m' ∈ N, m * m' ∈ N},
   suffices : ∃ N ∈ S, ∀ N' ∈ S, N' ⊆ N → N' = N,
   { rcases this with ⟨N, ⟨N_closed, ⟨m, hm⟩, N_mul⟩, N_minimal⟩,
     use m,
 /- We now have an element `m : M` of a minimal subsemigroup `N`, and want to show `m + m = m`.
 We first show that every element of `N` is of the form `m' + m`.-/
     have scaling_eq_self : (* m) '' N = N,
     { apply N_minimal,
-      { refine ⟨(continuous_mul_left m).is_closed_map _ N_closed,
-          ⟨_, ⟨m, hm, rfl⟩⟩, _⟩,
+      { refine ⟨(continuous_mul_left m).is_closed_map _ N_closed, ⟨_, ⟨m, hm, rfl⟩⟩, _⟩,
         rintros _ ⟨m'', hm'', rfl⟩ _ ⟨m', hm', rfl⟩,
-        refine ⟨m'' * m * m', N_mul _ (N_mul _ hm'' _ hm) _ hm', mul_assoc _ _ _⟩, },
+        refine ⟨m'' * m * m', N_mul _ (N_mul _ hm'' _ hm) _ hm', mul_assoc _ _ _⟩ },
       { rintros _ ⟨m', hm', rfl⟩,
-        exact N_mul _ hm' _ hm, }, },
+        exact N_mul _ hm' _ hm } },
 /- In particular, this means that `m' * m = m` for some `m'`. We now use minimality again to show
-that this holds for _all_ `m' ∈ N`. -/
-    have absorbing_eq_self : N ∩ { m' | m' * m = m} = N,
+that this holds for all `m' ∈ N`. -/
+    have absorbing_eq_self : N ∩ {m' | m' * m = m} = N,
     { apply N_minimal,
       { refine ⟨N_closed.inter ((t1_space.t1 m).preimage (continuous_mul_left m)), _, _⟩,
-        { rw ←scaling_eq_self at hm, exact hm },
+        { rwa ←scaling_eq_self at hm },
         { rintros m'' ⟨mem'', eq'' : _ = m⟩ m' ⟨mem', eq' : _ = m⟩,
           refine ⟨N_mul _ mem'' _ mem', _⟩,
-          rw [set.mem_set_of_eq, mul_assoc, eq', eq''], }, },
-      apply set.inter_subset_left, },
+          rw [set.mem_set_of_eq, mul_assoc, eq', eq''] } },
+      apply set.inter_subset_left },
 /- Thus `m * m = m` as desired. -/
     rw ←absorbing_eq_self at hm,
-    exact hm.2, },
-  apply zorn_superset,
-  intros c hcs hc,
-  refine ⟨⋂₀ c, ⟨is_closed_sInter $ λ t ht, (hcs ht).1, _, _⟩, _⟩,
+    exact hm.2 },
+  refine zorn_superset _ (λ c hcs hc, _),
+  refine ⟨⋂₀ c, ⟨is_closed_sInter $ λ t ht, (hcs ht).1, _, λ m hm m' hm', _⟩,
+    λ s hs, set.sInter_subset_of_mem hs⟩,
   { obtain rfl | hcnemp := c.eq_empty_or_nonempty,
-    { rw set.sInter_empty, apply set.univ_nonempty, },
+    { rw set.sInter_empty, apply set.univ_nonempty },
     convert @is_compact.nonempty_Inter_of_directed_nonempty_compact_closed _ _ _
       (set.nonempty_coe_sort.mpr hcnemp) (coe : c → set M) _ _ _ _,
     { simp only [subtype.range_coe_subtype, set.set_of_mem_eq] } ,
     { refine directed_on.directed_coe (is_chain.directed_on hc.symm) },
-    { intro i, exact (hcs i.property).2.1, },
-    { intro i, exact (hcs i.property).1.is_compact, },
-    { intro i, exact (hcs i.property).1, }, },
-  { intros m hm m' hm',
-    rw set.mem_sInter,
-    intros t ht,
-    exact (hcs ht).2.2 m (set.mem_sInter.mp hm t ht) m' (set.mem_sInter.mp hm' t ht) },
-  { intros s hs, exact set.sInter_subset_of_mem hs, },
+    exacts [λ i, (hcs i.prop).2.1, λ i, (hcs i.prop).1.is_compact, λ i, (hcs i.prop).1] },
+  { rw set.mem_sInter,
+    exact λ t ht, (hcs ht).2.2 m (set.mem_sInter.mp hm t ht) m' (set.mem_sInter.mp hm' t ht) },
 end
 
 /-- A version of `exists_idempotent_of_compact_t2_of_continuous_mul_left` where the idempotent lies
@@ -81,7 +75,7 @@ lemma exists_idempotent_in_compact_subsemigroup {M} [semigroup M] [topological_s
   (s : set M) (snemp : s.nonempty) (s_compact : is_compact s) (s_add : ∀ x y ∈ s, x * y ∈ s) :
   ∃ m ∈ s, m * m = m :=
 begin
-  let M' := { m // m ∈ s },
+  let M' := {m // m ∈ s},
   letI : semigroup M' :=
     { mul       := λ p q, ⟨p.1 * q.1, s_add _ p.2 _ q.2⟩,
       mul_assoc := λ p q r, subtype.eq (mul_assoc _ _ _) },
@@ -90,5 +84,5 @@ begin
   have : ∀ p : M', continuous (* p) := λ p, continuous_subtype_mk _
     ((continuous_mul_left p.1).comp continuous_subtype_val),
   obtain ⟨⟨m, hm⟩, idem⟩ := exists_idempotent_of_compact_t2_of_continuous_mul_left this,
-  exact ⟨m, hm, subtype.ext_iff.mp idem⟩,
+  exact ⟨m, hm, subtype.ext_iff.mp idem⟩
 end