-- 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 α
D : Matrix n n α
inst_7 : Invertible A
inst_8 : Invertible D
simp_rw :
  fromBlocks
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          0)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          D)
      (0 * A + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * 0)
      (0 * B + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
    1
simp_rw₁ :
  fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A + 0)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          D)
      (0 * A + 0) (0 * B + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
    1
simp_rw₂ :
  fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A + 0)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          D)
      (HAdd.hAdd (α := Matrix n m α) 0 0) (0 + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
    1
simp_rw₃ :
  fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A + 0)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          D)
      0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
    1
simp_rw₄ :
  fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          D)
      0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
    1
simp_rw₅ :
  fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ *
            D))
      0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
    1
⊢ fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)
        (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _))
        0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
      fromBlocks A B 0 D =
    1
have simp_rw₆ : Eq (α := Matrix (m ⊕ n) (m ⊕ n) α)
  (fromBlocks 1
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
      -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ *
          D))
    0 1)
  1
Tactic: simp_rw [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, zero_add, add_zero,
      Matrix.neg_mul, invOf_mul_self, Matrix.invOf_mul_cancel_right, add_neg_cancel,
      fromBlocks_one]