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✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible A
hA : A.IsHermitian
⊢ star (x ⊕ᵥ y) ᵥ* A.fromBlocks B B.conjTranspose D ⬝ᵥ (x ⊕ᵥ y) =
    star (x + (A⁻¹ * B).mulVec y) ᵥ* A ⬝ᵥ (x + (A⁻¹ * B).mulVec y) + star y ᵥ* (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ y
Tactic:
simp [Function.star_sum_elim, fromBlocks_mulVec, vecMul_fromBlocks, add_vecMul,
  dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, vecMul_mulVec, hA.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✝² : DecidableEq m
inst✝¹ : Fintype n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
x : m → 𝕜
y : n → 𝕜
inst✝ : Invertible A
hA : A.IsHermitian
⊢ star x ᵥ* A ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) =
    star x ᵥ* A ⬝ᵥ x + star y ᵥ* B.conjTranspose ⬝ᵥ x +
        (star x ᵥ* B ⬝ᵥ y + star y ᵥ* (B.conjTranspose * (A⁻¹ * B)) ⬝ᵥ y) +
      (star y ᵥ* D ⬝ᵥ y - star y ᵥ* (B.conjTranspose * (A⁻¹ * B)) ⬝ᵥ y)

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