Theorem: MatrixCookbook.eq_258 (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)⁻¹ =
    (A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
      (1 - t • ((B - t • A) * (A + t • B)⁻¹).map Complex.ofReal' -
        (t • 1 + (B - t • A) * (A + t • B)⁻¹).map fun x => x • I)
Tactic:
rw [eq_257 _ _ 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' *
        (1 - ((B - t • A) * (A + t • B)⁻¹).map fun x => x • I)) =
    (A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
      (1 - t • ((B - t • A) * (A + t • B)⁻¹).map Complex.ofReal' -
        (t • 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' *
        (1 - ((B - t • A) * (A + t • B)⁻¹).map fun x => x • I)) =
    (A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
      (1 - t • ((B - t • A) * (A + t • B)⁻¹).map Complex.ofReal' -
        (t • 1 + (B - t • A) * (A + t • B)⁻¹).map fun x => x • I)
Tactic:
sorry
State after:
no goals