reduce diffs

astrainfinita · astrainfinita · commit 58e2ba8c29b9 · 2023-10-23T09:52:49.000+08:00
diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean
@@ -300,7 +300,9 @@ variable [AddCommGroup F] [AddCommGroup G]
 
 variable [Module 𝕜 E] [Module 𝕜₂ E₂] [Module 𝕜₃ E₃] [Module 𝕜 F] [Module 𝕜 G]
 
-instance : IsScalarTower ℝ≥0 ℝ≥0 ℝ := IsScalarTower.left _
+-- Porting note: even though this instance is found immediately by typeclass search,
+-- it seems to be needed below!?
+noncomputable instance smul_nnreal_real : SMul ℝ≥0 ℝ := inferInstance
 
 variable [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ]
 
diff --git a/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean b/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
@@ -76,8 +76,7 @@ variable (σ R)
 
 /-- While equal, the former has a convenient definitional reduction. -/
 theorem homogeneousSubmodule_eq_finsupp_supported [CommSemiring R] (n : ℕ) :
-    homogeneousSubmodule σ R n =
-      (Finsupp.supported _ R {d | ∑ i in d.support, d i = n} : Submodule R (MvPolynomial σ R)) := by
+    homogeneousSubmodule σ R n = Finsupp.supported _ R { d | ∑ i in d.support, d i = n } := by
   ext
   rw [Finsupp.mem_supported, Set.subset_def]
   simp only [Finsupp.mem_support_iff, Finset.mem_coe]
diff --git a/Mathlib/RingTheory/MvPolynomial/Symmetric.lean b/Mathlib/RingTheory/MvPolynomial/Symmetric.lean
@@ -303,7 +303,7 @@ theorem psum_one : psum σ R 1 = ∑ i, X i := by
 
 @[simp]
 theorem rename_psum (n : ℕ) (e : σ ≃ τ) : rename e (psum σ R n) = psum τ R n := by
-  simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (fun i ↦ (X i ^ n : MvPolynomial τ R))]
+  simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (X · ^ n)]
 
 theorem psum_isSymmetric (n : ℕ) : IsSymmetric (psum σ R n) := rename_psum _ _ n
 
diff --git a/Mathlib/Topology/MetricSpace/MetrizableUniformity.lean b/Mathlib/Topology/MetricSpace/MetrizableUniformity.lean
@@ -128,7 +128,7 @@ theorem le_two_mul_dist_ofPreNNDist (d : X → X → ℝ≥0) (dist_self : ∀ x
   set L := zipWith d (x::l) (l ++ [y])
   have hL_len : length L = length l + 1 := by simp
   cases' eq_or_ne (d x y) 0 with hd₀ hd₀
-  · simp only [hd₀, zero_le (α := ℝ≥0)]
+  · simp only [hd₀, zero_le]
   rsuffices ⟨z, z', hxz, hzz', hz'y⟩ : ∃ z z' : X, d x z ≤ L.sum ∧ d z z' ≤ L.sum ∧ d z' y ≤ L.sum
   · exact (hd x z z' y).trans (mul_le_mul_left' (max_le hxz (max_le hzz' hz'y)) _)
   set s : Set ℕ := { m : ℕ | 2 * (take m L).sum ≤ L.sum }
@@ -161,7 +161,7 @@ theorem le_two_mul_dist_ofPreNNDist (d : X → X → ℝ≥0) (dist_self : ∀ x
       convert hMs.1.out
       rw [zipWith_distrib_take, take, take_succ, get?_append hMl, get?_eq_get hMl, ← Option.coe_def,
         Option.to_list_some, take_append_of_le_length hMl.le]
-  · exact single_le_sum (fun x _ ↦ zero_le (α := ℝ≥0) x) _ (mem_iff_get.2 ⟨⟨M, hM_lt⟩, get_zipWith⟩)
+  · exact single_le_sum (fun x _ => zero_le x) _ (mem_iff_get.2 ⟨⟨M, hM_lt⟩, get_zipWith⟩)
   · rcases hMl.eq_or_lt with (rfl | hMl)
     · simp only [get_append_right' le_rfl, sub_self, get_singleton, dist_self, zero_le]
     rw [get_append _ hMl]
