diff --git a/Mathlib/Algebra/Order/CauSeq/Completion.lean b/Mathlib/Algebra/Order/CauSeq/Completion.lean
index e835ea0fc6a27b..43f63c26c1587a 100644
--- a/Mathlib/Algebra/Order/CauSeq/Completion.lean
+++ b/Mathlib/Algebra/Order/CauSeq/Completion.lean
@@ -236,7 +236,7 @@ theorem inv_mk {f} (hf) : (@mk α _ β _ abv _ f)⁻¹ = mk (inv f hf) :=
 #align cau_seq.completion.inv_mk CauSeq.Completion.inv_mk
 
 theorem cau_seq_zero_ne_one : ¬(0 : CauSeq _ abv) ≈ 1 := fun h =>
-  have : LimZero (1 - 0) := Setoid.symm h
+  have : LimZero (1 - 0 : CauSeq _ abv) := Setoid.symm h
   have : LimZero 1 := by simpa
   by apply one_ne_zero <| const_limZero.1 this
 #align cau_seq.completion.cau_seq_zero_ne_one CauSeq.Completion.cau_seq_zero_ne_one
diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
index 06304fe75c151b..e63fdf1c2ad261 100644
--- a/Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
+++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
@@ -160,7 +160,7 @@ variable (𝕜 E F)
     ‖fst 𝕜 E F‖ = 1 := by
   refine le_antisymm (norm_fst_le ..) ?_
   let ⟨e, he⟩ := exists_ne (0 : E)
-  have : ‖e‖ ≤ _ * max ‖e‖ ‖0‖ := (fst 𝕜 E F).le_opNorm (e, 0)
+  have : ‖e‖ ≤ _ * max ‖e‖ ‖(0 : F)‖ := (fst 𝕜 E F).le_opNorm (e, 0)
   rw [norm_zero, max_eq_left (norm_nonneg e)] at this
   rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr he), one_mul]
 
@@ -170,7 +170,7 @@ variable (𝕜 E F)
     ‖snd 𝕜 E F‖ = 1 := by
   refine le_antisymm (norm_snd_le ..) ?_
   let ⟨f, hf⟩ := exists_ne (0 : F)
-  have : ‖f‖ ≤ _ * max ‖0‖ ‖f‖ := (snd 𝕜 E F).le_opNorm (0, f)
+  have : ‖f‖ ≤ _ * max ‖(0 : E)‖ ‖f‖ := (snd 𝕜 E F).le_opNorm (0, f)
   rw [norm_zero, max_eq_right (norm_nonneg f)] at this
   rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr hf), one_mul]
 
diff --git a/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean b/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
index 35b5932ff26a30..60ffd6fc7e1e9e 100644
--- a/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
+++ b/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
@@ -96,7 +96,7 @@ theorem not_integrableOn_Ioi_rpow (s : ℝ) : ¬ IntegrableOn (fun x ↦ x ^ s)
   · have : IntegrableOn (fun x ↦ x ^ s) (Ioo (0 : ℝ) 1) := h.mono Ioo_subset_Ioi_self le_rfl
     rw [integrableOn_Ioo_rpow_iff zero_lt_one] at this
     exact hs.not_lt this
-  · have : IntegrableOn (fun x ↦ x ^ s) (Ioi 1) := h.mono (Ioi_subset_Ioi zero_le_one) le_rfl
+  · have : IntegrableOn (fun x ↦ x ^ s) (Ioi (1 : ℝ)) := h.mono (Ioi_subset_Ioi zero_le_one) le_rfl
     rw [integrableOn_Ioi_rpow_iff zero_lt_one] at this
     exact hs.not_lt this
 
