chore(analysis/locally_convex/balanced_core_hull): Golf (#14987)

Golf and improve lemmas based on the naming convention:
* `balanced_mem` → `balanced_iff_smul_mem`
* `zero_singleton_balanced` → `balanced_zero`
* `balanced_core_emptyset` → `balanced_core_empty`
* `balanced_core_mem_iff` → `mem_balanced_core_iff`
* `balanced_hull_mem_iff` → `mem_balanced_hull_iff`
* `balanced_core_is_closed` → `is_closed.balanced_core`

src/analysis/locally_convex/balanced_core_hull.lean

@@ -50,9 +50,7 @@ section semi_normed_ring
 variables [semi_normed_ring 𝕜]
 
 section has_scalar
-variables [has_scalar 𝕜 E]
-
-variables (𝕜)
+variables (𝕜) [has_scalar 𝕜 E] {s t : set E} {x : E}
 
 /-- The largest balanced subset of `s`.-/
 def balanced_core (s : set E) := ⋃₀ {t : set E | balanced 𝕜 t ∧ t ⊆ s}
@@ -65,195 +63,129 @@ def balanced_hull (s : set E) := ⋃ (r : 𝕜) (hr : ∥r∥ ≤ 1), r • s
 
 variables {𝕜}
 
-lemma balanced_core_subset (s : set E) : balanced_core 𝕜 s ⊆ s :=
-begin
-  refine sUnion_subset (λ t ht, _),
-  simp only [mem_set_of_eq] at ht,
-  exact ht.2,
-end
+lemma balanced_core_subset (s : set E) : balanced_core 𝕜 s ⊆ s := sUnion_subset $ λ t ht, ht.2
 
-lemma balanced_core_emptyset : balanced_core 𝕜 (∅ : set E) = ∅ :=
-set.eq_empty_of_subset_empty (balanced_core_subset _)
+lemma balanced_core_empty : balanced_core 𝕜 (∅ : set E) = ∅ :=
+eq_empty_of_subset_empty (balanced_core_subset _)
 
-lemma balanced_core_mem_iff {s : set E} {x : E} : x ∈ balanced_core 𝕜 s ↔
-  ∃ t : set E, balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t :=
+lemma mem_balanced_core_iff : x ∈ balanced_core 𝕜 s ↔ ∃ t, balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t :=
 by simp_rw [balanced_core, mem_sUnion, mem_set_of_eq, exists_prop, and_assoc]
 
 lemma smul_balanced_core_subset (s : set E) {a : 𝕜} (ha : ∥a∥ ≤ 1) :
   a • balanced_core 𝕜 s ⊆ balanced_core 𝕜 s :=
 begin
-  rw subset_def,
-  intros x hx,
-  rw mem_smul_set at hx,
-  rcases hx with ⟨y, hy, hx⟩,
-  rw balanced_core_mem_iff at hy,
+  rintro x ⟨y, hy, rfl⟩,
+  rw mem_balanced_core_iff at hy,
   rcases hy with ⟨t, ht1, ht2, hy⟩,
-  rw ←hx,
-  refine ⟨t, _, ht1 a ha (smul_mem_smul_set hy)⟩,
-  rw mem_set_of_eq,
-  exact ⟨ht1, ht2⟩,
+  exact ⟨t, ⟨ht1, ht2⟩, ht1 a ha (smul_mem_smul_set hy)⟩,
 end
 
 lemma balanced_core_balanced (s : set E) : balanced 𝕜 (balanced_core 𝕜 s) :=
 λ _, smul_balanced_core_subset s
 
 /-- The balanced core of `t` is maximal in the sense that it contains any balanced subset
 `s` of `t`.-/
-lemma balanced.subset_core_of_subset {s t : set E} (hs : balanced 𝕜 s) (h : s ⊆ t):
-  s ⊆ balanced_core 𝕜 t :=
-begin
-  refine subset_sUnion_of_mem _,
-  rw [mem_set_of_eq],
-  exact ⟨hs, h⟩,
-end
+lemma balanced.subset_core_of_subset (hs : balanced 𝕜 s) (h : s ⊆ t) : s ⊆ balanced_core 𝕜 t :=
+subset_sUnion_of_mem ⟨hs, h⟩
 
-lemma balanced_core_aux_mem_iff (s : set E) (x : E) : x ∈ balanced_core_aux 𝕜 s ↔
-  ∀ (r : 𝕜) (hr : 1 ≤ ∥r∥), x ∈ r • s :=
-by rw [balanced_core_aux, set.mem_Inter₂]
+lemma mem_balanced_core_aux_iff : x ∈ balanced_core_aux 𝕜 s ↔ ∀ r : 𝕜, 1 ≤ ∥r∥ → x ∈ r • s :=
+mem_Inter₂
 
-lemma balanced_hull_mem_iff (s : set E) (x : E) : x ∈ balanced_hull 𝕜 s ↔
-  ∃ (r : 𝕜) (hr : ∥r∥ ≤ 1), x ∈ r • s :=
-by rw [balanced_hull, set.mem_Union₂]
+lemma mem_balanced_hull_iff : x ∈ balanced_hull 𝕜 s ↔ ∃ (r : 𝕜) (hr : ∥r∥ ≤ 1), x ∈ r • s :=
+mem_Union₂
 
-/-- The balanced core of `s` is minimal in the sense that it is contained in any balanced superset
+/-- The balanced hull of `s` is minimal in the sense that it is contained in any balanced superset
 `t` of `s`. -/
-lemma balanced.hull_subset_of_subset {s t : set E} (ht : balanced 𝕜 t) (h : s ⊆ t) :
-  balanced_hull 𝕜 s ⊆ t :=
-begin
-  intros x hx,
-  rcases (balanced_hull_mem_iff _ _).mp hx with ⟨r, hr, hx⟩,
-  rcases mem_smul_set.mp hx with ⟨y, hy, hx⟩,
-  rw ←hx,
-  exact balanced_mem ht (h hy) hr,
-end
+lemma balanced.hull_subset_of_subset (ht : balanced 𝕜 t) (h : s ⊆ t) : balanced_hull 𝕜 s ⊆ t :=
+λ x hx, by { obtain ⟨r, hr, y, hy, rfl⟩ := mem_balanced_hull_iff.1 hx, exact ht.smul_mem hr (h hy) }
 
 end has_scalar
 
-section add_comm_monoid
+section module
+variables [add_comm_group E] [module 𝕜 E] {s : set E}
 
-variables [add_comm_monoid E] [module 𝕜 E]
+lemma balanced_core_zero_mem (hs : (0 : E) ∈ s) : (0 : E) ∈ balanced_core 𝕜 s :=
+mem_balanced_core_iff.2 ⟨0, balanced_zero, zero_subset.2 hs, zero_mem_zero⟩
 
-lemma balanced_core_nonempty_iff {s : set E} : (balanced_core 𝕜 s).nonempty ↔ (0 : E) ∈ s :=
-begin
-  split; intro h,
-  { cases h with x hx,
-    have h' : balanced 𝕜 (balanced_core 𝕜 s) := balanced_core_balanced s,
-    have h'' := h' 0 (has_le.le.trans norm_zero.le zero_le_one),
-    refine mem_of_subset_of_mem (subset.trans h'' (balanced_core_subset s)) _,
-    exact mem_smul_set.mpr ⟨x, hx, zero_smul _ _⟩ },
-  refine nonempty_of_mem (mem_of_subset_of_mem _ (mem_singleton 0)),
-  exact balanced.subset_core_of_subset zero_singleton_balanced (singleton_subset_iff.mpr h),
-end
-
-lemma balanced_core_zero_mem {s : set E} (hs: (0 : E) ∈ s) : (0 : E) ∈ balanced_core 𝕜 s :=
-balanced_core_mem_iff.mpr
-  ⟨{0}, zero_singleton_balanced, singleton_subset_iff.mpr hs, mem_singleton 0⟩
+lemma balanced_core_nonempty_iff : (balanced_core 𝕜 s).nonempty ↔ (0 : E) ∈ s :=
+⟨λ h, zero_subset.1 $ (zero_smul_set h).superset.trans $ (balanced_core_balanced s (0 : 𝕜) $
+  norm_zero.trans_le zero_le_one).trans $ balanced_core_subset _,
+    λ h, ⟨0, balanced_core_zero_mem h⟩⟩
 
 variables (𝕜)
 
 lemma subset_balanced_hull [norm_one_class 𝕜] {s : set E} : s ⊆ balanced_hull 𝕜 s :=
-λ _ hx, (balanced_hull_mem_iff _ _).mpr ⟨1, norm_one.le, mem_smul_set.mp ⟨_, hx, one_smul _ _⟩⟩
+λ _ hx, mem_balanced_hull_iff.2 ⟨1, norm_one.le, _, hx, one_smul _ _⟩
 
 variables {𝕜}
 
 lemma balanced_hull.balanced (s : set E) : balanced 𝕜 (balanced_hull 𝕜 s) :=
 begin
   intros a ha,
   simp_rw [balanced_hull, smul_set_Union₂, subset_def, mem_Union₂],
-  intros x hx,
-  rcases hx with ⟨r, hr, hx⟩,
-  use [a • r],
-  split,
-  { rw smul_eq_mul,
-    refine has_le.le.trans (semi_normed_ring.norm_mul _ _) _,
-    refine mul_le_one ha (norm_nonneg r) hr },
-  rw smul_assoc,
-  exact hx,
+  rintro x ⟨r, hr, hx⟩,
+  rw ←smul_assoc at hx,
+  exact ⟨a • r, (semi_normed_ring.norm_mul _ _).trans (mul_le_one ha (norm_nonneg r) hr), hx⟩,
 end
 
-end add_comm_monoid
-
+end module
 end semi_normed_ring
 
 section normed_field
 
-variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E]
+variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {s t : set E}
 
 @[simp] lemma balanced_core_aux_empty : balanced_core_aux 𝕜 (∅ : set E) = ∅ :=
 begin
