bump to the latest mathlib4

Author: eric-wieser

.gitignore

@@ -1,2 +1,3 @@
 /build/
 /lake-packages
+lakefile.olean

MatrixCookbook/10FunctionsAndOperators.lean

@@ -38,8 +38,7 @@ variable [Field R]
 /-- The pdf does not mention `hx`! -/
 theorem eq_487 (X : Matrix m m R) (n : ℕ) (hx : (X - 1).det ≠ 0) :
     (X ^ n - 1) * (X - 1)⁻¹ = ∑ i in Finset.range n, X ^ i := by
-  rw [← geom_sum_mul X n, Matrix.mul_eq_mul, Matrix.mul_eq_mul,
-    mul_nonsing_inv_cancel_right _ _ hx.isUnit]
+  rw [← geom_sum_mul X n, mul_nonsing_inv_cancel_right _ _ hx.isUnit]
 
 /-! #### Taylor Expansion of Scalar Function -/
 
@@ -89,8 +88,8 @@ theorem eq_507 [Nontrivial m] [Nonempty n] :
   let A := stdBasisMatrix m1 n1 (1 : R)
   let B := stdBasisMatrix m2 n1 (1 : R)
   have := Matrix.ext_iff.mpr (h A B) (m1, m2) (n1, n1)
-  simpa [StdBasisMatrix.apply_same, StdBasisMatrix.apply_of_row_ne hm,
-    MulZeroClass.mul_zero, mul_one, one_ne_zero] using this
+  simp [StdBasisMatrix.apply_same, StdBasisMatrix.apply_of_row_ne hm,
+    mul_zero, mul_one, one_ne_zero] at this
 
 /-- Note we have to "cast" between the types -/
 theorem eq_508 (A : Matrix m n R) (B : Matrix r q R) (C : Matrix l p R) :
@@ -104,7 +103,7 @@ theorem eq_510 (A : Matrix m n R) (B : Matrix r q R) : (A ⊗ₖ B)ᵀ = Aᵀ 
   rw [kroneckerMap_transpose]
 
 theorem eq_511 (A : Matrix l m R) (B : Matrix p q R) (C : Matrix m n R) (D : Matrix q r R) :
-    A ⊗ₖ B ⬝ C ⊗ₖ D = (A ⬝ C) ⊗ₖ (B ⬝ D) := by rw [Matrix.mul_kronecker_mul]
+    A ⊗ₖ B * C ⊗ₖ D = (A * C) ⊗ₖ (B * D) := by rw [Matrix.mul_kronecker_mul]
 
 theorem eq_512 (A : Matrix m m R) (B : Matrix n n R) : (A ⊗ₖ B)⁻¹ = A⁻¹ ⊗ₖ B⁻¹ :=
   inv_kronecker _ _
@@ -129,13 +128,13 @@ def vec (A : Matrix m n R) : Matrix (n × m) Unit R :=
   col fun ij => A ij.2 ij.1
 
 theorem eq_520 (A : Matrix l m R) (X : Matrix m n R) (B : Matrix n p R) :
-    vec (A ⬝ X ⬝ B) = Bᵀ ⊗ₖ A ⬝ vec X := by
+    vec (A * X * B) = Bᵀ ⊗ₖ A * vec X := by
   ext ⟨k, l⟩
   simp_rw [vec, Matrix.mul_apply, Matrix.kroneckerMap_apply, col_apply, Finset.sum_mul,
     transpose_apply, ← Finset.univ_product_univ, Finset.sum_product, mul_right_comm _ _ (B _ _),
     mul_comm _ (B _ _)]
 
-theorem eq_521 (A B : Matrix m n R) : (Aᵀ ⬝ B).trace = ((vec A)ᵀ ⬝ vec B) () () := by
+theorem eq_521 (A B : Matrix m n R) : (Aᵀ * B).trace = ((vec A)ᵀ * vec B) () () := by
   simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, vec, transpose_apply, col_apply, ←
     Finset.univ_product_univ, Finset.sum_product]
 
@@ -147,7 +146,7 @@ theorem eq_523 (r : R) (A : Matrix m n R) : vec (r • A) = r • vec A :=
 
 -- note: `Bᵀ` is `B` in the PDF
 theorem eq_524 (a : m → R) (X : Matrix m n R) (B : Matrix n n R) (c : m → R) :
