Theorem: MatrixCookbook.eq_259 (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))⁻¹ * (1 - t • ((B - t • A) * (A + t • B)⁻¹))).map
        Complex.ofReal' -
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (t • 1 + (B - t • A) * (A + t • B)⁻¹)).map fun x =>
        x • I
Tactic:
rw [eq_258 _ _ h, mul_sub]
State after:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ ((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') -
      (A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (t • 1 + (B - t • A) * (A + t • B)⁻¹).map fun x => x • I) =
    ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (1 - t • ((B - t • A) * (A + t • B)⁻¹))).map
        Complex.ofReal' -
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (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)
⊢ ((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') -
      (A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (t • 1 + (B - t • A) * (A + t • B)⁻¹).map fun x => x • I) =
    ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (1 - t • ((B - t • A) * (A + t • B)⁻¹))).map
        Complex.ofReal' -
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (t • 1 + (B - t • A) * (A + t • B)⁻¹)).map fun x =>
        x • I
Tactic:
sorry
State after:
no goals