-- Lean 4 proof step from Mathlib.Data.Matrix.Invertible (goal)
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)
_ :
  (@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 + 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
⊢ (@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 + U * C * V) =
    1
have _₁ : @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: calc
    (⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)*(A + U*C*V)
    _ = ⅟A*A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*A + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V := by
      simp_rw [add_sub_assoc, _root_.mul_add, _root_.sub_mul, Matrix.mul_assoc]
    _ = (1 + ⅟A*U*C*V) - (⅟A*U*⅟(⅟C + V*⅟A*U)*V + ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V) := by
      rw [invOf_mul_self, Matrix.invOf_mul_cancel_right]
      abel
    _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(V + V*⅟A*U*C*V) := by
      rw [sub_right_inj, Matrix.mul_add]
      simp_rw [Matrix.mul_assoc]
    _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(⅟C + V*⅟A*U)*C*V := by
      simp only [Matrix.mul_add, Matrix.add_mul, ← Matrix.mul_assoc,
        Matrix.invOf_mul_cancel_right]
    _ = 1 := by
      rw [Matrix.invOf_mul_cancel_right]
      abel