-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
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)
⊢ 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)
      _
have 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)
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)