-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq l
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible D
inst_8 : Invertible (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C)
convert_7 :
  fromBlocks
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _)
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _ *
            B *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _))
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
            (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _))
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ +
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _ *
            B *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) =
    fromBlocks 1 0 (-(1 * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) * 1)) 1 *
      (fromBlocks
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
            (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _)
          (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _ *
                0 *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _))
          0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
        fromBlocks 1 (-(1 * (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) * 1)) 0 1)
⊢ fromBlocks
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _)
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _ *
            B *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _))
      (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
            (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _))
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ +
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) _ *
            B *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne
      (fromBlocks 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 0 1 *
          fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D *
        fromBlocks 1 0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 1)
      _

Tactic:
change
      _ =
        fromBlocks 1 0 (-(1 * (⅟D * C) * 1)) 1 *
          (fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * 0 * ⅟D)) 0 (⅟D) *
            fromBlocks 1 (-(1 * (B * ⅟D) * 1)) 0 1)

Premises used: Matrix.fromBlocks, HMul.hMul, HSub.hSub, Invertible.invOf, OfNat.ofNat, Neg.neg