diff --git a/Archive/Imo/Imo2024Q5.lean b/Archive/Imo/Imo2024Q5.lean
index 7b090f48cc987..5cbdf23de02f8 100644
--- a/Archive/Imo/Imo2024Q5.lean
+++ b/Archive/Imo/Imo2024Q5.lean
@@ -509,7 +509,7 @@ lemma Strategy.play_two (s : Strategy N) (m : MonsterData N) {k : ℕ} (hk : 2 <
   fin_cases i
   · rfl
   · have h : (1 : Fin 2) = Fin.last 1 := rfl
-    simp only [Fin.snoc_zero, Nat.reduceAdd, Fin.mk_one, Fin.isValue, Matrix.cons_val_one,
+    simp only [Fin.snoc_zero, Nat.reduceAdd, Fin.mk_one, Fin.isValue, id_eq, Matrix.cons_val_one,
       Matrix.head_cons]
     simp only [h, Fin.snoc_last]
     convert rfl
diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
index 0ac5af563ff8a..6a3125c87d0c9 100644
--- a/Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
+++ b/Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
@@ -243,9 +243,9 @@ theorem denom_cocycle (x y : GL(2, ℝ)⁺) (z : ℍ) :
     denom (x * y) z = denom x (smulAux y z) * denom y z := by
   change _ = (_ * (_ / _) + _) * _
   field_simp [denom_ne_zero]
-  simp only [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, denom, num, Subgroup.coe_mul,
-    GeneralLinearGroup.coe_mul, Fintype.univ_ofSubsingleton, Fin.mk_zero, Finset.sum_singleton,
-    Fin.succ_zero_eq_one, Complex.ofReal_add, Complex.ofReal_mul]
+  simp only [denom, Subgroup.coe_mul, Fin.isValue, Units.val_mul, mul_apply, Fin.sum_univ_succ,
+    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_zero_eq_one,
+    Complex.ofReal_add, Complex.ofReal_mul, num]
   ring
 
 theorem mul_smul' (x y : GL(2, ℝ)⁺) (z : ℍ) : smulAux (x * y) z = smulAux x (smulAux y z) := by
@@ -254,9 +254,9 @@ theorem mul_smul' (x y : GL(2, ℝ)⁺) (z : ℍ) : smulAux (x * y) z = smulAux
   change _ / _ = (_ * (_ / _) + _) / _
   rw [denom_cocycle]
   field_simp [denom_ne_zero]
-  simp only [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, num, denom, Subgroup.coe_mul,
-    GeneralLinearGroup.coe_mul, Fintype.univ_ofSubsingleton, Fin.mk_zero, Finset.sum_singleton,
-    Fin.succ_zero_eq_one, Complex.ofReal_add, Complex.ofReal_mul]
+  simp only [num, Subgroup.coe_mul, Fin.isValue, Units.val_mul, mul_apply, Fin.sum_univ_succ,
+    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_zero_eq_one,
+    Complex.ofReal_add, Complex.ofReal_mul, denom]
   ring
 
 /-- The action of `GLPos 2 ℝ` on the upper half-plane by fractional linear transformations. -/
diff --git a/Mathlib/Analysis/Convex/StoneSeparation.lean b/Mathlib/Analysis/Convex/StoneSeparation.lean
index 76a95705677f6..5a52d98fda2ea 100644
--- a/Mathlib/Analysis/Convex/StoneSeparation.lean
+++ b/Mathlib/Analysis/Convex/StoneSeparation.lean
@@ -67,8 +67,8 @@ theorem not_disjoint_segment_convexHull_triple {p q u v x y z : E} (hz : z ∈ s
       ((az * av * bu) • p + ((bz * au * bv) • q + (au * av) • (az • x + bz • y)))
     · module
     congr 3
-    simp only [w, z, smul_add, List.foldr, Matrix.cons_val_succ', Fin.mk_one,
-      Matrix.cons_val_one, Matrix.head_cons, add_zero]
+    simp only [smul_add, List.foldr, Fin.reduceFinMk, id_eq, Fin.isValue, Matrix.cons_val_two,
+      Nat.succ_eq_add_one, Nat.reduceAdd, Matrix.tail_cons, Matrix.head_cons, add_zero, w, z]
 
 /-- **Stone's Separation Theorem** -/
 theorem exists_convex_convex_compl_subset (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) (hst : Disjoint s t) :
diff --git a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean
index b07b1d09381f7..afdbc274d603b 100644
--- a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean
+++ b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean
@@ -354,14 +354,16 @@ theorem inner_mul_inner_add_areaForm_mul_areaForm' (a x : E) :
   apply (o.basisRightAngleRotation a ha).ext
   intro i
   fin_cases i
-  · simp only [Fin.mk_zero, coe_basisRightAngleRotation, Matrix.cons_val_zero, LinearMap.add_apply,
-      LinearMap.smul_apply, innerₛₗ_apply, real_inner_self_eq_norm_sq, smul_eq_mul,
-      areaForm_apply_self, mul_zero, add_zero, Real.rpow_two, real_inner_comm]
+  · simp only [Fin.zero_eta, Fin.isValue, id_eq, coe_basisRightAngleRotation, Nat.succ_eq_add_one,
+      Nat.reduceAdd, Matrix.cons_val_zero, LinearMap.add_apply, LinearMap.smul_apply, innerₛₗ_apply,
+      real_inner_self_eq_norm_sq, smul_eq_mul, areaForm_apply_self, mul_zero, add_zero,
+      real_inner_comm]
     ring
-  · simp only [Fin.mk_one, coe_basisRightAngleRotation, Matrix.cons_val_one, Matrix.head_cons,
-      LinearMap.add_apply, LinearMap.smul_apply, innerₛₗ_apply, inner_rightAngleRotation_right,
-      areaForm_apply_self, neg_zero, smul_eq_mul, mul_zero, areaForm_rightAngleRotation_right,
-      real_inner_self_eq_norm_sq, zero_add, Real.rpow_two, mul_neg]
+  · simp only [Fin.mk_one, Fin.isValue, id_eq, coe_basisRightAngleRotation, Nat.succ_eq_add_one,
+      Nat.reduceAdd, Matrix.cons_val_one, Matrix.head_cons, LinearMap.add_apply,
+      LinearMap.smul_apply, innerₛₗ_apply, inner_rightAngleRotation_right, areaForm_apply_self,
+      neg_zero, smul_eq_mul, mul_zero, areaForm_rightAngleRotation_right,
+      real_inner_self_eq_norm_sq, zero_add, mul_neg]
     rw [o.areaForm_swap]
     ring
 
@@ -381,15 +383,16 @@ theorem inner_mul_areaForm_sub' (a x : E) : ⟪a, x⟫ • ω a - ω a x • inn
   apply (o.basisRightAngleRotation a ha).ext
   intro i
   fin_cases i
-  · simp only [o.areaForm_swap a x, neg_smul, sub_neg_eq_add, Fin.mk_zero,
-      coe_basisRightAngleRotation, Matrix.cons_val_zero, LinearMap.add_apply, LinearMap.smul_apply,
-      areaForm_apply_self, smul_eq_mul, mul_zero, innerₛₗ_apply, real_inner_self_eq_norm_sq,
-      zero_add, Real.rpow_two]
+  · simp only [o.areaForm_swap a x, neg_smul, sub_neg_eq_add, Fin.zero_eta, Fin.isValue, id_eq,
+      coe_basisRightAngleRotation, Nat.succ_eq_add_one, Nat.reduceAdd, Matrix.cons_val_zero,
+      LinearMap.add_apply, LinearMap.smul_apply, areaForm_apply_self, smul_eq_mul, mul_zero,
+      innerₛₗ_apply, real_inner_self_eq_norm_sq, zero_add]
     ring
-  · simp only [Fin.mk_one, coe_basisRightAngleRotation, Matrix.cons_val_one, Matrix.head_cons,
-      LinearMap.sub_apply, LinearMap.smul_apply, areaForm_rightAngleRotation_right,
-      real_inner_self_eq_norm_sq, smul_eq_mul, innerₛₗ_apply, inner_rightAngleRotation_right,
-      areaForm_apply_self, neg_zero, mul_zero, sub_zero, Real.rpow_two, real_inner_comm]
+  · simp only [Fin.mk_one, Fin.isValue, id_eq, coe_basisRightAngleRotation, Nat.succ_eq_add_one,
+      Nat.reduceAdd, Matrix.cons_val_one, Matrix.head_cons, LinearMap.sub_apply,
+      LinearMap.smul_apply, areaForm_rightAngleRotation_right, real_inner_self_eq_norm_sq,
+      smul_eq_mul, innerₛₗ_apply, inner_rightAngleRotation_right, areaForm_apply_self, neg_zero,
+      mul_zero, sub_zero, real_inner_comm]
     ring
 
 /-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y`. -/
diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean
index 03674193faaec..4b86b7218cdfb 100644
--- a/Mathlib/Data/List/Defs.lean
+++ b/Mathlib/Data/List/Defs.lean
@@ -488,9 +488,17 @@ theorem length_mapAccumr₂ :
 
 end MapAccumr
 
+/- #adaptation_note: this attribute should be removed after Mathlib moves to v4.15.0-rc1. -/
+set_option allowUnsafeReducibility true in
+attribute [semireducible] Fin.foldr.loop
+
 /-- All elements of `Fin n`, from `0` to `n-1`. The corresponding finset is `Finset.univ`. -/
-def finRange (n : ℕ) : List (Fin n) :=
-  (range n).pmap Fin.mk fun _ => List.mem_range.1
+-- Note that we use `ofFn (fun x => x)` instead of `ofFn id` to avoid leaving `id` in the terms
+-- for e.g. `Fintype (Fin n)`.
+def finRange (n : Nat) : List (Fin n) := ofFn (fun x => x)
+
+-- Verify that `finRange` is semireducible.
+example : finRange 3 = [0, 1, 2] := rfl
 
 section Deprecated
 
diff --git a/Mathlib/Data/List/FinRange.lean b/Mathlib/Data/List/FinRange.lean
index 62d8122999597..bf592cfe78937 100644
--- a/Mathlib/Data/List/FinRange.lean
+++ b/Mathlib/Data/List/FinRange.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kenny Lau, Kim Morrison, Alex Keizer
 -/
 import Mathlib.Data.List.OfFn
-import Mathlib.Data.List.Range
 import Batteries.Data.List.Perm
+import Mathlib.Data.List.Nodup
 
 /-!
 # Lists of elements of `Fin n`
@@ -21,10 +21,66 @@ namespace List
 
 variable {α : Type u}
 
+
+theorem finRange_eq_pmap_range (n : ℕ) : finRange n = (range n).pmap Fin.mk (by simp) := by
+  apply List.ext_getElem <;> simp [finRange]
+
+@[simp]
+theorem finRange_zero : finRange 0 = [] := rfl
+
+@[simp]
+theorem mem_finRange {n : ℕ} (a : Fin n) : a ∈ finRange n := by
+  rw [finRange_eq_pmap_range]
+  exact mem_pmap.2
+    ⟨a.1, mem_range.2 a.2, by
+      cases a
+      rfl⟩
+
+theorem nodup_finRange (n : ℕ) : (finRange n).Nodup := by
+  rw [finRange_eq_pmap_range]
+  exact (Pairwise.pmap (nodup_range n) _) fun _ _ _ _ => @Fin.ne_of_val_ne _ ⟨_, _⟩ ⟨_, _⟩
+
+@[simp]
+theorem length_finRange (n : ℕ) : (finRange n).length = n := by
+  simp [finRange]
+
+@[simp]
+theorem finRange_eq_nil {n : ℕ} : finRange n = [] ↔ n = 0 := by
+  rw [← length_eq_zero, length_finRange]
+
+theorem pairwise_lt_finRange (n : ℕ) : Pairwise (· < ·) (finRange n) := by
+  rw [finRange_eq_pmap_range]
+  exact (List.pairwise_lt_range n).pmap (by simp) (by simp)
+
+theorem pairwise_le_finRange (n : ℕ) : Pairwise (· ≤ ·) (finRange n) := by
+  rw [finRange_eq_pmap_range]
+  exact (List.pairwise_le_range n).pmap (by simp) (by simp)
+
+@[simp]
+theorem getElem_finRange {n : ℕ} {i : ℕ} (h) :
+    (finRange n)[i] = ⟨i, length_finRange n ▸ h⟩ := by
+  simp [finRange, getElem_range, getElem_pmap]
+
+-- Porting note (https://github.com/leanprover-community/mathlib4/issues/10756): new theorem
+theorem get_finRange {n : ℕ} {i : ℕ} (h) :
+    (finRange n).get ⟨i, h⟩ = ⟨i, length_finRange n ▸ h⟩ := by
+  simp
+
+@[deprecated (since := "2024-08-19")] alias nthLe_finRange := get_finRange
+
+@[simp]
+theorem finRange_map_get (l : List α) : (finRange l.length).map l.get = l :=
+  List.ext_get (by simp) (by simp)
+
+@[simp] theorem indexOf_finRange {k : ℕ} (i : Fin k) : (finRange k).indexOf i = i := by
+  have : (finRange k).indexOf i < (finRange k).length := indexOf_lt_length.mpr (by simp)
+  have h₁ : (finRange k).get ⟨(finRange k).indexOf i, this⟩ = i := indexOf_get this
+  have h₂ : (finRange k).get ⟨i, by simp⟩ = i := get_finRange _
+  simpa using (Nodup.get_inj_iff (nodup_finRange k)).mp (Eq.trans h₁ h₂.symm)
+
 @[simp]
 theorem map_coe_finRange (n : ℕ) : ((finRange n) : List (Fin n)).map (Fin.val) = List.range n := by
-  simp_rw [finRange, map_pmap, pmap_eq_map]
-  exact List.map_id _
+  apply List.ext_getElem <;> simp
 
 theorem finRange_succ_eq_map (n : ℕ) : finRange n.succ = 0 :: (finRange n).map Fin.succ := by
   apply map_injective_iff.mpr Fin.val_injective
@@ -45,7 +101,7 @@ theorem ofFn_eq_pmap {n} {f : Fin n → α} :
   exact ext_getElem (by simp) fun i hi1 hi2 => by simp [List.getElem_ofFn f i hi1]
 
 theorem ofFn_id (n) : ofFn id = finRange n :=
-  ofFn_eq_pmap
+  rfl
 
 theorem ofFn_eq_map {n} {f : Fin n → α} : ofFn f = (finRange n).map f := by
   rw [← ofFn_id, map_ofFn, Function.comp_id]
diff --git a/Mathlib/Data/List/Range.lean b/Mathlib/Data/List/Range.lean
index 7cefc522da8e2..e133f0b507d6d 100644
--- a/Mathlib/Data/List/Range.lean
+++ b/Mathlib/Data/List/Range.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kenny Lau, Kim Morrison
 -/
 import Mathlib.Data.List.Chain
-import Mathlib.Data.List.Nodup
 
 /-!
 # Ranges of naturals as lists
@@ -42,58 +41,10 @@ theorem chain_range_succ (r : ℕ → ℕ → Prop) (n a : ℕ) :
   rw [range_succ_eq_map, chain_cons, and_congr_right_iff, ← chain'_range_succ, range_succ_eq_map]
   exact fun _ => Iff.rfl
 
-@[simp]
-theorem finRange_zero : finRange 0 = [] :=
-  rfl
-
-@[simp]
-theorem mem_finRange {n : ℕ} (a : Fin n) : a ∈ finRange n :=
-  mem_pmap.2
-    ⟨a.1, mem_range.2 a.2, by
-      cases a
-      rfl⟩
-
-theorem nodup_finRange (n : ℕ) : (finRange n).Nodup :=
-  (Pairwise.pmap (nodup_range n) _) fun _ _ _ _ => @Fin.ne_of_val_ne _ ⟨_, _⟩ ⟨_, _⟩
-
-@[simp]
-theorem length_finRange (n : ℕ) : (finRange n).length = n := by
-  rw [finRange, length_pmap, length_range]
-
-@[simp]
-theorem finRange_eq_nil {n : ℕ} : finRange n = [] ↔ n = 0 := by
-  rw [← length_eq_zero, length_finRange]
-
-theorem pairwise_lt_finRange (n : ℕ) : Pairwise (· < ·) (finRange n) :=
-  (List.pairwise_lt_range n).pmap (by simp) (by simp)
-
-theorem pairwise_le_finRange (n : ℕ) : Pairwise (· ≤ ·) (finRange n) :=
-  (List.pairwise_le_range n).pmap (by simp) (by simp)
-
-@[simp]
-theorem getElem_finRange {n : ℕ} {i : ℕ} (h) :
-    (finRange n)[i] = ⟨i, length_finRange n ▸ h⟩ := by
-  simp [finRange, getElem_range, getElem_pmap]
-
--- Porting note (https://github.com/leanprover-community/mathlib4/issues/10756): new theorem
-theorem get_finRange {n : ℕ} {i : ℕ} (h) :
-    (finRange n).get ⟨i, h⟩ = ⟨i, length_finRange n ▸ h⟩ := by
-  simp
-
 @[deprecated (since := "2024-08-19")] alias nthLe_range' := get_range'
 @[deprecated (since := "2024-08-19")] alias nthLe_range'_1 := getElem_range'_1
 @[deprecated (since := "2024-08-19")] alias nthLe_range := get_range
-@[deprecated (since := "2024-08-19")] alias nthLe_finRange := get_finRange
-
-@[simp]
-theorem finRange_map_get (l : List α) : (finRange l.length).map l.get = l :=
-  List.ext_get (by simp) (by simp)
 
-@[simp] theorem indexOf_finRange {k : ℕ} (i : Fin k) : (finRange k).indexOf i = i := by
-  have : (finRange k).indexOf i < (finRange k).length := indexOf_lt_length.mpr (by simp)
-  have h₁ : (finRange k).get ⟨(finRange k).indexOf i, this⟩ = i := indexOf_get this
-  have h₂ : (finRange k).get ⟨i, by simp⟩ = i := get_finRange _
-  simpa using (Nodup.get_inj_iff (nodup_finRange k)).mp (Eq.trans h₁ h₂.symm)
 
 section Ranges
 
diff --git a/Mathlib/Data/List/Sublists.lean b/Mathlib/Data/List/Sublists.lean
index cc89adca8c9e8..9a2c8391406a8 100644
--- a/Mathlib/Data/List/Sublists.lean
+++ b/Mathlib/Data/List/Sublists.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.Nat.Choose.Basic
-import Mathlib.Data.List.Range
+import Mathlib.Data.List.FinRange
 import Mathlib.Data.List.Perm.Basic
+import Mathlib.Data.List.Lex
 
 /-! # sublists
 
diff --git a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean
index 9476da73472ed..308268392107c 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean
@@ -618,7 +618,7 @@ theorem affineIndependent_of_ne {p₁ p₂ : P} (h : p₁ ≠ p₂) : AffineInde
     ext
     fin_cases i
     · simp at hi
-    · simp only [Fin.val_one]
+    · simp
   haveI : Unique { x // x ≠ (0 : Fin 2) } := ⟨⟨i₁⟩, he'⟩
   apply linearIndependent_unique
   rw [he' default]
diff --git a/Mathlib/NumberTheory/Modular.lean b/Mathlib/NumberTheory/Modular.lean
index 7eb5dbb5ffec4..59b083317b35b 100644
--- a/Mathlib/NumberTheory/Modular.lean
+++ b/Mathlib/NumberTheory/Modular.lean
@@ -207,17 +207,19 @@ theorem tendsto_lcRow0 {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0) (cd 1)) :
   ext ⟨g, rfl⟩ i j : 3
   fin_cases i <;> [fin_cases j; skip]
   -- the following are proved by `simp`, but it is replaced by `simp only` to avoid timeouts.
-  · simp only [mB, mulVec, dotProduct, Fin.sum_univ_two, coe_matrix_coe,
-      Int.coe_castRingHom, lcRow0_apply, Function.comp_apply, cons_val_zero, lcRow0Extend_apply,
+  · simp only [Fin.isValue, Int.cast_one, map_apply_coe, RingHom.mapMatrix_apply,
+      Int.coe_castRingHom, lcRow0_apply, map_apply, Fin.zero_eta, id_eq, Function.comp_apply,
+      of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one, lcRow0Extend_apply,
       LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLinear,
-      val_planeConformalMatrix, neg_neg, mulVecLin_apply, cons_val_one, head_cons, of_apply,
-      Fin.mk_zero, Fin.mk_one]
+      val_planeConformalMatrix, neg_neg, mulVecLin_apply, mulVec, dotProduct, Fin.sum_univ_two,
+      cons_val_one, head_cons, mB, f₁]
   · convert congr_arg (fun n : ℤ => (-n : ℝ)) g.det_coe.symm using 1
-    simp only [f₁, mulVec, dotProduct, Fin.sum_univ_two, Matrix.det_fin_two, Function.comp_apply,
-      Subtype.coe_mk, lcRow0Extend_apply, cons_val_zero,
+    simp only [Fin.zero_eta, id_eq, Function.comp_apply, lcRow0Extend_apply, cons_val_zero,
       LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLinear,
-      val_planeConformalMatrix, mulVecLin_apply, cons_val_one, head_cons, map_apply, neg_mul,
-      Int.cast_sub, Int.cast_mul, neg_sub, of_apply, Fin.mk_zero, Fin.mk_one]
+      mulVecLin_apply, mulVec, dotProduct, det_fin_two, f₁]
+    simp only [Fin.isValue, Fin.mk_one, val_planeConformalMatrix, neg_neg, of_apply, cons_val',
+      empty_val', cons_val_fin_one, cons_val_one, head_fin_const, map_apply, Fin.sum_univ_two,
+      cons_val_zero, neg_mul, head_cons, Int.cast_sub, Int.cast_mul, neg_sub]
     ring
   · rfl
 
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
index 84f4e2aa14e91..3b10a1368dea7 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
@@ -585,17 +585,17 @@ theorem stdBasis_repr_eq_matrixToStdBasis_mul (x : (K →+* ℂ) → ℂ)
   | inr c =>
     rcases c with ⟨w, j⟩
     fin_cases j
-    · simp_rw [Fin.mk_zero, stdBasis_apply_ofIsComplex_fst, fromBlocks_apply₂₁,
-        fromBlocks_apply₂₂, Matrix.zero_apply, submatrix_apply,
-        blockDiagonal_apply, Prod.swap_prod_mk, ite_mul, zero_mul, sum_const_zero, zero_add,
-        sum_add_distrib, sum_ite_eq, mem_univ, ite_true, of_apply, cons_val', cons_val_zero,
-        cons_val_one, head_cons, ← hx (embedding w), re_eq_add_conj]
+    · simp only [Fin.zero_eta, Fin.isValue, id_eq, stdBasis_apply_ofIsComplex_fst, re_eq_add_conj,
+        mul_neg, fromBlocks_apply₂₁, zero_apply, zero_mul, sum_const_zero, fromBlocks_apply₂₂,
+        submatrix_apply, Prod.swap_prod_mk, blockDiagonal_apply, of_apply, cons_val', cons_val_zero,
+        empty_val', cons_val_fin_one, ite_mul, cons_val_one, head_cons, sum_add_distrib, sum_ite_eq,
+        mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]
       field_simp
-    · simp_rw [Fin.mk_one, stdBasis_apply_ofIsComplex_snd, fromBlocks_apply₂₁,
-        fromBlocks_apply₂₂, Matrix.zero_apply, submatrix_apply, blockDiagonal_apply,
-        Prod.swap_prod_mk, ite_mul, zero_mul, sum_const_zero, zero_add, sum_add_distrib, sum_ite_eq,
-        mem_univ, ite_true, of_apply, cons_val', cons_val_zero, cons_val_one, head_cons,
-        ← hx (embedding w), im_eq_sub_conj]
+    · simp only [Fin.mk_one, Fin.isValue, id_eq, stdBasis_apply_ofIsComplex_snd, im_eq_sub_conj,
+        mul_neg, fromBlocks_apply₂₁, zero_apply, zero_mul, sum_const_zero, fromBlocks_apply₂₂,
+        submatrix_apply, Prod.swap_prod_mk, blockDiagonal_apply, of_apply, cons_val', cons_val_zero,
+        empty_val', cons_val_fin_one, cons_val_one, head_fin_const, ite_mul, neg_mul, head_cons,
+        sum_add_distrib, sum_ite_eq, mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]
       ring_nf; field_simp
 
 end stdBasis
diff --git a/Mathlib/Order/RelSeries.lean b/Mathlib/Order/RelSeries.lean
index b2c41395b294b..e385b759958c2 100644
--- a/Mathlib/Order/RelSeries.lean
+++ b/Mathlib/Order/RelSeries.lean
@@ -112,9 +112,9 @@ corresponds to each other. -/
 protected def Equiv : RelSeries r ≃ {x : List α | x ≠ [] ∧ x.Chain' r} where
   toFun x := ⟨_, x.toList_ne_nil, x.toList_chain'⟩
   invFun x := fromListChain' _ x.2.1 x.2.2
-  left_inv x := ext (by simp [toList]) <| by ext; apply List.get_ofFn
+  left_inv x := ext (by simp [toList]) <| by ext; dsimp; apply List.get_ofFn
   right_inv x := by
-    refine Subtype.ext (List.ext_get ?_ fun n hn1 _ => List.get_ofFn _ _)
+    refine Subtype.ext (List.ext_get ?_ fun n hn1 _ => by dsimp; apply List.get_ofFn)
     have := Nat.succ_pred_eq_of_pos <| List.length_pos.mpr x.2.1
     simp_all [toList]
 
diff --git a/Mathlib/RingTheory/Complex.lean b/Mathlib/RingTheory/Complex.lean
index 68be8e6b337a3..1f3b98e14ae26 100644
--- a/Mathlib/RingTheory/Complex.lean
+++ b/Mathlib/RingTheory/Complex.lean
@@ -18,11 +18,11 @@ theorem Algebra.leftMulMatrix_complex (z : ℂ) :
   rw [Algebra.leftMulMatrix_eq_repr_mul, Complex.coe_basisOneI_repr, Complex.coe_basisOneI, mul_re,
     mul_im, Matrix.of_apply]
   fin_cases j
-  · simp only [Fin.mk_zero, Matrix.cons_val_zero, one_re, mul_one, one_im, mul_zero, sub_zero,
-      zero_add]
+  · simp only [Fin.zero_eta, id_eq, Matrix.cons_val_zero, one_re, mul_one, one_im, mul_zero,
+      sub_zero, zero_add, Matrix.cons_val_fin_one]
     fin_cases i <;> rfl
-  · simp only [Fin.mk_one, Matrix.cons_val_one, Matrix.head_cons, I_re, mul_zero, I_im, mul_one,
-      zero_sub, add_zero]
+  · simp only [Fin.mk_one, id_eq, Matrix.cons_val_one, Matrix.head_cons, I_re, mul_zero, I_im,
+      mul_one, zero_sub, add_zero, Matrix.cons_val_fin_one]
     fin_cases i <;> rfl
 
 theorem Algebra.trace_complex_apply (z : ℂ) : Algebra.trace ℝ ℂ z = 2 * z.re := by
diff --git a/Mathlib/SetTheory/Cardinal/Subfield.lean b/Mathlib/SetTheory/Cardinal/Subfield.lean
index 604447735f1cc..37f45168df1dd 100644
--- a/Mathlib/SetTheory/Cardinal/Subfield.lean
+++ b/Mathlib/SetTheory/Cardinal/Subfield.lean
@@ -76,7 +76,7 @@ lemma cardinalMk_closure_le_max : #(closure s) ≤ max #s ℵ₀ :=
         exact (add_lt_aleph0 this h).le
       · rw [max_eq_left h, add_eq_right h (this.le.trans h), max_eq_left h]
     rintro (n|_)
-    · fin_cases n <;> infer_instance
+    · fin_cases n <;> (dsimp only [id_eq]; infer_instance)
     infer_instance
 
 @[deprecated (since := "2024-11-10")] alias cardinal_mk_closure_le_max := cardinalMk_closure_le_max