sorry
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)⁻¹
no goals