feat: port LinearAlgebra.Basis (#2435)

Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Co-authored-by: ADedecker <anatolededecker@gmail.com>
Co-authored-by: Anne Baanen <t.baanen@vu.nl>

Mathlib.lean

@@ -880,6 +880,7 @@ import Mathlib.Lean.Meta
 import Mathlib.Lean.Meta.Simp
 import Mathlib.LinearAlgebra.AffineSpace.Basic
 import Mathlib.LinearAlgebra.Basic
+import Mathlib.LinearAlgebra.Basis
 import Mathlib.LinearAlgebra.BilinearMap
 import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.LinearAlgebra.GeneralLinearGroup

Mathlib/Algebra/Module/Equiv.lean

@@ -280,6 +280,14 @@ def symm (e : M ≃ₛₗ[σ] M₂) : M₂ ≃ₛₗ[σ'] M :=
     map_smul' := fun r x => by dsimp only; rw [map_smulₛₗ] }
 #align linear_equiv.symm LinearEquiv.symm
 
+-- Porting note: this is new
+/-- See Note [custom simps projection] -/
+def Simps.apply {R : Type _} {S : Type _} [Semiring R] [Semiring S]
+    {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
+    {M : Type _} {M₂ : Type _} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂]
+    (e : M ≃ₛₗ[σ] M₂) : M → M₂ :=
+  e
+
 /-- See Note [custom simps projection] -/
 def Simps.symmApply {R : Type _} {S : Type _} [Semiring R] [Semiring S]
     {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
@@ -288,7 +296,7 @@ def Simps.symmApply {R : Type _} {S : Type _} [Semiring R] [Semiring S]
   e.symm
 #align linear_equiv.simps.symm_apply LinearEquiv.Simps.symmApply
 
-initialize_simps_projections LinearEquiv (toLinearMap → apply, invFun → symmApply)
+initialize_simps_projections LinearEquiv (toLinearMap_toAddHom_toFun → apply, invFun → symmApply)
 
 @[simp]
 theorem invFun_eq_symm : e.invFun = e.symm :=
@@ -614,6 +622,7 @@ def restrictScalars (f : M ≃ₗ[S] M₂) : M ≃ₗ[R] M₂ :=
     left_inv := f.left_inv
     right_inv := f.right_inv }
 #align linear_equiv.restrict_scalars LinearEquiv.restrictScalars
+#align linear_equiv.restrict_scalars_apply LinearEquiv.restrictScalars_apply
 #align linear_equiv.restrict_scalars_symm_apply LinearEquiv.restrictScalars_symmApply
 
 theorem restrictScalars_injective :
@@ -738,7 +747,7 @@ variable [Group S] [DistribMulAction S M] [SMulCommClass S R M]
 /-- Each element of the group defines a linear equivalence.
 
 This is a stronger version of `DistribMulAction.toAddEquiv`. -/
-@[simps]
+@[simps!]
 def toLinearEquiv (s : S) : M ≃ₗ[R] M :=
   { toAddEquiv M s, toLinearMap R M s with }
 #align distrib_mul_action.to_linear_equiv DistribMulAction.toLinearEquiv