Theorem: Matrix.schur_complement_eq₂₂ (CvxLean/Lib/Math/SchurComplement.lean)

State before:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible D
hD : D.IsHermitian
⊢ star (x ⊕ᵥ y) ᵥ* A.fromBlocks B B.conjTranspose D ⬝ᵥ (x ⊕ᵥ y) =
    star ((D⁻¹ * B.conjTranspose).mulVec x + y) ᵥ* D ⬝ᵥ ((D⁻¹ * B.conjTranspose).mulVec x + y) +
      star x ᵥ* (A - B * D⁻¹ * B.conjTranspose) ⬝ᵥ x
Tactic:
simp [Function.star_sum_elim, fromBlocks_mulVec, vecMul_fromBlocks, add_vecMul,
  dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, vecMul_mulVec, hD.eq,
  conjTranspose_nonsing_inv, star_mulVec]
State after:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible D
hD : D.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* (B * (D⁻¹ * B.conjTranspose)) ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x +
        (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) +
      (star x ᵥ* A ⬝ᵥ x - star x ᵥ* (B * (D⁻¹ * B.conjTranspose)) ⬝ᵥ x)

State before:
n : Type u_2
m : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible D
hD : D.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* (B * (D⁻¹ * B.conjTranspose)) ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x +
        (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) +
      (star x ᵥ* A ⬝ᵥ x - star x ᵥ* (B * (D⁻¹ * B.conjTranspose)) ⬝ᵥ x)
Tactic:
abel
State after:
no goals