Theorem: MatrixCookbook.eq_257 (MatrixCookbook/4ComplexMatrices.lean)

State before:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (A.map Complex.ofReal' + B.map fun x => x • I)⁻¹ =
    (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (1 - ((B - t • A) * (A + t • B)⁻¹).map fun x => x • I))
Tactic:
rw [eq_256 _ _ h]
State after:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' -
          ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (B - t • A) * (A + t • B)).map fun x =>
            x • I)⁻¹ =
    (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (1 - ((B - t • A) * (A + t • B)⁻¹).map fun x => x • I))

State before:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' -
          ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (B - t • A) * (A + t • B)).map fun x =>
            x • I)⁻¹ =
    (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (1 - ((B - t • A) * (A + t • B)⁻¹).map fun x => x • I))
Tactic:
sorry
State after:
no goals