-- Module: Mathlib.Data.Matrix.Invertible
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
inst_4 : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst_5 : Invertible A
inst_6 : Invertible C
inst_7 :
  Invertible
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
      V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
simp_rw :
  (A + U * C * V) *
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                  V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                _ *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) =
    A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                  V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                _ *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ +
      (U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                  V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                _ *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)
simp_rw₁ :
  A *
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                    V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                  _ *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) +
      U * C * V *
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                    V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                  _ *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) =
    A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                  V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                _ *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ +
      (U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                  V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                _ *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)
simp_rw₂ :
  A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        A *
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                    V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                  _ *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) +
      (U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        U * C * V *
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                    V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                  _ *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)) =
    A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                  V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                _ *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ +
      (U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                  V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                _ *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)
⊢ (A + U * C * V) *
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                  V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                _ *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) =
    A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
          A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                    V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                  _ *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ +
        U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
              _ *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _

Tactic:
simp_rw [add_sub_assoc, add_mul, mul_sub, Matrix.mul_assoc]

Premises used: add_sub_assoc, add_mul, mul_sub, Matrix.mul_assoc