chore(linear_algebra/matrix): Use the new matrix notation in most places (#15306)

eric-wieser · eric-wieser · commit 65ec59902eb1 · 2022-07-17T21:26:35.000Z
diff --git a/src/algebra/lie/cartan_matrix.lean b/src/algebra/lie/cartan_matrix.lean
@@ -5,7 +5,7 @@ Authors: Oliver Nash
 -/
 import algebra.lie.free
 import algebra.lie.quotient
-import data.matrix.basic
+import data.matrix.notation
 
 /-!
 # Lie algebras from Cartan matrices
@@ -182,12 +182,12 @@ The corresponding Dynkin diagram is:
 o --- o --- o --- o --- o
 ```
 -/
-def E₆ : matrix (fin 6) (fin 6) ℤ := ![![ 2,  0, -1,  0,  0,  0],
-                                       ![ 0,  2,  0, -1,  0,  0],
-                                       ![-1,  0,  2, -1,  0,  0],
-                                       ![ 0, -1, -1,  2, -1,  0],
-                                       ![ 0,  0,  0, -1,  2, -1],
-                                       ![ 0,  0,  0,  0, -1,  2]]
+def E₆ : matrix (fin 6) (fin 6) ℤ := !![ 2,  0, -1,  0,  0,  0;
+                                         0,  2,  0, -1,  0,  0;
+                                        -1,  0,  2, -1,  0,  0;
+                                         0, -1, -1,  2, -1,  0;
+                                         0,  0,  0, -1,  2, -1;
+                                         0,  0,  0,  0, -1,  2]
 
 /-- The Cartan matrix of type e₇. See [bourbaki1968] plate VI, page 281.
 
@@ -198,13 +198,13 @@ The corresponding Dynkin diagram is:
 o --- o --- o --- o --- o --- o
 ```
 -/
-def E₇ : matrix (fin 7) (fin 7) ℤ := ![![ 2,  0, -1,  0,  0,  0,  0],
-                                       ![ 0,  2,  0, -1,  0,  0,  0],
-                                       ![-1,  0,  2, -1,  0,  0,  0],
-                                       ![ 0, -1, -1,  2, -1,  0,  0],
-                                       ![ 0,  0,  0, -1,  2, -1,  0],
-                                       ![ 0,  0,  0,  0, -1,  2, -1],
-                                       ![ 0,  0,  0,  0,  0, -1,  2]]
+def E₇ : matrix (fin 7) (fin 7) ℤ := !![ 2,  0, -1,  0,  0,  0,  0;
+                                         0,  2,  0, -1,  0,  0,  0;
+                                        -1,  0,  2, -1,  0,  0,  0;
+                                         0, -1, -1,  2, -1,  0,  0;
+                                         0,  0,  0, -1,  2, -1,  0;
+                                         0,  0,  0,  0, -1,  2, -1;
+                                         0,  0,  0,  0,  0, -1,  2]
 
 /-- The Cartan matrix of type e₈. See [bourbaki1968] plate VII, page 285.
 
@@ -215,14 +215,14 @@ The corresponding Dynkin diagram is:
 o --- o --- o --- o --- o --- o --- o
 ```
 -/
-def E₈ : matrix (fin 8) (fin 8) ℤ := ![![ 2,  0, -1,  0,  0,  0,  0,  0],
-                                       ![ 0,  2,  0, -1,  0,  0,  0,  0],
-                                       ![-1,  0,  2, -1,  0,  0,  0,  0],
-                                       ![ 0, -1, -1,  2, -1,  0,  0,  0],
-                                       ![ 0,  0,  0, -1,  2, -1,  0,  0],
-                                       ![ 0,  0,  0,  0, -1,  2, -1,  0],
-                                       ![ 0,  0,  0,  0,  0, -1,  2, -1],
-                                       ![ 0,  0,  0,  0,  0,  0, -1,  2]]
+def E₈ : matrix (fin 8) (fin 8) ℤ := !![ 2,  0, -1,  0,  0,  0,  0,  0;
+                                         0,  2,  0, -1,  0,  0,  0,  0;
+                                        -1,  0,  2, -1,  0,  0,  0,  0;
+                                         0, -1, -1,  2, -1,  0,  0,  0;
+                                         0,  0,  0, -1,  2, -1,  0,  0;
+                                         0,  0,  0,  0, -1,  2, -1,  0;
+                                         0,  0,  0,  0,  0, -1,  2, -1;
+                                         0,  0,  0,  0,  0,  0, -1,  2]
 
 /-- The Cartan matrix of type f₄. See [bourbaki1968] plate VIII, page 288.
 
@@ -231,10 +231,10 @@ The corresponding Dynkin diagram is:
 o --- o =>= o --- o
 ```
 -/
-def F₄ : matrix (fin 4) (fin 4) ℤ := ![![ 2, -1,  0,  0],
-                                       ![-1,  2, -2,  0],
-                                       ![ 0, -1,  2, -1],
-                                       ![ 0,  0, -1,  2]]
+def F₄ : matrix (fin 4) (fin 4) ℤ := !![ 2, -1,  0,  0;
+                                        -1,  2, -2,  0;
+                                         0, -1,  2, -1;
+                                         0,  0, -1,  2]
 
 /-- The Cartan matrix of type g₂. See [bourbaki1968] plate IX, page 290.
 
@@ -244,8 +244,8 @@ o ≡>≡ o
 ```
 Actually we are using the transpose of Bourbaki's matrix. This is to make this matrix consistent
 with `cartan_matrix.F₄`, in the sense that all non-zero values below the diagonal are -1. -/
-def G₂ : matrix (fin 2) (fin 2) ℤ := ![![ 2, -3],
-                                       ![-1,  2]]
+def G₂ : matrix (fin 2) (fin 2) ℤ := !![ 2, -3;
+                                        -1,  2]
 
 end cartan_matrix
 
diff --git a/src/analysis/complex/isometry.lean b/src/analysis/complex/isometry.lean
@@ -141,7 +141,7 @@ begin
 end
 
 /-- The matrix representation of `rotation a` is equal to the conformal matrix
-`![![re a, -im a], ![im a, re a]]`. -/
+`!![re a, -im a; im a, re a]`. -/
 lemma to_matrix_rotation (a : circle) :
   linear_map.to_matrix basis_one_I basis_one_I (rotation a).to_linear_equiv =
     matrix.plane_conformal_matrix (re a) (im a) (by simp [pow_two, ←norm_sq_apply]) :=
diff --git a/src/analysis/special_functions/polar_coord.lean b/src/analysis/special_functions/polar_coord.lean
@@ -97,7 +97,7 @@ It is a homeomorphism between `ℝ^2 - (-∞, 0]` and `(0, +∞) × (-π, π)`.
 lemma has_fderiv_at_polar_coord_symm (p : ℝ × ℝ) :
   has_fderiv_at polar_coord.symm
     (matrix.to_lin (basis.fin_two_prod ℝ) (basis.fin_two_prod ℝ)
-      (![![cos p.2, -p.1 * sin p.2], ![sin p.2, p.1 * cos p.2]])).to_continuous_linear_map p :=
+      (!![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2])).to_continuous_linear_map p :=
 begin
   rw matrix.to_lin_fin_two_prod_to_continuous_linear_map,
   convert has_fderiv_at.prod
@@ -130,15 +130,14 @@ theorem integral_comp_polar_coord_symm
 begin
   set B : (ℝ × ℝ) → ((ℝ × ℝ) →L[ℝ] (ℝ × ℝ)) := λ p,
     (matrix.to_lin (basis.fin_two_prod ℝ) (basis.fin_two_prod ℝ)
-      ![![cos p.2, -p.1 * sin p.2], ![sin p.2, p.1 * cos p.2]]).to_continuous_linear_map with hB,
+      !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2]).to_continuous_linear_map with hB,
   have A : ∀ p ∈ polar_coord.symm.source, has_fderiv_at polar_coord.symm (B p) p :=
     λ p hp, has_fderiv_at_polar_coord_symm p,
   have B_det : ∀ p, (B p).det = p.1,
   { assume p,
     conv_rhs {rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2] },
     simp only [neg_mul, linear_map.det_to_continuous_linear_map, linear_map.det_to_lin,
-      matrix.det_fin_two, sub_neg_eq_add, matrix.cons_val_zero, matrix.cons_val_one,
-      matrix.head_cons],
+      matrix.det_fin_two_of, sub_neg_eq_add],
     ring_exp },
   symmetry,
   calc
diff --git a/src/data/complex/determinant.lean b/src/data/complex/determinant.lean
@@ -19,7 +19,7 @@ namespace complex
 /-- The determinant of `conj_ae`, as a linear map. -/
 @[simp] lemma det_conj_ae : conj_ae.to_linear_map.det = -1 :=
 begin
-  rw [←linear_map.det_to_matrix basis_one_I, to_matrix_conj_ae, matrix.det_fin_two],
+  rw [←linear_map.det_to_matrix basis_one_I, to_matrix_conj_ae, matrix.det_fin_two_of],
   simp
 end
 
diff --git a/src/data/complex/module.lean b/src/data/complex/module.lean
@@ -230,7 +230,7 @@ def conj_ae : ℂ ≃ₐ[ℝ] ℂ :=
 
 /-- The matrix representation of `conj_ae`. -/
 @[simp] lemma to_matrix_conj_ae :
-  linear_map.to_matrix basis_one_I basis_one_I conj_ae.to_linear_map = ![![1, 0], ![0, -1]] :=
+  linear_map.to_matrix basis_one_I basis_one_I conj_ae.to_linear_map = !![1, 0; 0, -1] :=
 begin
   ext i j,
   simp [linear_map.to_matrix_apply],
diff --git a/src/data/fin/vec_notation.lean b/src/data/fin/vec_notation.lean
@@ -13,9 +13,8 @@ import meta.univs
 
 This file defines notation for vectors and matrices. Given `a b c d : α`,
 the notation allows us to write `![a, b, c, d] : fin 4 → α`.
-Nesting vectors gives a matrix, so `![![a, b], ![c, d]] : fin 2 → fin 2 → α`.
-Later we will define `matrix m n α` to be `m → n → α`, so the type of `![![a, b], ![c, d]]`
-can be written as `matrix (fin 2) (fin 2) α`.
+Nesting vectors gives coefficients of a matrix, so `![![a, b], ![c, d]] : fin 2 → fin 2 → α`.
+In later files we introduce `!![a, b; c, d]` as notation for `matrix.of ![![a, b], ![c, d]]`.
 
 ## Main definitions
 
diff --git a/src/data/matrix/notation.lean b/src/data/matrix/notation.lean
@@ -15,7 +15,7 @@ This file includes `simp` lemmas for applying operations in `data.matrix.basic`
 of the matrix notation `![a, b] = vec_cons a (vec_cons b vec_empty)` defined in
 `data.fin.vec_notation`.
 
-This also provides the new notation `!![a, b; c, d] = ![![a, b], ![c, d]]`.
+This also provides the new notation `!![a, b; c, d] = matrix.of ![![a, b], ![c, d]]`.
 This notation also works for empty matrices; `!![,,,] : matrix (fin 0) (fin 3)` and
 `!![;;;] : matrix (fin 3) (fin 0)`.
 
@@ -238,6 +238,10 @@ by { ext i, simp [vec_mul] }
   vec_mul v (of $ vec_cons w B) = vec_head v • w + vec_mul (vec_tail v) (of B) :=
 by { ext i, simp [vec_mul] }
 
+@[simp] lemma cons_vec_mul_cons (x : α) (v : fin n → α) (w : o' → α) (B : fin n → o' → α) :
+  vec_mul (vec_cons x v) (of $ vec_cons w B) = x • w + vec_mul v (of B) :=
+by simp
+
 end vec_mul
 
 section mul_vec
@@ -323,6 +327,15 @@ by { ext i j, fin_cases i; fin_cases j; refl }
 
 end one
 
+lemma eta_fin_two (A : matrix (fin 2) (fin 2) α) : A = !![A 0 0, A 0 1; A 1 0, A 1 1] :=
+by { ext i j, fin_cases i; fin_cases j; refl }
+
+lemma eta_fin_three (A : matrix (fin 3) (fin 3) α) :
+  A = !![A 0 0, A 0 1, A 0 2;
+         A 1 0, A 1 1, A 1 2;
+         A 2 0, A 2 1, A 2 2] :=
+by { ext i j, fin_cases i; fin_cases j; refl }
+
 lemma mul_fin_two [add_comm_monoid α] [has_mul α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
   !![a₁₁, a₁₂;
      a₂₁, a₂₂] ⬝ !![b₁₁, b₁₂;
diff --git a/src/linear_algebra/general_linear_group.lean b/src/linear_algebra/general_linear_group.lean
@@ -210,11 +210,11 @@ $GL_2(R)$ if `a ^ 2 + b ^ 2` is nonzero. -/
 @[simps coe {fully_applied := ff}]
 def plane_conformal_matrix {R} [field R] (a b : R) (hab : a ^ 2 + b ^ 2 ≠ 0) :
   matrix.general_linear_group (fin 2) R :=
-general_linear_group.mk_of_det_ne_zero ![![a, -b], ![b, a]]
+general_linear_group.mk_of_det_ne_zero !![a, -b; b, a]
   (by simpa [det_fin_two, sq] using hab)
 
-/- TODO: Add Iwasawa matrices `n_x=![![1,x],![0,1]]`, `a_t=![![exp(t/2),0],![0,exp(-t/2)]]` and
-  `k_θ==![![cos θ, sin θ],![-sin θ, cos θ]]`
+/- TODO: Add Iwasawa matrices `n_x=!![1,x; 0,1]`, `a_t=!![exp(t/2),0;0,exp(-t/2)]` and
+  `k_θ=!![cos θ, sin θ; -sin θ, cos θ]`
 -/
 
 end examples
diff --git a/src/linear_algebra/matrix/adjugate.lean b/src/linear_algebra/matrix/adjugate.lean
@@ -342,18 +342,18 @@ end
 adjugate_subsingleton A
 
 lemma adjugate_fin_two (A : matrix (fin 2) (fin 2) α) :
-  adjugate A = ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] :=
+  adjugate A = !![A 1 1, -A 0 1; -A 1 0, A 0 0] :=
 begin
   ext i j,
   rw [adjugate_apply, det_fin_two],
   fin_cases i with [0, 1]; fin_cases j with [0, 1];
   simp only [nat.one_ne_zero, one_mul, fin.one_eq_zero_iff, pi.single_eq_same, zero_mul,
     fin.zero_eq_one_iff, sub_zero, pi.single_eq_of_ne, ne.def, not_false_iff, update_row_self,
-    update_row_ne, cons_val_zero, mul_zero, mul_one, zero_sub, cons_val_one, head_cons],
+    update_row_ne, cons_val_zero, mul_zero, mul_one, zero_sub, cons_val_one, head_cons, of_apply],
 end
 
-@[simp] lemma adjugate_fin_two' (a b c d : α) :
-  adjugate ![![a, b], ![c, d]] = ![![d, -b], ![-c, a]] :=
+@[simp] lemma adjugate_fin_two_of (a b c d : α) :
+  adjugate !![a, b; c, d] = !![d, -b; -c, a] :=
 adjugate_fin_two _
 
 lemma adjugate_conj_transpose [star_ring α] (A : matrix n n α) : A.adjugateᴴ = adjugate (Aᴴ) :=
diff --git a/src/linear_algebra/matrix/determinant.lean b/src/linear_algebra/matrix/determinant.lean
@@ -5,6 +5,7 @@ Authors: Kenny Lau, Chris Hughes, Tim Baanen
 -/
 import data.matrix.pequiv
 import data.matrix.block
+import data.matrix.notation
 import data.fintype.card
 import group_theory.perm.fin
 import group_theory.perm.sign
@@ -719,7 +720,7 @@ det_is_empty
 /-- Determinant of 1x1 matrix -/
 lemma det_fin_one (A : matrix (fin 1) (fin 1) R) : det A = A 0 0  := det_unique A
 
-lemma det_fin_one_mk (a : R) : det ![![a]] = a := det_fin_one _
+lemma det_fin_one_of (a : R) : det !![a] = a := det_fin_one _
 
 /-- Determinant of 2x2 matrix -/
 lemma det_fin_two (A : matrix (fin 2) (fin 2) R) :
@@ -730,7 +731,7 @@ begin
 end
 
 @[simp] lemma det_fin_two_of (a b c d : R) :
-  matrix.det (of ![![a, b], ![c, d]]) = a * d - b * c :=
+  matrix.det !![a, b; c, d] = a * d - b * c :=
 det_fin_two _
 
 /-- Determinant of 3x3 matrix -/
diff --git a/src/linear_algebra/matrix/to_lin.lean b/src/linear_algebra/matrix/to_lin.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
 -/
 import data.matrix.block
+import data.matrix.notation
 import linear_algebra.matrix.finite_dimensional
 import linear_algebra.std_basis
 import ring_theory.algebra_tower
@@ -597,12 +598,12 @@ lemma matrix.to_lin_alg_equiv_mul (A B : matrix n n R) :
 by convert matrix.to_lin_mul v₁ v₁ v₁ A B
 
 @[simp] lemma matrix.to_lin_fin_two_prod_apply (a b c d : R) (x : R × R) :
-  matrix.to_lin (basis.fin_two_prod R) (basis.fin_two_prod R) ![![a, b], ![c, d]] x =
+  matrix.to_lin (basis.fin_two_prod R) (basis.fin_two_prod R) !![a, b; c, d] x =
     (a * x.fst + b * x.snd, c * x.fst + d * x.snd) :=
 by simp [matrix.to_lin_apply, matrix.mul_vec, matrix.dot_product]
 
 lemma matrix.to_lin_fin_two_prod (a b c d : R) :
-  matrix.to_lin (basis.fin_two_prod R) (basis.fin_two_prod R) ![![a, b], ![c, d]] =
+  matrix.to_lin (basis.fin_two_prod R) (basis.fin_two_prod R) !![a, b; c, d] =
     (a • linear_map.fst R R R + b • linear_map.snd R R R).prod
     (c • linear_map.fst R R R + d • linear_map.snd R R R) :=
 linear_map.ext $ matrix.to_lin_fin_two_prod_apply _ _ _ _
diff --git a/src/number_theory/modular.lean b/src/number_theory/modular.lean
@@ -95,7 +95,7 @@ lemma bottom_row_surj {R : Type*} [comm_ring R] :
     {cd | is_coprime (cd 0) (cd 1)} :=
 begin
   rintros cd ⟨b₀, a, gcd_eqn⟩,
-  let A := ![![a, -b₀], cd],
+  let A := of ![![a, -b₀], cd],
   have det_A_1 : det A = 1,
   { convert gcd_eqn,
     simp [A, det_fin_two, (by ring : a * (cd 1) + b₀ * (cd 0) = b₀ * (cd 0) + a * (cd 1))] },
@@ -192,9 +192,10 @@ theorem tendsto_lc_row0 {cd : fin 2 → ℤ} (hcd : is_coprime (cd 0) (cd 1)) :
   tendsto (λ g : {g : SL(2, ℤ) // ↑ₘg 1 = cd}, lc_row0 cd ↑(↑g : SL(2, ℝ)))
     cofinite (cocompact ℝ) :=
 begin
-  let mB : ℝ → (matrix (fin 2) (fin 2)  ℝ) := λ t, ![![t, (-(1:ℤ):ℝ)], coe ∘ cd],
+  let mB : ℝ → (matrix (fin 2) (fin 2) ℝ) := λ t, of ![![t, (-(1:ℤ):ℝ)], coe ∘ cd],
   have hmB : continuous mB,
-  { simp only [continuous_pi_iff, fin.forall_fin_two, mB, continuous_const, continuous_id',
+  { refine continuous_matrix _,
+    simp only [fin.forall_fin_two, mB, continuous_const, continuous_id', of_apply,
       cons_val_zero, cons_val_one, and_self ] },
   refine filter.tendsto.of_tendsto_comp _ (comap_cocompact_le hmB),
   let f₁ : SL(2, ℤ) → matrix (fin 2) (fin 2) ℝ :=
@@ -216,13 +217,13 @@ begin
       int.coe_cast_ring_hom, lc_row0_apply, function.comp_app, cons_val_zero, lc_row0_extend_apply,
       linear_map.general_linear_group.coe_fn_general_linear_equiv,
       general_linear_group.to_linear_apply, coe_plane_conformal_matrix, neg_neg, mul_vec_lin_apply,
-      cons_val_one, head_cons] },
+      cons_val_one, head_cons, of_apply] },
   { convert congr_arg (λ n : ℤ, (-n:ℝ)) g.det_coe.symm using 1,
     simp only [f₁, mul_vec, dot_product, fin.sum_univ_two, matrix.det_fin_two, function.comp_app,
       subtype.coe_mk, lc_row0_extend_apply, cons_val_zero,
       linear_map.general_linear_group.coe_fn_general_linear_equiv,
       general_linear_group.to_linear_apply, coe_plane_conformal_matrix, mul_vec_lin_apply,
-      cons_val_one, head_cons, map_apply, neg_mul, int.cast_sub, int.cast_mul, neg_sub],
+      cons_val_one, head_cons, map_apply, neg_mul, int.cast_sub, int.cast_mul, neg_sub, of_apply],
     ring },
   { refl }
 end
@@ -307,28 +308,26 @@ begin
 end
 
 /-- The matrix `T = [[1,1],[0,1]]` as an element of `SL(2,ℤ)` -/
-def T : SL(2,ℤ) := ⟨![![1, 1], ![0, 1]], by norm_num [matrix.det_fin_two]⟩
+def T : SL(2,ℤ) := ⟨!![1, 1; 0, 1], by norm_num [matrix.det_fin_two_of]⟩
 
 /-- The matrix `S = [[0,-1],[1,0]]` as an element of `SL(2,ℤ)` -/
-def S : SL(2,ℤ) := ⟨![![0, -1], ![1, 0]], by norm_num [matrix.det_fin_two]⟩
+def S : SL(2,ℤ) := ⟨!![0, -1; 1, 0], by norm_num [matrix.det_fin_two_of]⟩
 
-lemma coe_S : ↑ₘS = ![![0, -1], ![1, 0]] := rfl
+lemma coe_S : ↑ₘS = !![0, -1; 1, 0] := rfl
 
-lemma coe_T : ↑ₘT = ![![1, 1], ![0, 1]] := rfl
+lemma coe_T : ↑ₘT = !![1, 1; 0, 1] := rfl
 
-lemma coe_T_inv : ↑ₘ(T⁻¹) = ![![1, -1], ![0, 1]] := by simp [coe_inv, coe_T, adjugate_fin_two]
+lemma coe_T_inv : ↑ₘ(T⁻¹) = !![1, -1; 0, 1] := by simp [coe_inv, coe_T, adjugate_fin_two]
 
-lemma coe_T_zpow (n : ℤ) : ↑ₘ(T ^ n) = ![![1, n], ![0,1]] :=
+lemma coe_T_zpow (n : ℤ) : ↑ₘ(T ^ n) = !![1, n; 0, 1] :=
 begin
   induction n using int.induction_on with n h n h,
-  { ext i j, fin_cases i; fin_cases j;
-    simp, },
-  { rw [zpow_add, zpow_one, coe_mul, h, coe_T],
-    ext i j, fin_cases i; fin_cases j;
-    simp [matrix.mul_apply, fin.sum_univ_succ, add_comm (1 : ℤ)], },
-  { rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv],
-    ext i j, fin_cases i; fin_cases j;
-    simp [matrix.mul_apply, fin.sum_univ_succ, neg_add_eq_sub (1 : ℤ)], },
+  { rw [zpow_zero, coe_one, matrix.one_fin_two] },
+  { simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, matrix.mul_fin_two],
+    congrm !![_, _; _, _],
+    rw [mul_one, mul_one, add_comm] },
+  { simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, matrix.mul_fin_two],
+    congrm !![_, _; _, _]; ring },
 end
 
 @[simp] lemma T_pow_mul_apply_one (n : ℤ) (g : SL(2, ℤ)) : ↑ₘ(T ^ n * g) 1 = ↑ₘg 1 :=
@@ -379,8 +378,11 @@ lemma g_eq_of_c_eq_one (hc : ↑ₘg 1 0 = 1) :
 begin
   have hg := g.det_coe.symm,
   replace hg : ↑ₘg 0 1 = ↑ₘg 0 0 * ↑ₘg 1 1 - 1, { rw [det_fin_two, hc] at hg, linarith, },
-  ext i j, fin_cases i; fin_cases j;
-  simp [coe_S, coe_T_zpow, matrix.mul_apply, fin.sum_univ_succ, hg, hc],
+  refine subtype.ext _,
+  conv_lhs { rw matrix.eta_fin_two ↑ₘg },
+  rw [hc, hg],
+  simp only [coe_mul, coe_T_zpow, coe_S, mul_fin_two],
+  congrm !![_, _; _, _]; ring
 end
 
 /-- If `1 < |z|`, then `|S • z| < 1`. -/
diff --git a/src/topology/algebra/module/finite_dimension.lean b/src/topology/algebra/module/finite_dimension.lean
@@ -372,7 +372,7 @@ rfl
 
 lemma _root_.matrix.to_lin_fin_two_prod_to_continuous_linear_map (a b c d : 𝕜) :
   (matrix.to_lin (basis.fin_two_prod 𝕜) (basis.fin_two_prod 𝕜)
-      ![![a, b], ![c, d]]).to_continuous_linear_map =
+      !![a, b; c, d]).to_continuous_linear_map =
   (a • continuous_linear_map.fst 𝕜 𝕜 𝕜 + b • continuous_linear_map.snd 𝕜 𝕜 𝕜).prod
   (c • continuous_linear_map.fst 𝕜 𝕜 𝕜 + d • continuous_linear_map.snd 𝕜 𝕜 𝕜) :=
 continuous_linear_map.ext $ matrix.to_lin_fin_two_prod_apply _ _ _ _
