congr
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⁻¹)
case e_a.e_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⁻¹ * col b * (1 + row c * A⁻¹ * col b)⁻¹ = (1 + c ⬝ᵥ A⁻¹ *ᵥ b)⁻¹ • (A⁻¹ * col b)