-  rw [balanced_core_aux, set.Inter₂_eq_empty_iff],
-  intros _,
-  simp only [smul_set_empty, mem_empty_eq, not_false_iff, exists_prop, and_true],
-  exact ⟨1, norm_one.ge⟩,
+  simp_rw [balanced_core_aux, Inter₂_eq_empty_iff, smul_set_empty],
+  exact λ _, ⟨1, norm_one.ge, not_mem_empty _⟩,
 end
 
 lemma balanced_core_aux_subset (s : set E) : balanced_core_aux 𝕜 s ⊆ s :=
-begin
-  rw subset_def,
-  intros x hx,
-  rw balanced_core_aux_mem_iff at hx,
-  have h := hx 1 norm_one.ge,
-  rw one_smul at h,
-  exact h,
-end
+λ x hx, by simpa only [one_smul] using mem_balanced_core_aux_iff.1 hx 1 norm_one.ge
 
-lemma balanced_core_aux_balanced {s : set E} (h0 : (0 : E) ∈ balanced_core_aux 𝕜 s):
+lemma balanced_core_aux_balanced (h0 : (0 : E) ∈ balanced_core_aux 𝕜 s):
   balanced 𝕜 (balanced_core_aux 𝕜 s) :=
 begin
-  intros a ha x hx,
-  rcases mem_smul_set.mp hx with ⟨y, hy, hx⟩,
-  by_cases (a = 0),
-  { simp[h] at hx,
-    rw ←hx,
-    exact h0 },
-  rw [←hx, balanced_core_aux_mem_iff],
-  rw balanced_core_aux_mem_iff at hy,
+  rintro a ha x ⟨y, hy, rfl⟩,
+  obtain rfl | h := eq_or_ne a 0,
+  { rwa zero_smul },
+  rw mem_balanced_core_aux_iff at ⊢ hy,
   intros r hr,
