Equation 158 (#16)

Adapted from #3, using new results that have since been upstreamed to mathlib

Co-authored-by: MohanadAhmed <[email protected]>

MatrixCookbook/3Inverses.lean

@@ -104,10 +104,26 @@ theorem eq_157 (A : Matrix n n ℂ) (B : Matrix m m ℂ) (U : Matrix n m ℂ) (V
   Matrix.add_mul_mul_inv_eq_sub _ _ _ _ hA hB h
 
 open scoped ComplexOrder in
+/-- Note that this has been generalized from the `ℝ`/`ᵀ` in the source to `ℂ`/`ᴴ`. -/
 theorem eq_158 (P : Matrix n n ℂ) (R : Matrix m m ℂ) (B : Matrix m n ℂ)
     (hP : P.PosDef) (hR : R.PosDef) :
-    (P + Bᵀ * R * B)⁻¹ * Bᵀ * R⁻¹ = P * Bᵀ * (B*P⁻¹*Bᵀ + R)⁻¹ := by
-  sorry
+    (P⁻¹ + Bᴴ * R⁻¹ * B)⁻¹ * Bᴴ * R⁻¹ = P * Bᴴ * (B * P * Bᴴ + R)⁻¹ := by
+  letI : Invertible P := hP.isUnit.invertible
+  letI : Invertible R := hR.isUnit.invertible
+  letI : Invertible (R + B*P*Bᴴ) :=
+    (hR.add_posSemidef <| hP.posSemidef.mul_mul_conjTranspose_same B).isUnit.invertible
+  rw [Matrix.add_mul_mul_inv_eq_sub, add_comm _ R]
+  · simp_rw [Matrix.inv_inv_of_invertible, Matrix.sub_mul, Matrix.mul_assoc, ← Matrix.mul_sub]
+    congr 2
+    simp_rw [← Matrix.mul_assoc]
+    refine hR.isUnit.isRegular.right ?_
+    simp_rw [Matrix.sub_mul, sub_eq_iff_eq_add, Matrix.mul_assoc, ← Matrix.mul_add,
+      ← Matrix.mul_assoc, Matrix.inv_mul_cancel_right_of_invertible,
+      Matrix.inv_mul_of_invertible]
+  · simpa only [isUnit_nonsing_inv_iff] using hP.isUnit
+  · simpa only [isUnit_nonsing_inv_iff] using hR.isUnit
+  · simp_rw [Matrix.inv_inv_of_invertible]
+    exact isUnit_of_invertible _
 
 /-! ### The Kailath Variant -/