awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U =
    U * C *
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
        V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)

Tactic:
simp only [Matrix.mul_add, Matrix.mul_invOf_cancel_right, ← Matrix.mul_assoc]

Premises used: Matrix.mul_assoc, Matrix.mul_invOf_cancel_right, Matrix.mul_add
-- 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 + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    1
⊢ 1 + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      U * C *
              (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one 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 _ =
    1

Tactic:
rw [Matrix.mul_invOf_cancel_right]

Premises used: Matrix.mul_invOf_cancel_right
-- 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)
⊢ 1 + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    1

Tactic:
abel
-- 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)
⊢ 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)

Tactic:
abel
-- 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)
⊢ @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 _ * 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:
simp_rw [Matrix.mul_assoc]

Premises used: Matrix.mul_assoc
-- 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)
⊢ 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 + 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)
                _ *
            (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
              V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) *
          C *
        V

Tactic:
simp only [Matrix.mul_add, Matrix.add_mul, ← Matrix.mul_assoc,
        Matrix.invOf_mul_cancel_right]

Premises used: Matrix.mul_assoc, Matrix.add_mul, Matrix.mul_add, Matrix.invOf_mul_cancel_right
-- 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 * C * V -
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C * V =
    1
⊢ 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)
                _ *
            (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
              V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) *
          C *
        V =
    1

Tactic:
rw [Matrix.invOf_mul_cancel_right]

Premises used: Matrix.invOf_mul_cancel_right
-- 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)
⊢ 1 + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C * V -
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C * V =
    1

Tactic:
abel
-- 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)
inst_8 : Invertible (A + U * C * V)
this : Invertible (A + U * C * V) := A.invertibleAddMulMul U C V
⊢ @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A + U * C * V) _ =
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A + U * C * V) _

Tactic:
(rfl : ⅟(A + U * C * V) = _)

Premises used: rfl
-- 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)
inst_8 : Invertible (A + U * C * V)
this : Invertible (A + U * C * V) := A.invertibleAddMulMul U C 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 _

Tactic:
convert! (rfl : ⅟(A + U * C * V) = _)

Premises used: rfl
-- 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 + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
simp :
  1 + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      (A *
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
                C *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) +
        U * C * V *
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
                C *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)) =
    1
⊢ (A + U * C * V) *
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              C *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) =
    1

Tactic:
simp only [Matrix.mul_sub, Matrix.add_mul, mul_invOf_self']

Premises used: Matrix.mul_sub, Matrix.add_mul, mul_invOf_self'
-- 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 + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
rw :
  U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    A *
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              C *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) +
      U * C * V *
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              C *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)
⊢ 1 + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      (A *
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
                C *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) +
        U * C * V *
          (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
                C *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)) =
    1

Tactic:
rw [add_sub_assoc, add_eq_left, sub_eq_zero]

Premises used: add_sub_assoc, sub_eq_zero, add_eq_left
-- 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 + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
simp :
  U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    (U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) * C *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
          C *
        V *
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _
⊢ U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    U * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            C *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ +
      U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            C *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _

Tactic:
simp only [← Matrix.add_mul]

Premises used: Matrix.add_mul
-- 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 + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
e_a :
  U =
    (U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) * C *
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _
⊢ U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
    (U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) * C *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
          C *
        V *
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _

Tactic:
congr
-- 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 + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
e_a :
  U * (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) =
    (U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) * C
⊢ U =
    (U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) * C *
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
        (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _

Tactic:
rw [← Matrix.mul_right_eq_iff_eq_mul_invOf]

Premises used: Matrix.mul_right_eq_iff_eq_mul_invOf
-- 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 + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ U * (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) =
    (U + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U) * C

Tactic:
simp only [Matrix.add_mul, Matrix.mul_add, Matrix.mul_assoc]

Premises used: Matrix.mul_assoc, Matrix.add_mul, Matrix.mul_add
-- 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 + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
simp :
  1 -
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
                C *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
          A +
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * (U * C * V) -
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                    (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
                C *
              V *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ *
          (U * C * V)) =
    1
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
                @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                  (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
              C *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) *
      (A + U * C * V) =
    1

Tactic:
simp only [Matrix.mul_add, Matrix.sub_mul, invOf_mul_self']

Premises used: Matrix.sub_mul, Matrix.mul_add, invOf_mul_self'