Theorem: MatrixCookbook.eq_256 (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' -
          ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (B - t • A) * (A + t • B)).map fun x => x • I)⁻¹
Tactic:
rw [eq_255 _ _ 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).map Complex.ofReal' + (B - t • A).map fun x => x • I)⁻¹ =
    (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)⁻¹

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).map Complex.ofReal' + (B - t • A).map fun x => x • I)⁻¹ =
    (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)⁻¹
Tactic:
sorry
State after:
no goals