-  have h'' : 1 ≤ ∥a⁻¹ • r∥ :=
-  begin
-    rw smul_eq_mul,
-    simp only [norm_mul, norm_inv],
-    exact one_le_mul_of_one_le_of_one_le (one_le_inv (norm_pos_iff.mpr h) ha) hr,
-  end,
+  have h'' : 1 ≤ ∥a⁻¹ • r∥,
+  { rw [norm_smul, norm_inv],
+    exact one_le_mul_of_one_le_of_one_le (one_le_inv (norm_pos_iff.mpr h) ha) hr },
   have h' := hy (a⁻¹ • r) h'',
-  rw smul_assoc at h',
-  exact (mem_inv_smul_set_iff₀ h _ _).mp h',
+  rwa [smul_assoc, mem_inv_smul_set_iff₀ h] at h',
 end
 
-lemma balanced_core_aux_maximal {s t : set E} (h : t ⊆ s) (ht : balanced 𝕜 t) :
-  t ⊆ balanced_core_aux 𝕜 s :=
+lemma balanced_core_aux_maximal (h : t ⊆ s) (ht : balanced 𝕜 t) : t ⊆ balanced_core_aux 𝕜 s :=
 begin
-  intros x hx,
-  rw balanced_core_aux_mem_iff,
-  intros r hr,
-  rw mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.mp (lt_of_lt_of_le zero_lt_one hr)),
-  refine h (balanced_mem ht hx _),
+  refine λ x hx, mem_balanced_core_aux_iff.2 (λ r hr, _),
+  rw mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.mp $ zero_lt_one.trans_le hr),
+  refine h (ht.smul_mem _ hx),
   rw norm_inv,
   exact inv_le_one hr,
 end
 
