fix: simps config for Units (#6514)

Mathlib/Algebra/Algebra/Spectrum.lean

@@ -87,6 +87,8 @@ noncomputable def IsUnit.subInvSMul {r : Rˣ} {s : R} {a : A} (h : IsUnit <| r 
   val_inv := by rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_val_inv]
   inv_val := by rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.val_inv_mul]
 #align is_unit.sub_inv_smul IsUnit.subInvSMul
+#align is_unit.coe_sub_inv_smul IsUnit.val_subInvSMul
+#align is_unit.coe_inv_sub_inv_smul IsUnit.val_inv_subInvSMul
 
 end Defs
 
@@ -158,8 +160,8 @@ theorem units_smul_resolvent {r : Rˣ} {s : R} {a : A} :
   · simp only [resolvent]
     have h' : IsUnit (r • algebraMap R A (r⁻¹ • s) - a) := by
       simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using not_mem_iff.mp h
-    rw [← h'.subInvSMul_val, ← (not_mem_iff.mp h).unit_spec, Ring.inverse_unit, Ring.inverse_unit,
-      ←h'.subInvSMul.inv_eq_val_inv, h'.subInvSMul_inv]
+    rw [← h'.val_subInvSMul, ← (not_mem_iff.mp h).unit_spec, Ring.inverse_unit, Ring.inverse_unit,
+      h'.val_inv_subInvSMul]
     simp only [Algebra.algebraMap_eq_smul_one, smul_assoc, smul_inv_smul]
 #align spectrum.units_smul_resolvent spectrum.units_smul_resolvent
 

Mathlib/Algebra/Group/Units.lean

@@ -112,13 +112,21 @@ instance instInv : Inv αˣ :=
   ⟨fun u => ⟨u.2, u.1, u.4, u.3⟩⟩
 attribute [instance] AddUnits.instNeg
 
-/- porting note: the result of these definitions is syntactically equal to `Units.val` and
-`Units.inv` because of the way coercions work in Lean 4, so there is no need for these custom
-`simp` projections. -/
+/- porting note: the result of these definitions is syntactically equal to `Units.val` because of
+the way coercions work in Lean 4, so there is no need for these custom `simp` projections. -/
 #noalign units.simps.coe
 #noalign add_units.simps.coe
-#noalign units.simps.coe_inv
-#noalign add_units.simps.coe_neg
+
+/-- See Note [custom simps projection] -/
+@[to_additive "See Note [custom simps projection]"]
+def Simps.val_inv (u : αˣ) : α := ↑(u⁻¹)
+#align units.simps.coe_inv Units.Simps.val_inv
+#align add_units.simps.coe_neg AddUnits.Simps.val_neg
+
+initialize_simps_projections Units (as_prefix val, val_inv → null, inv → val_inv, as_prefix val_inv)
+
+initialize_simps_projections AddUnits
+  (as_prefix val, val_neg → null, neg → val_neg, as_prefix val_neg)
 
 -- Porting note: removed `simp` tag because of the tautology
 @[to_additive]
@@ -164,6 +172,10 @@ def copy (u : αˣ) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑u⁻¹)
   { val, inv, inv_val := hv.symm ▸ hi.symm ▸ u.inv_val, val_inv := hv.symm ▸ hi.symm ▸ u.val_inv }
 #align units.copy Units.copy
 #align add_units.copy AddUnits.copy
+#align units.coe_copy Units.val_copy
+#align add_units.coe_copy AddUnits.val_copy
+#align units.coe_inv_copy Units.val_inv_copy
+#align add_units.coe_neg_copy AddUnits.val_neg_copy
 
 @[to_additive]
 theorem copy_eq (u : αˣ) (val hv inv hi) : u.copy val hv inv hi = u :=
@@ -241,12 +253,9 @@ theorem inv_mk (x y : α) (h₁ h₂) : (mk x y h₁ h₂)⁻¹ = mk y x h₂ h
 #noalign units.val_eq_coe
 #noalign add_units.val_eq_coe
 
