chore: some simpNF cleanaup after #3414 (#4033)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib/Data/Finset/Pointwise.lean

@@ -2044,7 +2044,7 @@ theorem mem_inv_smul_finset_iff₀ (ha : a ≠ 0) : b ∈ a⁻¹ • s ↔ a •
   show _ ∈ (Units.mk0 a ha)⁻¹ • _ ↔ _ from mem_inv_smul_finset_iff
 #align finset.mem_inv_smul_finset_iff₀ Finset.mem_inv_smul_finset_iff₀
 
--- @[simp] -- Porting note: `simpNF` linter times out
+@[simp]
 theorem smul_finset_subset_smul_finset_iff₀ (ha : a ≠ 0) : a • s ⊆ a • t ↔ s ⊆ t :=
   show Units.mk0 a ha • _ ⊆ _ ↔ _ from smul_finset_subset_smul_finset_iff
 #align finset.smul_finset_subset_smul_finset_iff₀ Finset.smul_finset_subset_smul_finset_iff₀

Mathlib/LinearAlgebra/Isomorphisms.lean

@@ -108,52 +108,42 @@ noncomputable def quotientInfEquivSupQuotient (p p' : Submodule R M) :
     ⟨quotientInfEquivSupQuotient_injective p p', quotientInfEquivSupQuotient_surjective p p'⟩
 #align linear_map.quotient_inf_equiv_sup_quotient LinearMap.quotientInfEquivSupQuotient
 
--- Porting note: wrapper to help with tc synthesis timing out
--- Try to remove these during lean4#2210 cleanup
-/-- These should be removed -/
-abbrev asFun (f : M ≃ₗ[R] M₂) : M → M₂ := f
-theorem asFun_coe (f : M ≃ₗ[R] M₂) : asFun f = f := rfl
-
 -- @[simp]
 -- Porting note: `simp` affects the type arguments of `FunLike.coe`, so this theorem can't be
 --               a simp theorem anymore, even if it has high priority.
 theorem coe_quotientInfToSupQuotient (p p' : Submodule R M) :
-    ⇑(quotientInfToSupQuotient p p') = asFun (quotientInfEquivSupQuotient p p') :=
+    ⇑(quotientInfToSupQuotient p p') = quotientInfEquivSupQuotient p p' :=
   rfl
 #align linear_map.coe_quotient_inf_to_sup_quotient LinearMap.coe_quotientInfToSupQuotient
 
--- Porting note: using asFun to avoid timing out
-@[simp, nolint simpNF] -- Porting note: The linter timeouts.
+@[simp]
 theorem quotientInfEquivSupQuotient_apply_mk (p p' : Submodule R M) (x : p) :
     let map := ofLe (le_sup_left : p ≤ p ⊔ p')
-    asFun (quotientInfEquivSupQuotient p p') (Submodule.Quotient.mk x) =
+    quotientInfEquivSupQuotient p p' (Submodule.Quotient.mk x) =
       @Submodule.Quotient.mk R (p ⊔ p' : Submodule R M) _ _ _ (comap (p ⊔ p').subtype p') (map x) :=
   rfl
 #align linear_map.quotient_inf_equiv_sup_quotient_apply_mk LinearMap.quotientInfEquivSupQuotient_apply_mk
 
--- Porting note: using asFun to avoid timing out
 theorem quotientInfEquivSupQuotient_symm_apply_left (p p' : Submodule R M) (x : ↥(p ⊔ p'))
     (hx : (x : M) ∈ p) :
-    asFun ((quotientInfEquivSupQuotient p p').symm) (Submodule.Quotient.mk x) =
+    (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) =
       Submodule.Quotient.mk ⟨x, hx⟩ :=
   (LinearEquiv.symm_apply_eq _).2 <| by
     -- Porting note: Was `simp`.
-    rw [← asFun_coe, quotientInfEquivSupQuotient_apply_mk, ofLe_apply]
+    rw [quotientInfEquivSupQuotient_apply_mk, ofLe_apply]
 #align linear_map.quotient_inf_equiv_sup_quotient_symm_apply_left LinearMap.quotientInfEquivSupQuotient_symm_apply_left
 
 
--- Porting note: using asFun to avoid timing out
 -- @[simp] -- Porting note: simp can prove this
 theorem quotientInfEquivSupQuotient_symm_apply_eq_zero_iff {p p' : Submodule R M} {x : ↥(p ⊔ p')} :
-    asFun ((quotientInfEquivSupQuotient p p').symm) (Submodule.Quotient.mk x) = 0 ↔ (x : M) ∈ p' :=
+    (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0 ↔ (x : M) ∈ p' :=
   (LinearEquiv.symm_apply_eq _).trans <| by
     -- Porting note: Was `simp`.
     rw [_root_.map_zero, Quotient.mk_eq_zero, mem_comap, Submodule.coeSubtype]
 #align linear_map.quotient_inf_equiv_sup_quotient_symm_apply_eq_zero_iff LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff
 
--- Porting note: using asFun to avoid timing out
 theorem quotientInfEquivSupQuotient_symm_apply_right (p p' : Submodule R M) {x : ↥(p ⊔ p')}
-    (hx : (x : M) ∈ p') : asFun ((quotientInfEquivSupQuotient p p').symm) (Submodule.Quotient.mk x)
+    (hx : (x : M) ∈ p') : (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x)
     = 0 :=
   quotientInfEquivSupQuotient_symm_apply_eq_zero_iff.2 hx
 #align linear_map.quotient_inf_equiv_sup_quotient_symm_apply_right LinearMap.quotientInfEquivSupQuotient_symm_apply_right

Mathlib/RingTheory/Ideal/QuotientOperations.lean

@@ -286,12 +286,18 @@ theorem kerLiftAlg_mk (f : A →ₐ[R₁] B) (a : A) :
   rfl
 #align ideal.ker_lift_alg_mk Ideal.kerLiftAlg_mk
 
--- Porting note: short circuit tc synth and use unification (_)
-@[simp]
+-- Porting note: not sure about this simpNF
+-- The linter says:
+-- #check Ideal.kerLiftAlg_toRingHom.{u_3, u_2, u_1} /- Left-hand side simplifies from
+--   ↑(Ideal.kerLiftAlg f)
+-- to
+--   ↑(Ideal.kerLiftAlg f)
+-- using
+--   simp only [@AlgHom.toRingHom_eq_coe]
+@[simp, nolint simpNF]
 theorem kerLiftAlg_toRingHom (f : A →ₐ[R₁] B) :
-    @AlgHom.toRingHom (R := R₁) (A := A ⧸ RingHom.ker f) (B := B) _ (_) _ (_) _ (kerLiftAlg f)
-      = RingHom.kerLift (R := A) (S := B)
-        (@AlgHom.toRingHom (R := R₁) (A := A) (B := B) _ _ _ _ _ f) := rfl
+    (kerLiftAlg f).toRingHom = RingHom.kerLift (f : A →+* B) :=
+  rfl
 #align ideal.ker_lift_alg_to_ring_hom Ideal.kerLiftAlg_toRingHom
 
 -- Porting note: short circuit tc synth and use unification (_)
@@ -662,14 +668,6 @@ theorem quotQuotEquivComm_algebraMap (x : R) :
   rfl
 #align double_quot.quot_quot_equiv_comm_algebra_map DoubleQuot.quotQuotEquivComm_algebraMap
 
--- Porting note: timing out due to Lean4#2074
-attribute [nolint simpNF] Ideal.kerLiftAlg_toRingHom
-Ideal.quotientKerAlgEquivOfRightInverse.apply
-Ideal.QuotientKerAlgEquivOfRightInverseSymm.apply
-DoubleQuot.quotQuotEquivComm_comp_quotQuotMk
-DoubleQuot.quotQuotEquivComm_mk_mk
-Ideal.kerLiftAlg_mk
-
 end Algebra
 
 end DoubleQuot