-lemma balanced_core_subset_balanced_core_aux {s : set E} :
-  balanced_core 𝕜 s ⊆ balanced_core_aux 𝕜 s :=
+lemma balanced_core_subset_balanced_core_aux : balanced_core 𝕜 s ⊆ balanced_core_aux 𝕜 s :=
 balanced_core_aux_maximal (balanced_core_subset s) (balanced_core_balanced s)
 
-lemma balanced_core_eq_Inter {s : set E} (hs : (0 : E) ∈ s) :
+lemma balanced_core_eq_Inter (hs : (0 : E) ∈ s) :
   balanced_core 𝕜 s = ⋂ (r : 𝕜) (hr : 1 ≤ ∥r∥), r • s :=
 begin
-  rw ←balanced_core_aux,
-  refine subset_antisymm balanced_core_subset_balanced_core_aux _,
-  refine balanced.subset_core_of_subset (balanced_core_aux_balanced _) (balanced_core_aux_subset s),
-  refine mem_of_subset_of_mem balanced_core_subset_balanced_core_aux (balanced_core_zero_mem hs),
+  refine balanced_core_subset_balanced_core_aux.antisymm  _,
+  refine (balanced_core_aux_balanced _).subset_core_of_subset (balanced_core_aux_subset s),
+  exact balanced_core_subset_balanced_core_aux (balanced_core_zero_mem hs),
 end
 
