chore(LinearAlgebra/Matrix/ToLin): clean up (#11171)

Mathlib/Data/Matrix/Basic.lean

@@ -201,6 +201,12 @@ instance inhabited [Inhabited α] : Inhabited (Matrix m n α) :=
 instance decidableEq [DecidableEq α] [Fintype m] [Fintype n] : DecidableEq (Matrix m n α) :=
   Fintype.decidablePiFintype
 
+instance {n m} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (α) [Fintype α] :
+    Fintype (Matrix m n α) := inferInstanceAs (Fintype (m → n → α))
+
+instance {n m} [Finite m] [Finite n] (α) [Finite α] :
+    Finite (Matrix m n α) := inferInstanceAs (Finite (m → n → α))
+
 instance add [Add α] : Add (Matrix m n α) :=
   Pi.instAdd
 

Mathlib/LinearAlgebra/Matrix/ToLin.lean

@@ -66,15 +66,7 @@ linear_map, matrix, linear_equiv, diagonal, det, trace
 noncomputable section
 
 open LinearMap Matrix Set Submodule
-
-open BigOperators
-
-open Matrix
-
-universe u v w
-
-instance {n m} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (R) [Fintype R] :
-    Fintype (Matrix m n R) := by unfold Matrix; infer_instance
+open scoped BigOperators
 
 section ToMatrixRight
 
@@ -84,8 +76,8 @@ variable {l m n : Type*}
 /-- `Matrix.vecMul M` is a linear map. -/
 def Matrix.vecMulLinear [Fintype m] (M : Matrix m n R) : (m → R) →ₗ[R] n → R where
   toFun x := x ᵥ* M
-  map_add' _ _ := funext fun _ => add_dotProduct _ _ _
-  map_smul' _ _ := funext fun _ => smul_dotProduct _ _ _
+  map_add' _ _ := funext fun _ ↦ add_dotProduct _ _ _
+  map_smul' _ _ := funext fun _ ↦ smul_dotProduct _ _ _
 #align matrix.vec_mul_linear Matrix.vecMulLinear
 
 @[simp] theorem Matrix.vecMulLinear_apply [Fintype m] (M : Matrix m n R) (x : m → R) :
@@ -98,7 +90,7 @@ variable [Fintype m] [DecidableEq m]
 
 @[simp]
 theorem Matrix.vecMul_stdBasis (M : Matrix m n R) (i j) :
-    (LinearMap.stdBasis R (fun _ => R) i 1 ᵥ* M) j = M i j := by
+    (LinearMap.stdBasis R (fun _ ↦ R) i 1 ᵥ* M) j = M i j := by
   have : (∑ i', (if i = i' then 1 else 0) * M i' j) = M i j := by
     simp_rw [boole_mul, Finset.sum_ite_eq, Finset.mem_univ, if_true]
   simp only [vecMul, dotProduct]
@@ -135,7 +127,7 @@ theorem Matrix.vecMul_injective_iff {R : Type*} [CommRing R] {M : Matrix m n R}
 by having matrices act by right multiplication.
  -/
 def LinearMap.toMatrixRight' : ((m → R) →ₗ[R] n → R) ≃ₗ[Rᵐᵒᵖ] Matrix m n R where
-  toFun f i j := f (stdBasis R (fun _ => R) i 1) j
+  toFun f i j := f (stdBasis R (fun _ ↦ R) i 1) j
   invFun := Matrix.vecMulLinear
   right_inv M := by
     ext i j
@@ -160,8 +152,7 @@ abbrev Matrix.toLinearMapRight' : Matrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →
 
 @[simp]
 theorem Matrix.toLinearMapRight'_apply (M : Matrix m n R) (v : m → R) :
-    Matrix.toLinearMapRight' M v = v ᵥ* M :=
-  rfl
+    (Matrix.toLinearMapRight') M v = v ᵥ* M := rfl
 #align matrix.to_linear_map_right'_apply Matrix.toLinearMapRight'_apply
 
 @[simp]
@@ -218,8 +209,8 @@ variable {k l m n : Type*}
 /-- `Matrix.mulVec M` is a linear map. -/
 def Matrix.mulVecLin [Fintype n] (M : Matrix m n R) : (n → R) →ₗ[R] m → R where
   toFun := M.mulVec
-  map_add' _ _ := funext fun _ => dotProduct_add _ _ _
-  map_smul' _ _ := funext fun _ => dotProduct_smul _ _ _
+  map_add' _ _ := funext fun _ ↦ dotProduct_add _ _ _
+  map_smul' _ _ := funext fun _ ↦ dotProduct_smul _ _ _
 #align matrix.mul_vec_lin Matrix.mulVecLin
 
 theorem Matrix.coe_mulVecLin [Fintype n] (M : Matrix m n R) :
@@ -239,7 +230,7 @@ theorem Matrix.mulVecLin_zero [Fintype n] : Matrix.mulVecLin (0 : Matrix m n R)
 @[simp]
 theorem Matrix.mulVecLin_add [Fintype n] (M N : Matrix m n R) :
     (M + N).mulVecLin = M.mulVecLin + N.mulVecLin :=
-  LinearMap.ext fun _ => add_mulVec _ _ _
+  LinearMap.ext fun _ ↦ add_mulVec _ _ _
 #align matrix.mul_vec_lin_add Matrix.mulVecLin_add
 
 @[simp] theorem Matrix.mulVecLin_transpose [Fintype m] (M : Matrix m n R) :
@@ -253,7 +244,7 @@ theorem Matrix.mulVecLin_add [Fintype n] (M N : Matrix m n R) :
 theorem Matrix.mulVecLin_submatrix [Fintype n] [Fintype l] (f₁ : m → k) (e₂ : n ≃ l)
     (M : Matrix k l R) :
     (M.submatrix f₁ e₂).mulVecLin = funLeft R R f₁ ∘ₗ M.mulVecLin ∘ₗ funLeft _ _ e₂.symm :=
-  LinearMap.ext fun _ => submatrix_mulVec_equiv _ _ _ _
+  LinearMap.ext fun _ ↦ submatrix_mulVec_equiv _ _ _ _
 #align matrix.mul_vec_lin_submatrix Matrix.mulVecLin_submatrix
 
 /-- A variant of `Matrix.mulVecLin_submatrix` that keeps around `LinearEquiv`s. -/
@@ -276,7 +267,7 @@ theorem Matrix.mulVecLin_one [DecidableEq n] :
 @[simp]
 theorem Matrix.mulVecLin_mul [Fintype m] (M : Matrix l m R) (N : Matrix m n R) :
     Matrix.mulVecLin (M * N) = (Matrix.mulVecLin M).comp (Matrix.mulVecLin N) :=
-  LinearMap.ext fun _ => (mulVec_mulVec _ _ _).symm
+  LinearMap.ext fun _ ↦ (mulVec_mulVec _ _ _).symm
 #align matrix.mul_vec_lin_mul Matrix.mulVecLin_mul
 
 theorem Matrix.ker_mulVecLin_eq_bot_iff {M : Matrix m n R} :
@@ -285,14 +276,14 @@ theorem Matrix.ker_mulVecLin_eq_bot_iff {M : Matrix m n R} :
 #align matrix.ker_mul_vec_lin_eq_bot_iff Matrix.ker_mulVecLin_eq_bot_iff
 
 theorem Matrix.mulVec_stdBasis [DecidableEq n] (M : Matrix m n R) (i j) :
-    (M *ᵥ LinearMap.stdBasis R (fun _ => R) j 1) i = M i j :=
+    (M *ᵥ LinearMap.stdBasis R (fun _ ↦ R) j 1) i = M i j :=
   (congr_fun (Matrix.mulVec_single _ _ (1 : R)) i).trans <| mul_one _
 #align matrix.mul_vec_std_basis Matrix.mulVec_stdBasis
 
 @[simp]
 theorem Matrix.mulVec_stdBasis_apply [DecidableEq n] (M : Matrix m n R) (j) :
-    M *ᵥ LinearMap.stdBasis R (fun _ => R) j 1 = Mᵀ j :=
-  funext fun i => Matrix.mulVec_stdBasis M i j
+    M *ᵥ LinearMap.stdBasis R (fun _ ↦ R) j 1 = Mᵀ j :=
+  funext fun i ↦ Matrix.mulVec_stdBasis M i j
 #align matrix.mul_vec_std_basis_apply Matrix.mulVec_stdBasis_apply
 
 theorem Matrix.range_mulVecLin (M : Matrix m n R) :
@@ -314,7 +305,7 @@ variable {k l m n : Type*} [DecidableEq n] [Fintype n]
 
 /-- Linear maps `(n → R) →ₗ[R] (m → R)` are linearly equivalent to `Matrix m n R`. -/
 def LinearMap.toMatrix' : ((n → R) →ₗ[R] m → R) ≃ₗ[R] Matrix m n R where
-  toFun f := of fun i j => f (stdBasis R (fun _ => R) j 1) i
+  toFun f := of fun i j ↦ f (stdBasis R (fun _ ↦ R) j 1) i
   invFun := Matrix.mulVecLin
   right_inv M := by
     ext i j
@@ -367,7 +358,7 @@ theorem Matrix.toLin'_toMatrix' (f : (n → R) →ₗ[R] m → R) :
 
 @[simp]
 theorem LinearMap.toMatrix'_apply (f : (n → R) →ₗ[R] m → R) (i j) :
-    LinearMap.toMatrix' f i j = f (fun j' => if j' = j then 1 else 0) i := by
+    LinearMap.toMatrix' f i j = f (fun j' ↦ if j' = j then 1 else 0) i := by
   simp only [LinearMap.toMatrix', LinearEquiv.coe_mk, of_apply]
   refine congr_fun ?_ _  -- Porting note: `congr` didn't do this
   congr
@@ -463,8 +454,8 @@ def Matrix.toLin'OfInv [Fintype m] [DecidableEq m] {M : Matrix m n R} {M' : Matr
   { Matrix.toLin' M' with
     toFun := Matrix.toLin' M'
     invFun := Matrix.toLin' M
-    left_inv := fun x => by rw [← Matrix.toLin'_mul_apply, hMM', Matrix.toLin'_one, id_apply]
-    right_inv := fun x => by
+    left_inv := fun x ↦ by rw [← Matrix.toLin'_mul_apply, hMM', Matrix.toLin'_one, id_apply]
+    right_inv := fun x ↦ by
       simp only
       rw [← Matrix.toLin'_mul_apply, hM'M, Matrix.toLin'_one, id_apply] }
 #align matrix.to_lin'_of_inv Matrix.toLin'OfInv
@@ -505,7 +496,7 @@ theorem Matrix.toLinAlgEquiv'_toMatrixAlgEquiv' (f : (n → R) →ₗ[R] n → R
 
 @[simp]
 theorem LinearMap.toMatrixAlgEquiv'_apply (f : (n → R) →ₗ[R] n → R) (i j) :
-    LinearMap.toMatrixAlgEquiv' f i j = f (fun j' => if j' = j then 1 else 0) i := by
+    LinearMap.toMatrixAlgEquiv' f i j = f (fun j' ↦ if j' = j then 1 else 0) i := by
   simp [LinearMap.toMatrixAlgEquiv']
 #align linear_map.to_matrix_alg_equiv'_apply LinearMap.toMatrixAlgEquiv'_apply
 
@@ -515,7 +506,7 @@ theorem Matrix.toLinAlgEquiv'_apply (M : Matrix n n R) (v : n → R) :
   rfl
 #align matrix.to_lin_alg_equiv'_apply Matrix.toLinAlgEquiv'_apply
 
--- Porting note: the simpNF lemma rejects this, as `simp` already simplifies the lhs
+-- Porting note: the simpNF linter rejects this, as `simp` already simplifies the lhs
 -- to `(1 : (n → R) →ₗ[R] n → R)`.
 -- @[simp]
 theorem Matrix.toLinAlgEquiv'_one : Matrix.toLinAlgEquiv' (1 : Matrix n n R) = LinearMap.id :=
@@ -612,7 +603,7 @@ theorem LinearMap.toMatrix_apply (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
 
 theorem LinearMap.toMatrix_transpose_apply (f : M₁ →ₗ[R] M₂) (j : n) :
     (LinearMap.toMatrix v₁ v₂ f)ᵀ j = v₂.repr (f (v₁ j)) :=
-  funext fun i => f.toMatrix_apply _ _ i j
+  funext fun i ↦ f.toMatrix_apply _ _ i j
 #align linear_map.to_matrix_transpose_apply LinearMap.toMatrix_transpose_apply
 
 theorem LinearMap.toMatrix_apply' (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
@@ -634,7 +625,7 @@ theorem Matrix.toLin_apply (M : Matrix m n R) (v : M₁) :
 @[simp]
 theorem Matrix.toLin_self (M : Matrix m n R) (i : n) :
     Matrix.toLin v₁ v₂ M (v₁ i) = ∑ j, M j i • v₂ j := by
-  rw [Matrix.toLin_apply, Finset.sum_congr rfl fun j _hj => ?_]
+  rw [Matrix.toLin_apply, Finset.sum_congr rfl fun j _hj ↦ ?_]
   rw [Basis.repr_self, Matrix.mulVec, dotProduct, Finset.sum_eq_single i, Finsupp.single_eq_same,
     mul_one]
   · intro i' _ i'_ne
@@ -713,7 +704,7 @@ theorem LinearMap.toMatrix_basis_equiv [Fintype l] [DecidableEq l] (b : Basis l
 theorem Matrix.toLin_mul [Fintype l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R) :
     Matrix.toLin v₁ v₃ (A * B) = (Matrix.toLin v₂ v₃ A).comp (Matrix.toLin v₁ v₂ B) := by
   apply (LinearMap.toMatrix v₁ v₃).injective
-  haveI : DecidableEq l := fun _ _ => Classical.propDecidable _
+  haveI : DecidableEq l := fun _ _ ↦ Classical.propDecidable _
   rw [LinearMap.toMatrix_comp v₁ v₂ v₃]
   repeat' rw [LinearMap.toMatrix_toLin]
 #align matrix.to_lin_mul Matrix.toLin_mul
@@ -732,8 +723,8 @@ def Matrix.toLinOfInv [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hM
   { Matrix.toLin v₁ v₂ M with
     toFun := Matrix.toLin v₁ v₂ M
     invFun := Matrix.toLin v₂ v₁ M'
-    left_inv := fun x => by rw [← Matrix.toLin_mul_apply, hM'M, Matrix.toLin_one, id_apply]
-    right_inv := fun x => by
+    left_inv := fun x ↦ by rw [← Matrix.toLin_mul_apply, hM'M, Matrix.toLin_one, id_apply]
+    right_inv := fun x ↦ by
       simp only
       rw [← Matrix.toLin_mul_apply, hMM', Matrix.toLin_one, id_apply] }
 #align matrix.to_lin_of_inv Matrix.toLinOfInv
@@ -782,7 +773,7 @@ theorem LinearMap.toMatrixAlgEquiv_apply (f : M₁ →ₗ[R] M₁) (i j : n) :
 
 theorem LinearMap.toMatrixAlgEquiv_transpose_apply (f : M₁ →ₗ[R] M₁) (j : n) :
     (LinearMap.toMatrixAlgEquiv v₁ f)ᵀ j = v₁.repr (f (v₁ j)) :=
-  funext fun i => f.toMatrix_apply _ _ i j
+  funext fun i ↦ f.toMatrix_apply _ _ i j
 #align linear_map.to_matrix_alg_equiv_transpose_apply LinearMap.toMatrixAlgEquiv_transpose_apply
 
 theorem LinearMap.toMatrixAlgEquiv_apply' (f : M₁ →ₗ[R] M₁) (i j : n) :
@@ -811,7 +802,7 @@ theorem LinearMap.toMatrixAlgEquiv_id : LinearMap.toMatrixAlgEquiv v₁ id = 1 :
   simp_rw [LinearMap.toMatrixAlgEquiv, AlgEquiv.ofLinearEquiv_apply, LinearMap.toMatrix_id]
 #align linear_map.to_matrix_alg_equiv_id LinearMap.toMatrixAlgEquiv_id
 
--- Porting note: the simpNF lemma rejects this, as `simp` already simplifies the lhs
+-- Porting note: the simpNF linter rejects this, as `simp` already simplifies the lhs
 -- to `(1 : M₁ →ₗ[R] M₁)`.
 -- @[simp]
 theorem Matrix.toLinAlgEquiv_one : Matrix.toLinAlgEquiv v₁ 1 = LinearMap.id := by
@@ -860,7 +851,7 @@ theorem Matrix.toLin_finTwoProd (a b c d : R) :
 @[simp]
 theorem toMatrix_distrib_mul_action_toLinearMap (x : R) :
     LinearMap.toMatrix v₁ v₁ (DistribMulAction.toLinearMap R M₁ x) =
-    Matrix.diagonal fun _ => x := by
+    Matrix.diagonal fun _ ↦ x := by
   ext
   rw [LinearMap.toMatrix_apply, DistribMulAction.toLinearMap_apply, LinearEquiv.map_smul,
     Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
@@ -889,7 +880,7 @@ theorem toMatrix_lmul' (x : S) (i j) :
 
 @[simp]
 theorem toMatrix_lsmul (x : R) :
-    LinearMap.toMatrix b b (Algebra.lsmul R R S x) = Matrix.diagonal fun _ => x :=
+    LinearMap.toMatrix b b (Algebra.lsmul R R S x) = Matrix.diagonal fun _ ↦ x :=
   toMatrix_distrib_mul_action_toLinearMap b x
 #align algebra.to_matrix_lsmul Algebra.toMatrix_lsmul
 
@@ -942,7 +933,7 @@ theorem toMatrix_lmul_eq (x : S) :
   rfl
 #align algebra.to_matrix_lmul_eq Algebra.toMatrix_lmul_eq
 
-theorem leftMulMatrix_injective : Function.Injective (leftMulMatrix b) := fun x x' h =>
+theorem leftMulMatrix_injective : Function.Injective (leftMulMatrix b) := fun x x' h ↦
   calc
     x = Algebra.lmul R S x 1 := (mul_one x).symm
     _ = Algebra.lmul R S x' 1 := by rw [(LinearMap.toMatrix b b).injective h]
@@ -966,7 +957,7 @@ theorem smul_leftMulMatrix (x) (ik jk) :
 #align algebra.smul_left_mul_matrix Algebra.smul_leftMulMatrix
 
 theorem smul_leftMulMatrix_algebraMap (x : S) :
-    leftMulMatrix (b.smul c) (algebraMap _ _ x) = blockDiagonal fun _ => leftMulMatrix b x := by
+    leftMulMatrix (b.smul c) (algebraMap _ _ x) = blockDiagonal fun _ ↦ leftMulMatrix b x := by
   ext ⟨i, k⟩ ⟨j, k'⟩
   rw [smul_leftMulMatrix, AlgHom.commutes, blockDiagonal_apply, algebraMap_matrix_apply]
   split_ifs with h <;> simp only at h <;> simp [h]
@@ -988,7 +979,7 @@ end Algebra
 
 section
 
-variable {R : Type v} [CommRing R] {n : Type*} [DecidableEq n]
+variable {R : Type*} [CommRing R] {n : Type*} [DecidableEq n]
 variable {M M₁ M₂ : Type*} [AddCommGroup M] [Module R M]
 variable [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂]
 
@@ -997,16 +988,15 @@ is compatible with the algebra structures. -/
 def algEquivMatrix' [Fintype n] : Module.End R (n → R) ≃ₐ[R] Matrix n n R :=
   { LinearMap.toMatrix' with
     map_mul' := LinearMap.toMatrix'_comp
-    -- Porting note: golfed away messy failing proof
     commutes' := LinearMap.toMatrix'_algebraMap }
 #align alg_equiv_matrix' algEquivMatrix'
 
 /-- A linear equivalence of two modules induces an equivalence of algebras of their
 endomorphisms. -/
 def LinearEquiv.algConj (e : M₁ ≃ₗ[R] M₂) : Module.End R M₁ ≃ₐ[R] Module.End R M₂ :=
   { e.conj with
-    map_mul' := fun f g => by apply e.arrowCongr_comp
-    commutes' := fun r => by
+    map_mul' := fun f g ↦ by apply e.arrowCongr_comp
+    commutes' := fun r ↦ by
       change e.conj (r • LinearMap.id) = r • LinearMap.id
       rw [LinearEquiv.map_smul, LinearEquiv.conj_id] }
 #align linear_equiv.alg_conj LinearEquiv.algConj