Theorem: MatrixCookbook.eq_160 (MatrixCookbook/3Inverses.lean)

State before:
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⁻¹
Tactic:
rw [eq_159, ← Matrix.mul_assoc _ (col b), Matrix.mul_assoc _ (row c), Matrix.mul_assoc _ (row c),
  Matrix.smul_mul]
State after:
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⁻¹)

State before:
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⁻¹)
Tactic:
congr
State after:
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)

State before:
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)
Tactic:
sorry
State after:
no goals