-lemma subset_balanced_core {U V : set E} (hV' : (0 : E) ∈ V)
-  (hUV : ∀ (a : 𝕜) (ha : ∥a∥ ≤ 1), a • U ⊆ V) :
-  U ⊆ balanced_core 𝕜 V :=
+lemma subset_balanced_core (ht : (0 : E) ∈ t) (hst : ∀ (a : 𝕜) (ha : ∥a∥ ≤ 1), a • s ⊆ t) :
+  s ⊆ balanced_core 𝕜 t :=
 begin
-  rw balanced_core_eq_Inter hV',
-  refine set.subset_Inter₂ (λ a ha, _),
-  rw [←one_smul 𝕜 U, ←mul_inv_cancel (norm_pos_iff.mp (lt_of_lt_of_le zero_lt_one ha)),
-    ←smul_eq_mul, smul_assoc],
-  refine set.smul_set_mono (hUV a⁻¹ _),
+  rw balanced_core_eq_Inter ht,
+  refine subset_Inter₂ (λ a ha, _),
+  rw ←smul_inv_smul₀ (norm_pos_iff.mp $ zero_lt_one.trans_le ha) s,
+  refine smul_set_mono (hst _ _),
   rw [norm_inv],
   exact inv_le_one ha,
 end
@@ -267,9 +199,9 @@ end balanced_hull
 section topology
 
 variables [nondiscrete_normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E]
-  [has_continuous_smul 𝕜 E]
+  [has_continuous_smul 𝕜 E] {U : set E}
 
-lemma balanced_core_is_closed {U : set E} (hU : is_closed U) : is_closed (balanced_core 𝕜 U) :=
+protected lemma is_closed.balanced_core (hU : is_closed U) : is_closed (balanced_core 𝕜 U) :=
 begin
   by_cases h : (0 : E) ∈ U,
   { rw balanced_core_eq_Inter h,
@@ -283,8 +215,7 @@ begin
   exact balanced_core_nonempty_iff.mp (set.ne_empty_iff_nonempty.mp h),
 end
 
-lemma balanced_core_mem_nhds_zero {U : set E} (hU : U ∈ 𝓝 (0 : E)) :
-  balanced_core 𝕜 U ∈ 𝓝 (0 : E) :=
+lemma balanced_core_mem_nhds_zero (hU : U ∈ 𝓝 (0 : E)) : balanced_core 𝕜 U ∈ 𝓝 (0 : E) :=
 begin
   -- Getting neighborhoods of the origin for `0 : 𝕜` and `0 : E`
   have h : filter.tendsto (λ (x : 𝕜 × E), x.fst • x.snd) (𝓝 (0,0)) (𝓝 ((0 : 𝕜) • (0 : E))) :=
@@ -321,7 +252,7 @@ lemma nhds_basis_closed_balanced [regular_space E] : (𝓝 (0 : E)).has_basis
 begin
   refine (closed_nhds_basis 0).to_has_basis (λ s hs, _) (λ s hs, ⟨s, ⟨hs.1, hs.2.1⟩, rfl.subset⟩),
   refine ⟨balanced_core 𝕜 s, ⟨balanced_core_mem_nhds_zero hs.1, _⟩, balanced_core_subset s⟩,
-  refine ⟨balanced_core_is_closed hs.2, balanced_core_balanced s⟩
+  exact ⟨hs.2.balanced_core, balanced_core_balanced s⟩
 end
 
 end topology

src/analysis/locally_convex/basic.lean

@@ -132,9 +132,10 @@ def balanced (A : set E) := ∀ a : 𝕜, ∥a∥ ≤ 1 → a • A ⊆ A
 
 variables {𝕜}
 
-lemma balanced_mem {s : set E} (hs : balanced 𝕜 s) {x : E} (hx : x ∈ s) {a : 𝕜} (ha : ∥a∥ ≤ 1) :
-  a • x ∈ s :=
-mem_of_subset_of_mem (hs a ha) (smul_mem_smul_set hx)
+lemma balanced_iff_smul_mem : balanced 𝕜 s ↔ ∀ ⦃a : 𝕜⦄, ∥a∥ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s :=
+forall₂_congr $ λ a ha, smul_set_subset_iff
+
+alias balanced_iff_smul_mem ↔ balanced.smul_mem _
 
 lemma balanced_univ : balanced 𝕜 (univ : set E) := λ a ha, subset_univ _
 
@@ -172,8 +173,7 @@ begin
   exact add_mem_add (hA₁ _ ha ⟨_, hx, rfl⟩) (hA₂ _ ha ⟨_, hy, rfl⟩),
 end
 
-lemma zero_singleton_balanced : balanced 𝕜 ({0} : set E) :=
-λ a ha, by simp only [smul_set_singleton, smul_zero]
+lemma balanced_zero : balanced 𝕜 (0 : set E) := λ a ha, (smul_zero _).subset
 
 end add_comm_monoid
 end semi_normed_ring

src/topology/algebra/module/finite_dimension.lean

@@ -132,7 +132,7 @@ begin
         exact not_mem_compl_iff.mpr (mem_singleton ξ₀) ((balanced_core_subset _) this) },
       -- For that, we use that `𝓑` is balanced : since `∥ξ₀∥ < ε < ∥ξ∥`, we have `∥ξ₀ / ξ∥ ≤ 1`,
       -- hence `ξ₀ = (ξ₀ / ξ) • ξ ∈ 𝓑` because `ξ ∈ 𝓑`.
-      refine balanced_mem (balanced_core_balanced _) hξ _,
+      refine (balanced_core_balanced _).smul_mem _ hξ,
       rw [norm_mul, norm_inv, mul_inv_le_iff (norm_pos_iff.mpr hξ0), mul_one],
       exact (hξ₀ε.trans h).le } },
   { -- Finally, to show `𝓣₀ ≤ 𝓣`, we simply argue that `id = (λ x, x • 1)` is continuous from