rw [eq_159, ← Matrix.mul_assoc _ (col b), Matrix.mul_assoc _ (row c), Matrix.mul_assoc _ (row c),
  Matrix.smul_mul]
m : Type ?u.18898
n : Type u_1
p : Type ?u.18904
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
b c : n → ℂ
⊢ (A + col b * row c)⁻¹ = A⁻¹ - (1 + c ⬝ᵥ A⁻¹ *ᵥ b)⁻¹ • A⁻¹ * (col b * row c) * A⁻¹
m : Type ?u.18898
n : Type u_1
p : Type ?u.18904
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
b c : n → ℂ
⊢ A⁻¹ - A⁻¹ * col b * (1 + row c * A⁻¹ * col b)⁻¹ * (row c * A⁻¹) =
    A⁻¹ - (1 + c ⬝ᵥ A⁻¹ *ᵥ b)⁻¹ • (A⁻¹ * col b) * (row c * A⁻¹)