-@[to_additive]
+@[to_additive (attr := simp)]
 theorem inv_eq_val_inv : a.inv = ((a⁻¹ : αˣ) : α) :=
   rfl
--- Porting note: the lower priority is needed to appease the `simpNF` linter
--- Note that `to_additive` doesn't copy `simp` priorities, so we use this as a workaround
-attribute [simp 900] Units.inv_eq_val_inv AddUnits.neg_eq_val_neg
 #align units.inv_eq_coe_inv Units.inv_eq_val_inv
 #align add_units.neg_eq_coe_neg AddUnits.neg_eq_val_neg
 

Mathlib/Algebra/Hom/Units.lean

@@ -272,7 +272,7 @@ variable [DivisionMonoid α] {a b c : α}
 /-- The element of the group of units, corresponding to an element of a monoid which is a unit. As
 opposed to `IsUnit.unit`, the inverse is computable and comes from the inversion on `α`. This is
 useful to transfer properties of inversion in `Units α` to `α`. See also `toUnits`. -/
-@[to_additive (attr := simps)
+@[to_additive (attr := simps val)
   "The element of the additive group of additive units, corresponding to an element of
   an additive monoid which is an additive unit. As opposed to `IsAddUnit.addUnit`, the negation is
   computable and comes from the negation on `α`. This is useful to transfer properties of negation
@@ -281,6 +281,13 @@ def unit' (h : IsUnit a) : αˣ :=
   ⟨a, a⁻¹, h.mul_inv_cancel, h.inv_mul_cancel⟩
 #align is_unit.unit' IsUnit.unit'
 #align is_add_unit.add_unit' IsAddUnit.addUnit'
+#align is_unit.coe_unit' IsUnit.val_unit'
+#align is_add_unit.coe_add_unit' IsAddUnit.val_addUnit'
+
+-- Porting note: TODO: `simps val_inv` fails
+@[to_additive] theorem val_inv_unit' (h : IsUnit a) : ↑(h.unit'⁻¹) = a⁻¹ := rfl
+#align is_unit.coe_inv_unit' IsUnit.val_inv_unit'
+#align is_add_unit.coe_neg_add_unit' IsAddUnit.val_neg_addUnit'
 
 @[to_additive (attr := simp)]
 protected theorem mul_inv_cancel_left (h : IsUnit a) : ∀ b, a * (a⁻¹ * b) = b :=

Mathlib/Algebra/Invertible.lean

@@ -188,14 +188,14 @@ theorem Invertible.congr [Ring α] (a b : α) [Invertible a] [Invertible b] (h :
 
 /-- An `Invertible` element is a unit. -/
 @[simps]
-def unitOfInvertible [Monoid α] (a : α) [Invertible a] :
-    αˣ where
+def unitOfInvertible [Monoid α] (a : α) [Invertible a] : αˣ where
   val := a
   inv := ⅟ a
   val_inv := by simp
   inv_val := by simp
 #align unit_of_invertible unitOfInvertible
-#align coe_unit_of_invertible unitOfInvertible_val
+#align coe_unit_of_invertible val_unitOfInvertible
+#align coe_inv_unit_of_invertible val_inv_unitOfInvertible
 
 theorem isUnit_of_invertible [Monoid α] (a : α) [Invertible a] : IsUnit a :=
   ⟨unitOfInvertible a, rfl⟩
@@ -377,8 +377,7 @@ variable [Monoid α]
 
 /-- This is the `Invertible` version of `Units.isUnit_units_mul` -/
 @[reducible]
-def invertibleOfInvertibleMul (a b : α) [Invertible a] [Invertible (a * b)] : Invertible b
-    where
+def invertibleOfInvertibleMul (a b : α) [Invertible a] [Invertible (a * b)] : Invertible b where
   invOf := ⅟ (a * b) * a
   invOf_mul_self := by rw [mul_assoc, invOf_mul_self]
   mul_invOf_self := by
@@ -388,8 +387,7 @@ def invertibleOfInvertibleMul (a b : α) [Invertible a] [Invertible (a * b)] : I
 
 /-- This is the `Invertible` version of `Units.isUnit_mul_units` -/
 @[reducible]
-def invertibleOfMulInvertible (a b : α) [Invertible (a * b)] [Invertible b] : Invertible a
-    where
+def invertibleOfMulInvertible (a b : α) [Invertible (a * b)] [Invertible b] : Invertible a where
   invOf := b * ⅟ (a * b)
   invOf_mul_self := by
     rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
@@ -398,24 +396,26 @@ def invertibleOfMulInvertible (a b : α) [Invertible (a * b)] [Invertible b] : I
 #align invertible_of_mul_invertible invertibleOfMulInvertible
 
 /-- `invertibleOfInvertibleMul` and `invertibleMul` as an equivalence. -/
-@[simps]
-def Invertible.mulLeft {a : α} (_ : Invertible a) (b : α) : Invertible b ≃ Invertible (a * b)
-    where
+@[simps apply symm_apply]
+def Invertible.mulLeft {a : α} (_ : Invertible a) (b : α) : Invertible b ≃ Invertible (a * b) where
   toFun _ := invertibleMul a b
   invFun _ := invertibleOfInvertibleMul a _
   left_inv _ := Subsingleton.elim _ _
   right_inv _ := Subsingleton.elim _ _
 #align invertible.mul_left Invertible.mulLeft
+#align invertible.mul_left_apply Invertible.mulLeft_apply
+#align invertible.mul_left_symm_apply Invertible.mulLeft_symm_apply
 
 /-- `invertibleOfMulInvertible` and `invertibleMul` as an equivalence. -/
-@[simps]
-def Invertible.mulRight (a : α) {b : α} (_ : Invertible b) : Invertible a ≃ Invertible (a * b)
-    where
+@[simps apply symm_apply]
+def Invertible.mulRight (a : α) {b : α} (_ : Invertible b) : Invertible a ≃ Invertible (a * b) where
   toFun _ := invertibleMul a b
   invFun _ := invertibleOfMulInvertible _ b
   left_inv _ := Subsingleton.elim _ _
   right_inv _ := Subsingleton.elim _ _
 #align invertible.mul_right Invertible.mulRight
+#align invertible.mul_right_apply Invertible.mulRight_apply
+#align invertible.mul_right_symm_apply Invertible.mulRight_symm_apply
 
 end Monoid
 

Mathlib/Algebra/Lie/Classical.lean

@@ -291,7 +291,7 @@ def typeDEquivSo' [Fintype l] [Invertible (2 : R)] : typeD l R ≃ₗ⁅R⁆ so'
   apply (skewAdjointMatricesLieSubalgebraEquiv (JD l R) (PD l R) (by infer_instance)).trans
   apply LieEquiv.ofEq
   ext A
-  rw [jd_transform, ← unitOfInvertible_val (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe,
+  rw [jd_transform, ← val_unitOfInvertible (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe,
     mem_skewAdjointMatricesLieSubalgebra_unit_smul]
   rfl
 #align lie_algebra.orthogonal.type_D_equiv_so' LieAlgebra.Orthogonal.typeDEquivSo'
@@ -380,7 +380,7 @@ def typeBEquivSo' [Invertible (2 : R)] : typeB l R ≃ₗ⁅R⁆ so' (Sum Unit l
         (Matrix.reindexAlgEquiv _ (Equiv.sumAssoc PUnit l l)) (Matrix.transpose_reindex _ _)).trans
   apply LieEquiv.ofEq
   ext A
-  rw [jb_transform, ← unitOfInvertible_val (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe,
+  rw [jb_transform, ← val_unitOfInvertible (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe,
     LieSubalgebra.mem_coe, mem_skewAdjointMatricesLieSubalgebra_unit_smul]
   simp [indefiniteDiagonal_assoc, S]
 #align lie_algebra.orthogonal.type_B_equiv_so' LieAlgebra.Orthogonal.typeBEquivSo'

Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

@@ -1144,7 +1144,7 @@ It is of $j$-invariant $0$ (see `EllipticCurve.ofJ0_j`). -/
 def ofJ0 [Invertible (3 : R)] : EllipticCurve R :=
   have := invertibleNeg (3 ^ 3 : R)
   ⟨WeierstrassCurve.ofJ0 R, unitOfInvertible (-3 ^ 3 : R),
-    by rw [unitOfInvertible_val, WeierstrassCurve.ofJ0_Δ R]; norm_num1⟩
+    by rw [val_unitOfInvertible, WeierstrassCurve.ofJ0_Δ R]; norm_num1⟩
 
 lemma ofJ0_j [Invertible (3 : R)] : (ofJ0 R).j = 0 := by
   simp only [j, ofJ0, WeierstrassCurve.ofJ0_c₄]
@@ -1155,10 +1155,10 @@ It is of $j$-invariant $1728$ (see `EllipticCurve.ofJ1728_j`). -/
 def ofJ1728 [Invertible (2 : R)] : EllipticCurve R :=
   have := invertibleNeg (2 ^ 6 : R)
   ⟨WeierstrassCurve.ofJ1728 R, unitOfInvertible (-2 ^ 6 : R),
-    by rw [unitOfInvertible_val, WeierstrassCurve.ofJ1728_Δ R]; norm_num1⟩
+    by rw [val_unitOfInvertible, WeierstrassCurve.ofJ1728_Δ R]; norm_num1⟩
 
 lemma ofJ1728_j [Invertible (2 : R)] : (ofJ1728 R).j = 1728 := by
-  field_simp [j, ofJ1728, @unitOfInvertible_val _ _ _ <| invertibleNeg _,
+  field_simp [j, ofJ1728, @val_unitOfInvertible _ _ _ <| invertibleNeg _,
     WeierstrassCurve.ofJ1728_c₄]
   norm_num1
 
@@ -1173,7 +1173,7 @@ def ofJ' (j : R) [Invertible j] [Invertible (j - 1728)] : EllipticCurve R :=
     (WeierstrassCurve.ofJ_Δ j).symm⟩
 
 lemma ofJ'_j (j : R) [Invertible j] [Invertible (j - 1728)] : (ofJ' j).j = j := by
-  field_simp [EllipticCurve.j, ofJ', @unitOfInvertible_val _ _ _ <| invertibleMul _ _,
+  field_simp [EllipticCurve.j, ofJ', @val_unitOfInvertible _ _ _ <| invertibleMul _ _,
     WeierstrassCurve.ofJ_c₄]
   ring1
 

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -180,7 +180,7 @@ theorem denom_ne_zero (g : GL(2, ℝ)⁺) (z : ℍ) : denom g z ≠ 0 := by
   intro H
   have DET := (mem_glpos _).1 g.prop
   have hz := z.prop
-  simp only [GeneralLinearGroup.det_apply_val] at DET
+  simp only [GeneralLinearGroup.val_det_apply] at DET
   have H1 : (↑ₘg 1 0 : ℝ) = 0 ∨ z.im = 0 := by simpa [num, denom] using congr_arg Complex.im H
   cases' H1 with H1
   · simp only [H1, Complex.ofReal_zero, denom, zero_mul, zero_add,
@@ -219,7 +219,7 @@ def smulAux (g : GL(2, ℝ)⁺) (z : ℍ) : ℍ :=
     rw [smulAux'_im]
     convert mul_pos ((mem_glpos _).1 g.prop)
         (div_pos z.im_pos (Complex.normSq_pos.mpr (denom_ne_zero g z))) using 1
-    simp only [GeneralLinearGroup.det_apply_val]
+    simp only [GeneralLinearGroup.val_det_apply]
     ring
 #align upper_half_plane.smul_aux UpperHalfPlane.smulAux
 
@@ -404,7 +404,7 @@ theorem c_mul_im_sq_le_normSq_denom (z : ℍ) (g : SL(2, ℝ)) :
 nonrec theorem SpecialLinearGroup.im_smul_eq_div_normSq :
     (g • z).im = z.im / Complex.normSq (denom g z) := by
   convert im_smul_eq_div_normSq g z
-  simp only [GeneralLinearGroup.det_apply_val, coe_GLPos_coe_GL_coe_matrix,
+  simp only [GeneralLinearGroup.val_det_apply, coe_GLPos_coe_GL_coe_matrix,
     Int.coe_castRingHom, (g : SL(2, ℝ)).prop, one_mul, coe']
 #align upper_half_plane.special_linear_group.im_smul_eq_div_norm_sq UpperHalfPlane.SpecialLinearGroup.im_smul_eq_div_normSq
 

Mathlib/Analysis/NormedSpace/Star/Spectrum.lean

@@ -33,12 +33,12 @@ theorem unitary.spectrum_subset_circle (u : unitary E) :
   nontriviality E
   refine' fun k hk => mem_sphere_zero_iff_norm.mpr (le_antisymm _ _)
   · simpa only [CstarRing.norm_coe_unitary u] using norm_le_norm_of_mem hk
-  · rw [← unitary.toUnits_apply_val u] at hk
+  · rw [← unitary.val_toUnits_apply u] at hk
     have hnk := ne_zero_of_mem_of_unit hk
     rw [← inv_inv (unitary.toUnits u), ← spectrum.map_inv, Set.mem_inv] at hk
     have : ‖k‖⁻¹ ≤ ‖(↑(unitary.toUnits u)⁻¹ : E)‖ :=
       by simpa only [norm_inv] using norm_le_norm_of_mem hk
-    simpa [←Units.inv_eq_val_inv] using inv_le_of_inv_le (norm_pos_iff.mpr hnk) this
+    simpa using inv_le_of_inv_le (norm_pos_iff.mpr hnk) this
 #align unitary.spectrum_subset_circle unitary.spectrum_subset_circle
 
 theorem spectrum.subset_circle_of_unitary {u : E} (h : u ∈ unitary E) :

Mathlib/Analysis/NormedSpace/Units.lean

@@ -46,7 +46,7 @@ def oneSub (t : R) (h : ‖t‖ < 1) : Rˣ where
   val_inv := mul_neg_geom_series t h
   inv_val := geom_series_mul_neg t h
 #align units.one_sub Units.oneSub
-#align units.coe_one_sub Units.oneSub_val
+#align units.coe_one_sub Units.val_oneSub
 
 /-- In a complete normed ring, a perturbation of a unit `x` by an element `t` of distance less than
 `‖x⁻¹‖⁻¹` from `x` is a unit.  Here we construct its `Units` structure. -/
@@ -63,15 +63,15 @@ def add (x : Rˣ) (t : R) (h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹) : Rˣ :=
         _ = 1 := mul_inv_cancel (ne_of_gt hpos)))
     (x + t) (by simp [mul_add]) _ rfl
 #align units.add Units.add
-#align units.coe_add Units.add_val
+#align units.coe_add Units.val_add
 
 /-- In a complete normed ring, an element `y` of distance less than `‖x⁻¹‖⁻¹` from `x` is a unit.
 Here we construct its `Units` structure. -/
 @[simps! val]
 def ofNearby (x : Rˣ) (y : R) (h : ‖y - x‖ < ‖(↑x⁻¹ : R)‖⁻¹) : Rˣ :=
   (x.add (y - x : R) h).copy y (by simp) _ rfl
 #align units.unit_of_nearby Units.ofNearby
-#align units.coe_unit_of_nearby Units.ofNearby_val
+#align units.coe_unit_of_nearby Units.val_ofNearby
 
 /-- The group of units of a complete normed ring is an open subset of the ring. -/
 protected theorem isOpen : IsOpen { x : R | IsUnit x } := by
@@ -111,7 +111,7 @@ open Classical BigOperators
 open Asymptotics Filter Metric Finset Ring
 
 theorem inverse_one_sub (t : R) (h : ‖t‖ < 1) : inverse (1 - t) = ↑(Units.oneSub t h)⁻¹ := by
-  rw [← inverse_unit (Units.oneSub t h), Units.oneSub_val]
+  rw [← inverse_unit (Units.oneSub t h), Units.val_oneSub]
 #align normed_ring.inverse_one_sub NormedRing.inverse_one_sub
 
 /-- The formula `Ring.inverse (x + t) = Ring.inverse (1 + x⁻¹ * t) * x⁻¹` holds for `t` sufficiently
@@ -122,8 +122,8 @@ theorem inverse_add (x : Rˣ) :
   rw [Metric.eventually_nhds_iff]
   refine ⟨‖(↑x⁻¹ : R)‖⁻¹, by cancel_denoms, fun t ht ↦ ?_⟩
   rw [dist_zero_right] at ht
-  rw [← x.add_val t ht, inverse_unit, Units.add, Units.copy_eq, mul_inv_rev, Units.val_mul,
-    ← inverse_unit, Units.oneSub_val, sub_neg_eq_add]
+  rw [← x.val_add t ht, inverse_unit, Units.add, Units.copy_eq, mul_inv_rev, Units.val_mul,
+    ← inverse_unit, Units.val_oneSub, sub_neg_eq_add]
 #align normed_ring.inverse_add NormedRing.inverse_add
 
 theorem inverse_one_sub_nth_order' (n : ℕ) {t : R} (ht : ‖t‖ < 1) :

Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean

@@ -72,7 +72,7 @@ def det : GL n R →* Rˣ where
   map_one' := Units.ext det_one
   map_mul' A B := Units.ext <| det_mul _ _
 #align matrix.general_linear_group.det Matrix.GeneralLinearGroup.det
-#align matrix.general_linear_group.coe_det_apply Matrix.GeneralLinearGroup.det_apply_val
+#align matrix.general_linear_group.coe_det_apply Matrix.GeneralLinearGroup.val_det_apply
 
 /-- The `GL n R` and `Matrix.GeneralLinearGroup R n` groups are multiplicatively equivalent-/
 def toLin : GL n R ≃* LinearMap.GeneralLinearGroup R (n → R) :=
@@ -213,7 +213,7 @@ each element. -/
 instance : Neg (GLPos n R) :=
   ⟨fun g =>
     ⟨-g, by
-      rw [mem_glpos, GeneralLinearGroup.det_apply_val, Units.val_neg, det_neg,
+      rw [mem_glpos, GeneralLinearGroup.val_det_apply, Units.val_neg, det_neg,
         (Fact.out (p := Even <| Fintype.card n)).neg_one_pow, one_mul]
       exact g.prop⟩⟩
 

Mathlib/NumberTheory/Cyclotomic/Gal.lean

@@ -78,7 +78,7 @@ theorem autToPow_injective : Function.Injective <| hμ.autToPow K := by
   convert hfg
   rw [hμ.eq_orderOf]
   -- Porting note: was `{occs := occurrences.pos [2]}`
-  conv_rhs => rw [← hμ.toRootsOfUnity_coe_val]
+  conv_rhs => rw [← hμ.val_toRootsOfUnity_coe]
   rw [orderOf_units, orderOf_subgroup]
 #align is_primitive_root.aut_to_pow_injective IsPrimitiveRoot.autToPow_injective
 
@@ -131,12 +131,12 @@ noncomputable def autEquivPow : (L ≃ₐ[K] L) ≃* (ZMod n)ˣ :=
 -- Porting note: was `rw ← hζ.coe_to_roots_of_unity_coe at key {occs := occurrences.pos [1, 5]}`.
       conv at key =>
         congr; congr
-        rw [← hζ.toRootsOfUnity_coe_val]
+        rw [← hζ.val_toRootsOfUnity_coe]
         rfl; rfl
-        rw [← hζ.toRootsOfUnity_coe_val]
+        rw [← hζ.val_toRootsOfUnity_coe]
       simp only [← rootsOfUnity.coe_pow] at key
       replace key := rootsOfUnity.coe_injective key
-      rw [pow_eq_pow_iff_modEq, ← orderOf_subgroup, ← orderOf_units, hζ.toRootsOfUnity_coe_val, ←
+      rw [pow_eq_pow_iff_modEq, ← orderOf_subgroup, ← orderOf_units, hζ.val_toRootsOfUnity_coe, ←
         (zeta_spec n K L).eq_orderOf, ← ZMod.eq_iff_modEq_nat] at key
       simp only [ZMod.nat_cast_val, ZMod.cast_id', id.def] at key
       exact Units.ext key }

Mathlib/NumberTheory/Modular.lean

@@ -223,13 +223,13 @@ theorem tendsto_lcRow0 {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0) (cd 1)) :
   · simp only [mulVec, dotProduct, Fin.sum_univ_two, coe_matrix_coe,
       Int.coe_castRingHom, lcRow0_apply, Function.comp_apply, cons_val_zero, lcRow0Extend_apply,
       LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLinear,
-      planeConformalMatrix_val, neg_neg, mulVecLin_apply, cons_val_one, head_cons, of_apply,
+      val_planeConformalMatrix, neg_neg, mulVecLin_apply, cons_val_one, head_cons, of_apply,
       Fin.mk_zero, Fin.mk_one]
   · convert congr_arg (fun n : ℤ => (-n : ℝ)) g.det_coe.symm using 1
     simp only [mulVec, dotProduct, Fin.sum_univ_two, Matrix.det_fin_two, Function.comp_apply,
       Subtype.coe_mk, lcRow0Extend_apply, cons_val_zero,
       LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLinear,
-      planeConformalMatrix_val, mulVecLin_apply, cons_val_one, head_cons, map_apply, neg_mul,
+      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]
     ring
   · rfl

Mathlib/NumberTheory/ModularForms/SlashActions.lean

@@ -134,7 +134,7 @@ private theorem smul_slash (k : ℤ) (A : GL(2, ℝ)⁺) (f : ℍ → ℂ) (c :
   simp_rw [← smul_one_smul ℂ c f, ← smul_one_smul ℂ c (f ∣[k]A)]
   ext1
   simp_rw [slash]
-  simp only [slash, Algebra.id.smul_eq_mul, Matrix.GeneralLinearGroup.det_apply_val, Pi.smul_apply]
+  simp only [slash, Algebra.id.smul_eq_mul, Matrix.GeneralLinearGroup.val_det_apply, Pi.smul_apply]
   ring
 
 private theorem zero_slash (k : ℤ) (A : GL(2, ℝ)⁺) : (0 : ℍ → ℂ) ∣[k]A = 0 :=
@@ -204,7 +204,7 @@ theorem slash_action_eq'_iff (k : ℤ) (Γ : Subgroup SL(2, ℤ)) (f : ℍ → 
 theorem mul_slash (k1 k2 : ℤ) (A : GL(2, ℝ)⁺) (f g : ℍ → ℂ) :
     (f * g) ∣[k1 + k2] A = ((↑ₘA).det : ℝ) • f ∣[k1] A * g ∣[k2] A := by
   ext1 x
-  simp only [slash_def, slash, Matrix.GeneralLinearGroup.det_apply_val,
+  simp only [slash_def, slash, Matrix.GeneralLinearGroup.val_det_apply,
     Pi.mul_apply, Pi.smul_apply, Algebra.smul_mul_assoc, real_smul]
   set d : ℂ := ↑((↑ₘA).det : ℝ)
   have h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1) := by