-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_5 : Invertible A
rw :
  (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1 *
          fromBlocks A 0 0 (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) *
        fromBlocks 1 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) 0 1).det =
    A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
rw₁ :
  (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1 *
          fromBlocks A 0 0 (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B)).det *
      det (fromBlocks 1 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) 0 1) =
    A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
rw₂ :
  det (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1) *
        (fromBlocks A 0 0 (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B)).det *
      det (fromBlocks 1 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) 0 1) =
    A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
rw₃ :
  det (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1) *
        (A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det) *
      det (fromBlocks 1 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) 0 1) =
    A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
rw₄ :
  det (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1) *
        (A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det) *
      HMul.hMul (α := α) (det.{u_4, u_2} (n := m) 1) (det.{u_4, u_3} (n := n) 1) =
    A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
rw₅ :
  HMul.hMul (α := α) (det.{u_4, u_2} (n := m) 1) (det.{u_4, u_3} (n := n) 1) *
        (A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det) *
      HMul.hMul (α := α) (det.{u_4, u_2} (n := m) 1) (det.{u_4, u_3} (n := n) 1) =
    A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
rw₆ :
  HMul.hMul (α := α) 1 (det.{u_4, u_3} (n := n) 1) *
        (A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det) *
      HMul.hMul (α := α) 1 (det.{u_4, u_3} (n := n) 1) =
    A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
rw₇ :
  HMul.hMul (α := α) 1 1 * (A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det) *
      HMul.hMul (α := α) 1 1 =
    A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
⊢ (fromBlocks A B C D).det = A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
have rw₈ : 1 * (A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det) * 1 =
  A.det * (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B).det
Tactic: rw [fromBlocks_eq_of_invertible₁₁ (A := A), det_mul, det_mul, det_fromBlocks_zero₂₁,
    det_fromBlocks_zero₂₁, det_fromBlocks_zero₁₂, det_one, det_one, one_mul, one_mul, mul_one]