-- 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)
rw :
  1 -
          @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 *
                  @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 =
    1 + @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 _ * 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 _ * 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 _ * 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 _ *
            U *
          C *
        V =
    1 + @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 _ * 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)

Tactic:
rw [invOf_mul_self, Matrix.invOf_mul_cancel_right]

Premises used: invOf_mul_self, Matrix.invOf_mul_cancel_right