diff --git a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean
index ab91ba6657b6bb..914f92776b9ffa 100644
--- a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean
+++ b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean
@@ -520,7 +520,7 @@ lemma tendsto_zero_sumCoeffsExp : Tendsto (fun (p : ℝ) => ∑ i, a i * (b i) ^
   linarith
 
 lemma tendsto_atTop_sumCoeffsExp : Tendsto (fun (p : ℝ) => ∑ i, a i * (b i) ^ p) atBot atTop := by
-  have h₁ : Tendsto (fun p => (a (max_bi b) : ℝ) * b (max_bi b) ^ p) atBot atTop :=
+  have h₁ : Tendsto (fun p : ℝ => (a (max_bi b) : ℝ) * b (max_bi b) ^ p) atBot atTop :=
     Tendsto.mul_atTop (R.a_pos (max_bi b)) (by simp)
       <| tendsto_rpow_atBot_of_base_lt_one _
       (by have := R.b_pos (max_bi b); linarith) (R.b_lt_one _)
diff --git a/Mathlib/GroupTheory/Coset.lean b/Mathlib/GroupTheory/Coset.lean
index 3e22b20e912cda..0f4b46c1664b10 100644
--- a/Mathlib/GroupTheory/Coset.lean
+++ b/Mathlib/GroupTheory/Coset.lean
@@ -148,7 +148,7 @@ variable [Monoid α] (s : Submonoid α)
 
 @[to_additive mem_own_leftAddCoset]
 theorem mem_own_leftCoset (a : α) : a ∈ a • (s : Set α) :=
-  suffices a * 1 ∈ a • ↑s by simpa
+  suffices a * 1 ∈ a • (s : Set α) by simpa
   mem_leftCoset a (one_mem s : 1 ∈ s)
 #align mem_own_left_coset mem_own_leftCoset
 #align mem_own_left_add_coset mem_own_leftAddCoset
diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
index 6a5351e8839ba5..b7885fae4ed406 100644
--- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
+++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
@@ -118,7 +118,7 @@ def invertibleEquivDetInvertible : Invertible A ≃ Invertible A.det where
 variable {A B}
 
 theorem mul_eq_one_comm : A * B = 1 ↔ B * A = 1 :=
-  suffices ∀ A B, A * B = 1 → B * A = 1 from ⟨this A B, this B A⟩
+  suffices ∀ A B : Matrix n n α, A * B = 1 → B * A = 1 from ⟨this A B, this B A⟩
   fun A B h => by
   letI : Invertible B.det := detInvertibleOfLeftInverse _ _ h
   letI : Invertible B := invertibleOfDetInvertible B
diff --git a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean
index 6a74cbf3e0ea69..39ef8d37ab32f6 100644
--- a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean
+++ b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean
@@ -492,7 +492,7 @@ lemma measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport
     · simpa using (u_mem n).2.le
   have I1 := I μ' (by infer_instance)
   simp_rw [M] at I1
-  have J1 : ∫ (x : G), indicator {1} (fun _ ↦ 1) (f x) ∂μ'
+  have J1 : ∫ (x : G), indicator {1} (fun _ ↦ (1 : ℝ)) (f x) ∂μ'
       = ∫ (x : G), indicator {1} (fun _ ↦ 1) (f x) ∂(haarScalarFactor μ' μ • μ) :=
     tendsto_nhds_unique I1 (I (haarScalarFactor μ' μ • μ) (by infer_instance))
   have J2 : ENNReal.toReal (μ' (f ⁻¹' {1}))
diff --git a/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean b/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean
index 9a94e2cc82300c..1e5a747035295a 100644
--- a/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean
+++ b/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean
@@ -88,7 +88,7 @@ theorem prime_of_nat_prime_of_mod_four_eq_three (p : ℕ) [hp : Fact p.Prime] (h
   irreducible_iff_prime.1 <|
     by_contradiction fun hpi =>
       let ⟨a, b, hab⟩ := sq_add_sq_of_nat_prime_of_not_irreducible p hpi
-      have : ∀ a b : ZMod 4, a ^ 2 + b ^ 2 ≠ ↑p := by
+      have : ∀ a b : ZMod 4, a ^ 2 + b ^ 2 ≠ (p : ZMod 4) := by
         erw [← ZMod.natCast_mod p 4, hp3]; decide
       this a b (hab ▸ by simp)
 #align gaussian_int.prime_of_nat_prime_of_mod_four_eq_three GaussianInt.prime_of_nat_prime_of_mod_four_eq_three
diff --git a/Mathlib/Order/PrimeIdeal.lean b/Mathlib/Order/PrimeIdeal.lean
index 00ca6fc656f295..137da1310f5c3e 100644
--- a/Mathlib/Order/PrimeIdeal.lean
+++ b/Mathlib/Order/PrimeIdeal.lean
@@ -158,7 +158,7 @@ instance (priority := 100) IsMaximal.isPrime [IsMaximal I] : IsPrime I := by
   let J := I ⊔ principal x
   have hJuniv : (J : Set P) = Set.univ :=
     IsMaximal.maximal_proper (lt_sup_principal_of_not_mem ‹_›)
-  have hyJ : y ∈ ↑J := Set.eq_univ_iff_forall.mp hJuniv y
+  have hyJ : y ∈ (J : Set P) := Set.eq_univ_iff_forall.mp hJuniv y
   rw [coe_sup_eq] at hyJ
   rcases hyJ with ⟨a, ha, b, hb, hy⟩
   rw [hy]
diff --git a/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean b/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean
index 21b12711a50b1f..86bc20cf4ce1f7 100644
--- a/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean
+++ b/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean
@@ -175,7 +175,7 @@ theorem dvd_pow_natDegree_of_eval₂_eq_zero {f : R →+* A} (hf : Function.Inje
           (Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem
       _ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl
   rw [injective_iff_map_eq_zero'] at hf
-  have : eval₂ _ _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h
+  have : eval₂ f _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h
   rwa [hz, Polynomial.eval₂_at_apply, hf] at this
 #align polynomial.dvd_pow_nat_degree_of_eval₂_eq_zero Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero
 
diff --git a/Mathlib/Topology/ContinuousFunction/Bounded.lean b/Mathlib/Topology/ContinuousFunction/Bounded.lean
index c37c0582b37d3c..39ec9997fa04d6 100644
--- a/Mathlib/Topology/ContinuousFunction/Bounded.lean
+++ b/Mathlib/Topology/ContinuousFunction/Bounded.lean
@@ -581,7 +581,7 @@ theorem arzela_ascoli₂ (s : Set β) (hs : IsCompact s) (A : Set (α →ᵇ β)
     IsCompact A := by
   /- This version is deduced from the previous one by restricting to the compact type in the target,
   using compactness there and then lifting everything to the original space. -/
-  have M : LipschitzWith 1 (↑) := LipschitzWith.subtype_val s
+  have M : LipschitzWith 1 Subtype.val := LipschitzWith.subtype_val s
   let F : (α →ᵇ s) → α →ᵇ β := comp (↑) M
   refine' IsCompact.of_isClosed_subset ((_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed
       fun f hf => _