feat(Analysis/Convex/TotallyBounded): strengthen to an iff (leanprover-community#41226)

... and golf the existing proof using the fancy new `grw`.

From MeanFourier

Author: YaelDillies

Mathlib/Analysis/Convex/TotallyBounded.lean

@@ -30,26 +30,23 @@ public section
 
 open Set Pointwise
 
-variable (E : Type*) {s : Set E}
+variable {E : Type*} {s : Set E}
 variable [AddCommGroup E] [Module ℝ E]
-variable [UniformSpace E] [IsUniformAddGroup E] [lcs : LocallyConvexSpace ℝ E] [ContinuousSMul ℝ E]
+variable [UniformSpace E] [IsUniformAddGroup E] [LocallyConvexSpace ℝ E] [ContinuousSMul ℝ E]
 
-theorem totallyBounded_convexHull (hs : TotallyBounded s) :
+protected lemma TotallyBounded.convexHull (hs : TotallyBounded s) :
     TotallyBounded (convexHull ℝ s) := by
-  rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero]
+  rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at ⊢ hs
   intro U hU
   obtain ⟨W, hW₁, hW₂⟩ := exists_nhds_zero_half hU
-  obtain ⟨V, ⟨hV₁, hV₂, hV₃⟩⟩ := (locallyConvexSpace_iff_exists_convex_subset_zero ℝ E).mp lcs W hW₁
-  obtain ⟨t, ⟨htf, hts⟩⟩ := (totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp hs) _ hV₁
-  obtain ⟨t', ⟨htf', hts'⟩⟩ := (totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp
-    (IsCompact.totallyBounded (Finite.isCompact_convexHull ℝ htf)) _ hV₁)
+  obtain ⟨V, hV₁,hV₂, hV₃⟩ := (locallyConvexSpace_iff_exists_convex_subset_zero ℝ E).mp ‹_› W hW₁
+  obtain ⟨t, htf, hts⟩ := hs _ hV₁
+  obtain ⟨t', htf', hts'⟩ := totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp
+    (htf.isCompact_convexHull ℝ).totallyBounded _ hV₁
   use t', htf'
   simp only [iUnion_vadd_set, vadd_eq_add] at hts hts' ⊢
-  calc convexHull ℝ s
-    _ ⊆ convexHull ℝ (t + V) := convexHull_mono hts
-    _ ⊆ convexHull ℝ t + convexHull ℝ V := convexHull_add_subset
-    _ = convexHull ℝ t + V := by rw [hV₂.convexHull_eq]
-    _ ⊆ t' + V + V := add_subset_add_right hts'
-    _ = t' + (V + V) := by rw [add_assoc]
-    _ ⊆ t' + (W + W) := add_subset_add_left (add_subset_add hV₃ hV₃)
-    _ ⊆ t' + U := add_subset_add_left (add_subset_iff.mpr hW₂)
+  grw [hts, convexHull_add_subset, hV₂.convexHull_eq, hts', add_assoc, hV₃, add_subset_iff.mpr hW₂]
+
+@[simp] lemma totallyBounded_convexHull : TotallyBounded (convexHull ℝ s) ↔ TotallyBounded s where
+  mp := .subset <| subset_convexHull ..
+  mpr := .convexHull

Mathlib/Analysis/LocallyConvex/AbsConvex.lean

@@ -343,17 +343,15 @@ theorem convexHull_union_neg_eq_absConvexHull {s : Set E} :
       rw [← Convex.convexHull_eq (convex_convexHull ℝ (s ∪ -s))]
       exact convexHull_mono balancedHull_subset_convexHull_union_neg)
 
-variable (E 𝕜) {s : Set E}
+variable (𝕜) {s : Set E}
 variable [NontriviallyNormedField 𝕜] [PartialOrder 𝕜] [Module 𝕜 E] [SMulCommClass ℝ 𝕜 E]
 variable [UniformSpace E] [IsUniformAddGroup E] [lcs : LocallyConvexSpace ℝ E] [ContinuousSMul ℝ E]
 
--- TVS II.25 Prop3
-theorem totallyBounded_absConvexHull (hs : TotallyBounded s) :
-    TotallyBounded (absConvexHull ℝ s) := by
-  rw [← convexHull_union_neg_eq_absConvexHull]
-  apply totallyBounded_convexHull
-  rw [totallyBounded_union]
-  exact ⟨hs, totallyBounded_neg hs⟩
+@[simp]
+lemma totallyBounded_absConvexHull : TotallyBounded (absConvexHull ℝ s) ↔ TotallyBounded s := by
+  simp [← convexHull_union_neg_eq_absConvexHull]
+
+protected alias ⟨_, TotallyBounded.absConvexHull⟩ := totallyBounded_absConvexHull
 
 end
 
@@ -367,5 +365,4 @@ theorem isCompact_closedAbsConvexHull_of_totallyBounded {E : Type*} [AddCommGrou
     [QuasiCompleteSpace ℝ E] {s : Set E} (ht : TotallyBounded s) :
     IsCompact (closedAbsConvexHull ℝ s) := by
   rw [closedAbsConvexHull_eq_closure_absConvexHull]
-  exact isCompact_closure_of_totallyBounded_quasiComplete (𝕜 := ℝ)
-    (totallyBounded_absConvexHull E ht)
+  exact isCompact_closure_of_totallyBounded_quasiComplete (𝕜 := ℝ) ht.absConvexHull

Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean

@@ -137,9 +137,13 @@ theorem totallyBounded_iff_subset_finite_iUnion_nhds_one {s : Set α} :
     simp [← preimage_smul_inv, preimage]
 
 @[to_additive]
-theorem totallyBounded_inv {s : Set α} (hs : TotallyBounded s) : TotallyBounded (s⁻¹) := by
-  convert! TotallyBounded.image hs uniformContinuous_inv
-  aesop
+protected lemma TotallyBounded.inv {s : Set α} (hs : TotallyBounded s) : TotallyBounded s⁻¹ := by
+  simpa using hs.image uniformContinuous_inv
+
+@[to_additive (attr := simp)]
+lemma totallyBounded_inv {s : Set α} : TotallyBounded s⁻¹ ↔ TotallyBounded s where
+  mp hs := by simpa using hs.inv
+  mpr := .inv
 
 section UniformConvergence