chore(analysis/seminorm): golf (#18089)

A part of this PR is forward-ported as leanprover-community/mathlib4#1429

src/algebra/order/field/basic.lean

@@ -445,6 +445,10 @@ begin
   exact lt_max_iff.2 (or.inl $ lt_add_one _)
 end
 
+lemma exists_pos_lt_mul {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b < c * a :=
+let ⟨c, hc₀, hc⟩ := exists_pos_mul_lt h b
+in ⟨c⁻¹, inv_pos.2 hc₀, by rwa [← div_eq_inv_mul, lt_div_iff hc₀]⟩
+
 lemma monotone.div_const {β : Type*} [preorder β] {f : β → α} (hf : monotone f)
   {c : α} (hc : 0 ≤ c) : monotone (λ x, (f x) / c) :=
 begin

src/analysis/locally_convex/abs_convex.lean

@@ -144,29 +144,22 @@ variables [smul_comm_class ℝ 𝕜 E] [locally_convex_space ℝ E]
 lemma with_gauge_seminorm_family : with_seminorms (gauge_seminorm_family 𝕜 E) :=
 begin
   refine seminorm_family.with_seminorms_of_has_basis _ _,
-  refine filter.has_basis.to_has_basis (nhds_basis_abs_convex_open 𝕜 E) (λ s hs, _) (λ s hs, _),
+  refine (nhds_basis_abs_convex_open 𝕜 E).to_has_basis (λ s hs, _) (λ s hs, _),
   { refine ⟨s, ⟨_, rfl.subset⟩⟩,
-    rw seminorm_family.basis_sets_iff,
-    refine ⟨{⟨s, hs⟩}, 1, one_pos, _⟩,
-    simp only [finset.sup_singleton],
-    rw gauge_seminorm_family_ball,
-    simp only [subtype.coe_mk] },
+    convert (gauge_seminorm_family _ _).basis_sets_singleton_mem ⟨s, hs⟩ one_pos,
+    rw [gauge_seminorm_family_ball, subtype.coe_mk] },
   refine ⟨s, ⟨_, rfl.subset⟩⟩,
   rw seminorm_family.basis_sets_iff at hs,
-  rcases hs with ⟨t, r, hr, hs⟩,
-  rw seminorm.ball_finset_sup_eq_Inter _ _ _ hr at hs,
-  rw hs,
+  rcases hs with ⟨t, r, hr, rfl⟩,
+  rw [seminorm.ball_finset_sup_eq_Inter _ _ _ hr],
   -- We have to show that the intersection contains zero, is open, balanced, and convex
   refine ⟨mem_Inter₂.mpr (λ _ _, by simp [seminorm.mem_ball_zero, hr]),
-    is_open_bInter (to_finite _) (λ _ _, _),
+    is_open_bInter (to_finite _) (λ S _, _),
     balanced_Inter₂ (λ _ _, seminorm.balanced_ball_zero _ _),
     convex_Inter₂ (λ _ _, seminorm.convex_ball _ _ _)⟩,
   -- The only nontrivial part is to show that the ball is open
   have hr' : r = ‖(r : 𝕜)‖ * 1 := by simp [abs_of_pos hr],
-  have hr'' : (r : 𝕜) ≠ 0 := by simp [ne_of_gt hr],
-  rw hr',
-  rw ←seminorm.smul_ball_zero (norm_pos_iff.mpr hr''),
-  refine is_open.smul₀ _ hr'',
-  rw gauge_seminorm_family_ball,
-  exact abs_convex_open_sets.coe_is_open _,
+  have hr'' : (r : 𝕜) ≠ 0 := by simp [hr.ne'],
+  rw [hr', ← seminorm.smul_ball_zero hr'', gauge_seminorm_family_ball],
+  exact S.coe_is_open.smul₀ hr''
 end

src/analysis/locally_convex/bounded.lean

@@ -280,7 +280,7 @@ begin
     rcases h (metric.ball_mem_nhds 0 zero_lt_one) with ⟨ρ, hρ, hρball⟩,
     rcases normed_field.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩,
     specialize hρball a ha.le,
-    rw [← ball_norm_seminorm 𝕜 E, seminorm.smul_ball_zero (hρ.trans ha),
+    rw [← ball_norm_seminorm 𝕜 E, seminorm.smul_ball_zero (norm_pos_iff.1 $ hρ.trans ha),
         ball_norm_seminorm, mul_one] at hρball,
     exact ⟨‖a‖, hρball.trans metric.ball_subset_closed_ball⟩ },
   { exact λ ⟨C, hC⟩, (is_vonN_bounded_closed_ball 𝕜 E C).subset hC }

src/analysis/locally_convex/with_seminorms.lean

@@ -488,7 +488,7 @@ begin
     rcases h with ⟨r, hr, h⟩,
     cases normed_field.exists_lt_norm 𝕜 r with a ha,
     specialize h a (le_of_lt ha),
-    rw [seminorm.smul_ball_zero (lt_trans hr ha), mul_one] at h,
+    rw [seminorm.smul_ball_zero (norm_pos_iff.1 $ hr.trans ha), mul_one] at h,
     refine ⟨‖a‖, lt_trans hr ha, _⟩,
     intros x hx,
     specialize h hx,

src/analysis/seminorm.lean

@@ -780,51 +780,28 @@ section normed_field
 variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) {A B : set E}
   {a : 𝕜} {r : ℝ} {x : E}
 
-lemma smul_ball_zero {p : seminorm 𝕜 E} {k : 𝕜} {r : ℝ} (hk : 0 < ‖k‖) :
+lemma smul_ball_zero {p : seminorm 𝕜 E} {k : 𝕜} {r : ℝ} (hk : k ≠ 0) :
   k • p.ball 0 r = p.ball 0 (‖k‖ * r) :=
 begin
   ext,
-  rw [set.mem_smul_set, seminorm.mem_ball_zero],
-  split; intro h,
-  { rcases h with ⟨y, hy, h⟩,
-    rw [←h, map_smul_eq_mul],
-    rw seminorm.mem_ball_zero at hy,
-    exact (mul_lt_mul_left hk).mpr hy },
-  refine ⟨k⁻¹ • x, _, _⟩,
-  { rw [seminorm.mem_ball_zero, map_smul_eq_mul, norm_inv, ←(mul_lt_mul_left hk),
-      ←mul_assoc, ←(div_eq_mul_inv ‖k‖ ‖k‖), div_self (ne_of_gt hk), one_mul],
-    exact h},
-  rw [←smul_assoc, smul_eq_mul, ←div_eq_mul_inv, div_self (norm_pos_iff.mp hk), one_smul],
+  rw [mem_smul_set_iff_inv_smul_mem₀ hk, p.mem_ball_zero, p.mem_ball_zero, map_smul_eq_mul,
+    norm_inv, ← div_eq_inv_mul, div_lt_iff (norm_pos_iff.2 hk), mul_comm]
 end
 
 lemma ball_zero_absorbs_ball_zero (p : seminorm 𝕜 E) {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) :
   absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂) :=
 begin
-  by_cases hr₂ : r₂ ≤ 0,
-  { rw ball_eq_emptyset p hr₂, exact absorbs_empty },
-  rw [not_le] at hr₂,
-  rcases exists_between hr₁ with ⟨r, hr, hr'⟩,
-  refine ⟨r₂/r, div_pos hr₂ hr, _⟩,
-  simp_rw set.subset_def,
-  intros a ha x hx,
-  have ha' : 0 < ‖a‖ := lt_of_lt_of_le (div_pos hr₂ hr) ha,
-  rw [smul_ball_zero ha', p.mem_ball_zero],
+  rcases exists_pos_lt_mul hr₁ r₂ with ⟨r, hr₀, hr⟩,
+  refine ⟨r, hr₀, λ a ha x hx, _⟩,
+  rw [smul_ball_zero (norm_pos_iff.1 $ hr₀.trans_le ha), p.mem_ball_zero],
   rw p.mem_ball_zero at hx,
-  rw div_le_iff hr at ha,
-  exact hx.trans (lt_of_le_of_lt ha ((mul_lt_mul_left ha').mpr hr')),
+  exact hx.trans (hr.trans_le $ mul_le_mul_of_nonneg_right ha hr₁.le)
 end
 
 /-- Seminorm-balls at the origin are absorbent. -/
 protected lemma absorbent_ball_zero (hr : 0 < r) : absorbent 𝕜 (ball p (0 : E) r) :=
-begin
-  rw absorbent_iff_nonneg_lt,
-  rintro x,
-  have hxr : 0 ≤ p x / r := by positivity,
-  refine ⟨p x/r, hxr, λ a ha, _⟩,
-  have ha₀ : 0 < ‖a‖ := hxr.trans_lt ha,
-  refine ⟨a⁻¹ • x, _, smul_inv_smul₀ (norm_pos_iff.1 ha₀) x⟩,
-  rwa [mem_ball_zero, map_smul_eq_mul, norm_inv, inv_mul_lt_iff ha₀, ←div_lt_iff hr],
-end
+absorbent_iff_forall_absorbs_singleton.2 $ λ x, (p.ball_zero_absorbs_ball_zero hr).mono_right $
+  singleton_subset_iff.2 $ p.mem_ball_zero.2 $ lt_add_one _
 
 /-- Closed seminorm-balls at the origin are absorbent. -/
 protected lemma absorbent_closed_ball_zero (hr : 0 < r) : absorbent 𝕜 (closed_ball p (0 : E) r) :=
@@ -946,8 +923,7 @@ begin
   suffices : (p.restrict_scalars ℝ).ball 0 ε ∈ (𝓝 0 : filter E),
   { rwa seminorm.ball_zero_eq_preimage_ball at this },
   have := (set_smul_mem_nhds_zero_iff hε.ne.symm).mpr hp,
-  rwa [seminorm.smul_ball_zero (norm_pos_iff.mpr hε.ne.symm),
-      real.norm_of_nonneg hε.le, mul_one] at this
+  rwa [seminorm.smul_ball_zero hε.ne', real.norm_of_nonneg hε.le, mul_one] at this
 end
 
 protected lemma uniform_continuous_of_continuous_at_zero [uniform_space E] [uniform_add_group E]