-    row a ⬝ X ⬝ B ⬝ Xᵀ ⬝ col c = (vec X)ᵀ ⬝ Bᵀ ⊗ₖ (col c ⬝ row a) ⬝ vec X := by
+    row a * X * B * Xᵀ * col c = (vec X)ᵀ * Bᵀ ⊗ₖ (col c * row a) * vec X := by
   -- not the proof from the book
   ext ⟨i, j⟩
   simp only [vec, Matrix.mul_apply, Finset.sum_mul, Finset.mul_sum, Matrix.kroneckerMap_apply,
@@ -167,19 +166,19 @@ theorem eq_524 (a : m → R) (X : Matrix m n R) (B : Matrix n n R) (c : m → R)
 /-! #### Examples -/
 
 
-theorem eq_525 (x : n → ℂ) : ‖(PiLp.equiv 1 _).symm x‖ = ∑ i, Complex.abs (x i) := by
-  simpa using PiLp.norm_eq_of_nat 1 Nat.cast_one.symm ((PiLp.equiv 1 _).symm x)
+theorem eq_525 (x : n → ℂ) : ‖(WithLp.equiv 1 _).symm x‖ = ∑ i, Complex.abs (x i) := by
+  simpa using PiLp.norm_eq_of_nat 1 Nat.cast_one.symm ((WithLp.equiv 1 _).symm x)
 
-theorem eq_526 (x : n → ℂ) : ↑(‖(PiLp.equiv 2 _).symm x‖ ^ 2) = star x ⬝ᵥ x := by
+theorem eq_526 (x : n → ℂ) : ↑(‖(WithLp.equiv 2 _).symm x‖ ^ 2) = star x ⬝ᵥ x := by
   rw [← EuclideanSpace.inner_piLp_equiv_symm, inner_self_eq_norm_sq_to_K, Complex.ofReal_pow]
   rfl  -- porting note: added
 
 theorem eq_527 (x : n → ℂ) (p : ℝ≥0∞) (h : 0 < p.toReal) :
-    ‖(PiLp.equiv p _).symm x‖ = (∑ i, Complex.abs (x i) ^ p.toReal) ^ (1 / p.toReal) := by
-  simp_rw [PiLp.norm_eq_sum h, PiLp.equiv_symm_apply, Complex.norm_eq_abs]
+    ‖(WithLp.equiv p _).symm x‖ = (∑ i, Complex.abs (x i) ^ p.toReal) ^ (1 / p.toReal) := by
+  simp_rw [PiLp.norm_eq_sum h, WithLp.equiv_symm_pi_apply, Complex.norm_eq_abs]
 
-theorem eq_528 (x : n → ℂ) : ‖(PiLp.equiv ∞ _).symm x‖ = ⨆ i, Complex.abs (x i) := by
-  simp_rw [PiLp.norm_eq_ciSup, PiLp.equiv_symm_apply, Complex.norm_eq_abs]
+theorem eq_528 (x : n → ℂ) : ‖(WithLp.equiv ∞ _).symm x‖ = ⨆ i, Complex.abs (x i) := by
+  simp_rw [PiLp.norm_eq_ciSup, WithLp.equiv_symm_pi_apply, Complex.norm_eq_abs]
 
 /-! ### Matrix Norms -/
 
@@ -224,7 +223,7 @@ theorem eq_534 [Nonempty n] : ‖(1 : Matrix n n ℝ)‖ = 1 :=
 theorem eq_535 (A : Matrix m n ℝ) (x : n → ℝ) : ‖A.mulVec x‖ ≤ ‖A‖ * ‖x‖ :=
   linfty_op_norm_mulVec _ _
 
-theorem eq_536 (A : Matrix m n ℝ) (B : Matrix n p ℝ) : ‖A ⬝ B‖ ≤ ‖A‖ * ‖B‖ :=
+theorem eq_536 (A : Matrix m n ℝ) (B : Matrix n p ℝ) : ‖A * B‖ ≤ ‖A‖ * ‖B‖ :=
   linfty_op_norm_mul _ _
 
 end
@@ -279,7 +278,7 @@ end
 -- lemma eq_544 : sorry := sorry
 -- lemma eq_545 : sorry := sorry
 theorem eq_546 (A : Matrix m n ℝ) (B : Matrix n r ℝ) :
-    rank A + rank B - Fintype.card n ≤ rank (A ⬝ B) ∧ rank (A ⬝ B) ≤ min (rank A) (rank B) :=
+    rank A + rank B - Fintype.card n ≤ rank (A * B) ∧ rank (A * B) ≤ min (rank A) (rank B) :=
   ⟨sorry, rank_mul_le _ _⟩
 
 /-! ### Integral Involving Dirac Delta Functions -/
@@ -291,10 +290,11 @@ theorem eq_546 (A : Matrix m n ℝ) (B : Matrix n r ℝ) :
 -- lemma eq_547 : sorry := sorry
 -- lemma eq_548 : sorry := sorry
 theorem eq_549 (A : Matrix m n ℝ) :
-    A.rank = Aᵀ.rank ∧ A.rank = (A ⬝ Aᵀ).rank ∧ A.rank = (Aᵀ ⬝ A).rank :=
+    A.rank = Aᵀ.rank ∧ A.rank = (A * Aᵀ).rank ∧ A.rank = (Aᵀ * A).rank :=
   ⟨A.rank_transpose.symm, A.rank_self_mul_transpose.symm, A.rank_transpose_mul_self.symm⟩
 
-theorem eq_550 (A : Matrix m m ℝ) : A.PosDef ↔ ∃ B : (Matrix m m ℝ)ˣ, A = ↑B * ↑Bᵀ :=
+theorem eq_550 (A : Matrix m m ℝ) :
+    A.PosDef ↔ ∃ B : (Matrix m m ℝ)ˣ, A = (↑B : Matrix m m ℝ) * ↑Bᵀ :=
   sorry
 
 end MatrixCookbook

MatrixCookbook/1Basic.lean

@@ -39,7 +39,7 @@ theorem eq_3 {A : Matrix m m R} : Aᵀ⁻¹ = A⁻¹ᵀ :=
 theorem eq_4 {A B : Matrix m n R} : (A + B)ᵀ = Aᵀ + Bᵀ :=
   transpose_add _ _
 
-theorem eq_5 {A : Matrix m n R} {B : Matrix n p R} : (A ⬝ B)ᵀ = Bᵀ ⬝ Aᵀ :=
+theorem eq_5 {A : Matrix m n R} {B : Matrix n p R} : (A * B)ᵀ = Bᵀ * Aᵀ :=
   transpose_mul _ _
 
 theorem eq_6 {l : List (Matrix m m R)} : l.prodᵀ = (l.map transpose).reverse.prod :=
@@ -51,7 +51,7 @@ theorem eq_7 [StarRing R] {A : Matrix m m R} : Aᴴ⁻¹ = A⁻¹ᴴ :=
 theorem eq_8 [StarRing R] {A B : Matrix m n R} : (A + B)ᴴ = Aᴴ + Bᴴ :=
   conjTranspose_add _ _
 
-theorem eq_9 [StarRing R] {A : Matrix m n R} {B : Matrix n p R} : (A ⬝ B)ᴴ = Bᴴ ⬝ Aᴴ :=
+theorem eq_9 [StarRing R] {A : Matrix m n R} {B : Matrix n p R} : (A * B)ᴴ = Bᴴ * Aᴴ :=
   conjTranspose_mul _ _
 
 theorem eq_10 [StarRing R] {l : List (Matrix m m R)} :
@@ -72,17 +72,17 @@ theorem eq_12 {A : Matrix m m R} [IsAlgClosed R] : trace A = A.charpoly.roots.su
 theorem eq_13 {A : Matrix m m R} : trace A = trace Aᵀ :=
   (Matrix.trace_transpose _).symm
 
-theorem eq_14 {A : Matrix m n R} {B : Matrix n m R} : trace (A ⬝ B) = trace (B ⬝ A) :=
+theorem eq_14 {A : Matrix m n R} {B : Matrix n m R} : trace (A * B) = trace (B * A) :=
   Matrix.trace_mul_comm _ _
 
 theorem eq_15 {A B : Matrix m m R} : trace (A + B) = trace A + trace B :=
   trace_add _ _
 
 theorem eq_16 {A : Matrix m n R} {B : Matrix n p R} {C : Matrix p m R} :
-    trace (A ⬝ B ⬝ C) = trace (B ⬝ C ⬝ A) :=
+    trace (A * B * C) = trace (B * C * A) :=
   (Matrix.trace_mul_cycle B C A).symm
 
-theorem eq_17 {a : m → R} : dotProduct a a = trace (col a ⬝ row a) :=
+theorem eq_17 {a : m → R} : dotProduct a a = trace (col a * row a) :=
   (Matrix.trace_col_mul_row _ _).symm
 
 end
@@ -109,7 +109,7 @@ theorem eq_22 {A : Matrix m m R} : det A⁻¹ = (det A)⁻¹ :=
 theorem eq_23 {A : Matrix m m R} (k : ℕ) : det (A ^ k) = det A ^ k :=
   det_pow _ _
 
-theorem eq_24 {u v : m → R} : det (1 + col u ⬝ row v) = 1 + dotProduct u v := by
+theorem eq_24 {u v : m → R} : det (1 + col u * row v) = 1 + dotProduct u v := by
   rw [det_one_add_col_mul_row u v, dotProduct_comm]
 
 theorem eq_25 {A : Matrix (Fin 2) (Fin 2) R} : det (1 + A) = 1 + det A + trace A := by
@@ -118,7 +118,7 @@ theorem eq_25 {A : Matrix (Fin 2) (Fin 2) R} : det (1 + A) = 1 + det A + trace A
 theorem eq_26 {A : Matrix (Fin 3) (Fin 3) R} [Invertible (2 : R)] :
     det (1 + A) = 1 + det A + trace A + ⅟ 2 * trace A ^ 2 - ⅟ 2 * trace (A ^ 2) := by
   apply mul_left_cancel₀ (isUnit_of_invertible (2 : R)).ne_zero
-  simp only [det_fin_three, trace_fin_three, pow_two, Matrix.mul_eq_mul, Matrix.mul_apply,
+  simp only [det_fin_three, trace_fin_three, pow_two, Matrix.mul_apply,
     Fin.sum_univ_succ, Matrix.one_apply]
   dsimp
   simp only [mul_add, mul_sub, mul_invOf_self_assoc]
@@ -173,7 +173,8 @@ theorem eq_30 {A : Matrix (Fin 2) (Fin 2) R} : trace A = A 0 0 + A 1 1 :=
 /-! Note: there are some non-numbered eigenvalue things here -/
 
 
-theorem eq_31 {A : Matrix (Fin 2) (Fin 2) R} : A⁻¹ = (det A)⁻¹ • !![A 1 1, -A 0 1; -A 1 0, A 0 0] := by rw [inv_def, adjugate_fin_two, Ring.inverse_eq_inv]
+theorem eq_31 {A : Matrix (Fin 2) (Fin 2) R} : A⁻¹ = (det A)⁻¹ • !![A 1 1, -A 0 1; -A 1 0, A 0 0] := by
+  rw [inv_def, adjugate_fin_two, Ring.inverse_eq_inv]
 
 end
 

MatrixCookbook/2Derivatives.lean

@@ -36,7 +36,7 @@ open Matrix
 /-! TODO: is this what is actually meant by `∂(XY) = (∂X)Y + X(∂Y)`? -/
 
 
-theorem eq_33 (A : Matrix m n R) : (deriv fun x : R => A) = 0 :=
+theorem eq_33 (A : Matrix m n R) : (deriv fun _ : R => A) = 0 :=
   deriv_const' _
 
 theorem eq_34 (c : R) (X : R → Matrix m n R) (hX : Differentiable R X) :
@@ -53,7 +53,7 @@ theorem eq_36 (X : R → Matrix m m R) (hX : Differentiable R X) :
 
 theorem eq_37 (X : R → Matrix m n R) (Y : R → Matrix n p R) (hX : Differentiable R X)
     (hY : Differentiable R Y) :
-    (deriv fun a => X a ⬝ Y a) = fun a => deriv X a ⬝ Y a + X a ⬝ deriv Y a :=
+    (deriv fun a => X a * Y a) = fun a => deriv X a * Y a + X a * deriv Y a :=
   funext fun a => ((hX a).hasDerivAt.matrix_mul (hY a).hasDerivAt).deriv
 
 theorem eq_38 (X Y : R → Matrix n p R) (hX : Differentiable R X) (hY : Differentiable R Y) :

MatrixCookbook/3Inverses.lean

@@ -102,41 +102,41 @@ theorem eq158 : sorry :=
 
 
 theorem eq_159 (B : Matrix n m ℂ) (C : Matrix m n ℂ) :
-    (A + B ⬝ C)⁻¹ = A⁻¹ - A⁻¹ ⬝ B ⬝ (1 + C ⬝ A⁻¹ ⬝ B)⁻¹ ⬝ C ⬝ A⁻¹ :=
+    (A + B * C)⁻¹ = A⁻¹ - A⁻¹ * B * (1 + C * A⁻¹ * B)⁻¹ * C * A⁻¹ :=
   sorry
 
 /-! ### Sherman-Morrison -/
 
 
 theorem eq_160 (b c : n → ℂ) :
-    (A + col b ⬝ row c)⁻¹ = A⁻¹ - (1 + c ⬝ᵥ A⁻¹.mulVec b)⁻¹ • A⁻¹ ⬝ (col b ⬝ row c) ⬝ A⁻¹ := by
+    (A + col b * row c)⁻¹ = A⁻¹ - (1 + c ⬝ᵥ A⁻¹.mulVec b)⁻¹ • A⁻¹ * (col b * row c) * A⁻¹ := by
   rw [eq_159, ← Matrix.mul_assoc _ (col b), Matrix.mul_assoc _ (row c), Matrix.mul_assoc _ (row c),
-    ← Matrix.mul_smul, Matrix.mul_assoc _ _ (row c ⬝ _)]
+    Matrix.smul_mul]
   congr
   sorry
 
 /-! ### The Searle Set of Identities -/
 
 
-theorem eq_161 : (1 + A⁻¹)⁻¹ = A ⬝ (A + 1)⁻¹ :=
+theorem eq_161 : (1 + A⁻¹)⁻¹ = A * (A + 1)⁻¹ :=
   sorry
 
-theorem eq_162 : (A + Bᵀ ⬝ B)⁻¹ ⬝ B = A⁻¹ ⬝ B ⬝ (1 + Bᵀ ⬝ A⁻¹ ⬝ B)⁻¹ :=
+theorem eq_162 : (A + Bᵀ * B)⁻¹ * B = A⁻¹ * B * (1 + Bᵀ * A⁻¹ * B)⁻¹ :=
   sorry
 
-theorem eq_163 : (A⁻¹ + B⁻¹)⁻¹ = A ⬝ (A + B)⁻¹ ⬝ B ∧ (A⁻¹ + B⁻¹)⁻¹ = B ⬝ (A + B)⁻¹ ⬝ A :=
+theorem eq_163 : (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A :=
   sorry
 
-theorem eq_164 : A - A ⬝ (A + B)⁻¹ ⬝ A = B - B ⬝ (A + B)⁻¹ ⬝ B :=
+theorem eq_164 : A - A * (A + B)⁻¹ * A = B - B * (A + B)⁻¹ * B :=
   sorry
 
-theorem eq_165 : A⁻¹ + B⁻¹ = A⁻¹ ⬝ (A + B)⁻¹ ⬝ B⁻¹ :=
+theorem eq_165 : A⁻¹ + B⁻¹ = A⁻¹ * (A + B)⁻¹ * B⁻¹ :=
   sorry
 
-theorem eq_166 : (1 + A ⬝ B)⁻¹ = 1 - A ⬝ (1 + B ⬝ A)⁻¹ ⬝ B :=
+theorem eq_166 : (1 + A * B)⁻¹ = 1 - A * (1 + B * A)⁻¹ * B :=
   sorry
 
-theorem eq_167 : (1 + A ⬝ B)⁻¹ ⬝ A = A ⬝ (1 + B ⬝ A)⁻¹ :=
+theorem eq_167 : (1 + A * B)⁻¹ * A = A * (1 + B * A)⁻¹ :=
   sorry
 
 /-! ### Rank-1 update of inverse of inner product -/
@@ -196,7 +196,7 @@ theorem eq183 : sorry :=
 /-! ## Implication on Inverses -/
 
 
-theorem eq_184 : (A + B)⁻¹ = A⁻¹ + B⁻¹ → A ⬝ B⁻¹ ⬝ A = B ⬝ A⁻¹ ⬝ B :=
+theorem eq_184 : (A + B)⁻¹ = A⁻¹ + B⁻¹ → A * B⁻¹ * A = B * A⁻¹ * B :=
   sorry
 
 /-! ### A PosDef identity -/

MatrixCookbook/5SolutionsAndDecompositions.lean

@@ -230,7 +230,7 @@ theorem eq301 : sorry :=
 
 
 theorem eq_302 {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef) :
-    A = LDL.lower hA ⬝ LDL.diag hA ⬝ (LDL.lower hA)ᴴ :=
+    A = LDL.lower hA * LDL.diag hA * (LDL.lower hA)ᴴ :=
   (LDL.lower_conj_diag hA).symm
 
 end MatrixCookbook

MatrixCookbook/9SpecialMatrices.lean

@@ -35,36 +35,38 @@ namespace MatrixCookbook
 
 
 theorem eq_397 (A₁₁ : Matrix m m R) (A₁₂ : Matrix m n R) (A₂₁ : Matrix n m R) (A₂₂ : Matrix n n R)
-    [Invertible A₂₂] : (fromBlocks A₁₁ A₁₂ A₂₁ A₂₂).det = A₂₂.det * (A₁₁ - A₁₂ ⬝ ⅟ A₂₂ ⬝ A₂₁).det :=
+    [Invertible A₂₂] : (fromBlocks A₁₁ A₁₂ A₂₁ A₂₂).det = A₂₂.det * (A₁₁ - A₁₂ * ⅟ A₂₂ * A₂₁).det :=
   det_fromBlocks₂₂ _ _ _ _
 
 theorem eq_398 (A₁₁ : Matrix m m R) (A₁₂ : Matrix m n R) (A₂₁ : Matrix n m R) (A₂₂ : Matrix n n R)
-    [Invertible A₁₁] : (fromBlocks A₁₁ A₁₂ A₂₁ A₂₂).det = A₁₁.det * (A₂₂ - A₂₁ ⬝ ⅟ A₁₁ ⬝ A₁₂).det :=
+    [Invertible A₁₁] : (fromBlocks A₁₁ A₁₂ A₂₁ A₂₂).det = A₁₁.det * (A₂₂ - A₂₁ * ⅟ A₁₁ * A₁₂).det :=
   det_fromBlocks₁₁ _ _ _ _
 
 /-! ### The Inverse -/
 
 
 /-- Eq 399 is the definition of `C₁`, this is the equation below it without `C₂` at all. -/
 theorem eq_399 (A₁₁ : Matrix m m R) (A₁₂ : Matrix m n R) (A₂₁ : Matrix n m R) (A₂₂ : Matrix n n R)
-    [Invertible A₂₂] [Invertible (A₁₁ - A₁₂ ⬝ ⅟ A₂₂ ⬝ A₂₁)] :
+    [Invertible A₂₂] [Invertible (A₁₁ - A₁₂ * ⅟ A₂₂ * A₂₁)] :
     (fromBlocks A₁₁ A₁₂ A₂₁ A₂₂)⁻¹ =
-      let C₁ := A₁₁ - A₁₂ ⬝ ⅟ A₂₂ ⬝ A₂₁
+      let C₁ := A₁₁ - A₁₂ * ⅟ A₂₂ * A₂₁
       let i : Invertible C₁ := ‹_›
-      fromBlocks (⅟ C₁) (-⅟ C₁ ⬝ A₁₂ ⬝ ⅟ A₂₂) (-⅟ A₂₂ ⬝ A₂₁ ⬝ ⅟ C₁)
-        (⅟ A₂₂ + ⅟ A₂₂ ⬝ A₂₁ ⬝ ⅟ C₁ ⬝ A₁₂ ⬝ ⅟ A₂₂) := by
+      fromBlocks
+        (⅟ C₁) (-(⅟ C₁ * A₁₂ * ⅟ A₂₂))
+        (-(⅟ A₂₂ * A₂₁ * ⅟ C₁)) (⅟ A₂₂ + ⅟ A₂₂ * A₂₁ * ⅟ C₁ * A₁₂ * ⅟ A₂₂) := by
   letI := fromBlocks₂₂Invertible A₁₁ A₁₂ A₂₁ A₂₂
   convert invOf_fromBlocks₂₂_eq A₁₁ A₁₂ A₂₁ A₂₂
   rw [invOf_eq_nonsing_inv]
 
 /-- Eq 400 is the definition of `C₂`,  this is the equation below it without `C₁` at all. -/
 theorem eq_400 (A₁₁ : Matrix m m R) (A₁₂ : Matrix m n R) (A₂₁ : Matrix n m R) (A₂₂ : Matrix n n R)
-    [Invertible A₁₁] [Invertible (A₂₂ - A₂₁ ⬝ ⅟ A₁₁ ⬝ A₁₂)] :
+    [Invertible A₁₁] [Invertible (A₂₂ - A₂₁ * ⅟ A₁₁ * A₁₂)] :
     (fromBlocks A₁₁ A₁₂ A₂₁ A₂₂)⁻¹ =
-      let C₂ := A₂₂ - A₂₁ ⬝ ⅟ A₁₁ ⬝ A₁₂
+      let C₂ := A₂₂ - A₂₁ * ⅟ A₁₁ * A₁₂
       let i : Invertible C₂ := ‹_›
-      fromBlocks (⅟ A₁₁ + ⅟ A₁₁ ⬝ A₁₂ ⬝ ⅟ C₂ ⬝ A₂₁ ⬝ ⅟ A₁₁) (-⅟ A₁₁ ⬝ A₁₂ ⬝ ⅟ C₂)
-        (-⅟ C₂ ⬝ A₂₁ ⬝ ⅟ A₁₁) (⅟ C₂) := by
+      fromBlocks
+        (⅟ A₁₁ + ⅟ A₁₁ * A₁₂ * ⅟ C₂ * A₂₁ * ⅟ A₁₁) (-(⅟ A₁₁ * A₁₂ * ⅟ C₂))
+        (-(⅟ C₂ * A₂₁ * ⅟ A₁₁)) (⅟ C₂) := by
   letI := fromBlocks₁₁Invertible A₁₁ A₁₂ A₂₁ A₂₂
   convert invOf_fromBlocks₁₁_eq A₁₁ A₁₂ A₂₁ A₂₂
   rw [invOf_eq_nonsing_inv]
@@ -161,19 +163,19 @@ theorem eq_421 [StarRing R] (hA : IsIdempotentElem A) : IsIdempotentElem (1 - A
   sorry
 
 theorem eq_422 (hA : IsIdempotentElem A) (hB : IsIdempotentElem B) (h : Commute A B) :
-    IsIdempotentElem (A ⬝ B) :=
+    IsIdempotentElem (A * B) :=
   hA.mul_of_commute h hB
 
 theorem eq_423 (hA : IsIdempotentElem A) : sorry = trace A :=
   sorry
 
-theorem eq_424 (hA : IsIdempotentElem A) : A ⬝ (1 - A) = 0 := by
+theorem eq_424 (hA : IsIdempotentElem A) : A * (1 - A) = 0 := by
   -- porting note: was `simp [mul_sub, ← Matrix.mul_eq_mul, hA.eq]`
-  rw [Matrix.mul_sub, Matrix.mul_one, ←Matrix.mul_eq_mul, hA.eq, sub_self]
+  rw [Matrix.mul_sub, Matrix.mul_one, hA.eq, sub_self]
 
-theorem eq_425 (hA : IsIdempotentElem A) : (1 - A) ⬝ A = 0 := by
+theorem eq_425 (hA : IsIdempotentElem A) : (1 - A) * A = 0 := by
    -- porting note: was `simp [sub_mul, ← Matrix.mul_eq_mul, hA.eq]`
-  rw [Matrix.sub_mul, Matrix.one_mul, ←Matrix.mul_eq_mul, hA.eq, sub_self]
+  rw [Matrix.sub_mul, Matrix.one_mul, hA.eq, sub_self]
 
 theorem eq426 : sorry :=
   sorry
@@ -453,7 +455,7 @@ theorem eq_477 :
       of ![(Pi.single 1 1 : Fin 3 → R), Pi.single 0 1, Pi.single 2 1] := by ext i j; fin_cases i <;> fin_cases j <;> rfl
 
 theorem eq_478 (e : Equiv.Perm m) :
-    e.toPEquiv.toMatrix ⬝ e.toPEquiv.toMatrixᵀ = (1 : Matrix m m R) := by
+    e.toPEquiv.toMatrix * e.toPEquiv.toMatrixᵀ = (1 : Matrix m m R) := by
   rw [← PEquiv.toMatrix_symm, ← PEquiv.toMatrix_trans, ← Equiv.toPEquiv_symm, ←
     Equiv.toPEquiv_trans, Equiv.self_trans_symm, Equiv.toPEquiv_refl, PEquiv.toMatrix_refl]
 

MatrixCookbook/ForMathlib/Analysis/Matrix.lean

@@ -47,7 +47,7 @@ theorem hasDerivAt_matrix {f : R → Matrix m n A} {r : R} {f' : Matrix m n A} :
 
 theorem HasDerivAt.matrix_mul {X : R → Matrix m n A} {Y : R → Matrix n p A} {X' : Matrix m n A}
     {Y' : Matrix n p A} {r : R} (hX : HasDerivAt X X' r) (hY : HasDerivAt Y Y' r) :
-    HasDerivAt (fun a => X a ⬝ Y a) (X' ⬝ Y r + X r ⬝ Y') r := by
+    HasDerivAt (fun a => X a * Y a) (X' * Y r + X r * Y') r := by
   rw [hasDerivAt_matrix] at hX hY ⊢
   intro i j
   simp only [mul_apply, Matrix.add_apply, ← Finset.sum_add_distrib]
@@ -84,8 +84,8 @@ theorem HasDerivAt.conjTranspose [StarRing R] [TrivialStar R] [StarAddMonoid A]
 theorem deriv_matrix (f : R → Matrix m n A) (r : R) (hX : DifferentiableAt R f r) :
     deriv f r = of fun i j => deriv (fun r => f r i j) r := by
   ext i j
-  rw [deriv_pi]
-  simp_rw [deriv_pi, of_apply]
+  rw [of_apply, deriv_pi]
+  dsimp only
   rw [deriv_pi]
   · intro i
     erw [differentiableAt_pi] at hX -- porting note: added

MatrixCookbook/Lib/TraceDetFinFour.lean

@@ -40,7 +40,7 @@ theorem trace_pow_two_fin_four (A : Matrix (Fin 4) (Fin 4) R) :
             2 * A 1 2 * A 2 1 +
           2 * A 1 3 * A 3 1 +
         2 * A 2 3 * A 3 2 := by
-  simp_rw [Matrix.trace_fin_four, pow_two, mul_eq_mul, mul_apply, Fin.sum_univ_four]
+  simp_rw [Matrix.trace_fin_four, pow_two, mul_apply, Fin.sum_univ_four]
   ring
 
 -- porting note: added
@@ -68,7 +68,7 @@ theorem trace_pow_three_fin_four (A : Matrix (Fin 4) (Fin 4) R) :
             A 3 2 * (A 0 3 * A 2 0 + A 1 3 * A 2 1 + A 2 2 * A 2 3 + A 2 3 * A 3 3) +
           A 1 3 * (A 0 1 * A 3 0 + A 1 1 * A 3 1 + A 2 1 * A 3 2 + A 3 1 * A 3 3) +
         A 2 3 * (A 0 2 * A 3 0 + A 1 2 * A 3 1 + A 2 2 * A 3 2 + A 3 2 * A 3 3) := by
-  simp_rw [Matrix.trace_fin_four, pow_three, mul_eq_mul, mul_apply, Fin.sum_univ_four]
+  simp_rw [Matrix.trace_fin_four, pow_three, mul_apply, Fin.sum_univ_four]
   ring
 
 theorem det_one_add_fin_four (A : Matrix (Fin 4) (Fin 4) R) :