awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst_3 : Invertible C
rw : B = A * C ↔ A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _
⊢ A * C = B ↔ A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _
have rw₁ : B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = A ↔
  A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _
Tactic: rw [eq_comm, ← Matrix.mul_invOf_eq_iff_eq_mul_right, eq_comm]
-- 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 : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst_3 : Invertible C
rw : B = A * C ↔ A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _
rw₁ :
  B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ = A ↔
    A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _
⊢ A * C = B ↔ A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _
have rw₂ : A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ ↔
  A = B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _
Tactic: rw [eq_comm, ← Matrix.mul_invOf_eq_iff_eq_mul_right, eq_comm]
-- 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 : Semiring α
inst_3 : StarRing α
A : Matrix n n α
inst_4 : Invertible Aᴴ
⊢ Invertible A
have rw : Invertible (star Aᴴ)
Tactic: rw [← conjTranspose_conjTranspose A, ← star_eq_conjTranspose]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible A
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ * Aᵀ = 1
have rw : (A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ = 1
Tactic: rw [← transpose_mul, mul_invOf_self, transpose_one]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible A
rw : (A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ = 1
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ * Aᵀ = 1
have rw₁ : Eq (α := Matrix n n α) 1ᵀ 1
Tactic: rw [← transpose_mul, mul_invOf_self, transpose_one]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible A
rw : (A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ = 1
rw₁ : Eq (α := Matrix n n α) 1ᵀ 1
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ * Aᵀ = 1
have rw₂ : Eq (α := Matrix n n α) 1 1
Tactic: rw [← transpose_mul, mul_invOf_self, transpose_one]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible A
⊢ Aᵀ * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ = 1
have rw : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)ᵀ = 1
Tactic: rw [← transpose_mul, invOf_mul_self, transpose_one]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible A
rw : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)ᵀ = 1
⊢ Aᵀ * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ = 1
have rw₁ : Eq (α := Matrix n n α) 1ᵀ 1
Tactic: rw [← transpose_mul, invOf_mul_self, transpose_one]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible A
rw : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A)ᵀ = 1
rw₁ : Eq (α := Matrix n n α) 1ᵀ 1
⊢ Aᵀ * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)ᵀ = 1
have rw₂ : Eq (α := Matrix n n α) 1 1
Tactic: rw [← transpose_mul, invOf_mul_self, transpose_one]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible Aᵀ
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A = 1
have rw : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A = 1ᵀ
Tactic: rw [← transpose_one, ← mul_invOf_self Aᵀ, transpose_mul, transpose_transpose]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible Aᵀ
rw : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A = 1ᵀ
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A = 1
have rw₁ : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A =
  (Aᵀ * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ
Tactic: rw [← transpose_one, ← mul_invOf_self Aᵀ, transpose_mul, transpose_transpose]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible Aᵀ
rw : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A = 1ᵀ
rw₁ :
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A =
    (Aᵀ * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A = 1
have rw₂ : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A =
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * Aᵀᵀ
Tactic: rw [← transpose_one, ← mul_invOf_self Aᵀ, transpose_mul, transpose_transpose]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible Aᵀ
rw : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A = 1ᵀ
rw₁ :
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A =
    (Aᵀ * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ
rw₂ :
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A =
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * Aᵀᵀ
⊢ (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A = 1
have rw₃ : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A =
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ * A
Tactic: rw [← transpose_one, ← mul_invOf_self Aᵀ, transpose_mul, transpose_transpose]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible Aᵀ
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ = 1
have rw : A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ = 1ᵀ
Tactic: rw [← transpose_one, ← invOf_mul_self Aᵀ, transpose_mul, transpose_transpose]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible Aᵀ
rw : A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ = 1ᵀ
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ = 1
have rw₁ : A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ =
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _ * Aᵀ)ᵀ
Tactic: rw [← transpose_one, ← invOf_mul_self Aᵀ, transpose_mul, transpose_transpose]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible Aᵀ
rw : A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ = 1ᵀ
rw₁ :
  A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ =
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _ * Aᵀ)ᵀ
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ = 1
have rw₂ : A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ =
  Aᵀᵀ * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ
Tactic: rw [← transpose_one, ← invOf_mul_self Aᵀ, transpose_mul, transpose_transpose]
-- 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 : CommSemiring α
A : Matrix n n α
inst_3 : Invertible Aᵀ
rw : A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ = 1ᵀ
rw₁ :
  A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ =
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _ * Aᵀ)ᵀ
rw₂ :
  A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ =
    Aᵀᵀ * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ
⊢ A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ = 1
have rw₃ : A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ =
  A * (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one Aᵀ _)ᵀ
Tactic: rw [← transpose_one, ← invOf_mul_self Aᵀ, transpose_mul, transpose_transpose]
-- 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)
⊢ 1 + 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 _ * U *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
                  V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
                _ *
            V *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) =
    1 + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      (U + 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 _
have rw : 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 + 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: rw [sub_right_inj, Matrix.add_mul, Matrix.add_mul, Matrix.add_mul]
-- 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)
⊢ 1 + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
      (U + 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 _ =
    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 _
have e_a : 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: congr
-- 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)
⊢ 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
have rw : 1 + U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
    U * C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ =
  1
Tactic: rw [Matrix.mul_invOf_cancel_right]
-- 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)
⊢ (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 _) =
    1
have _ : (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: calc
    (A + U*C*V)*(⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)
    _ = A*⅟A - A*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A + U*C*V*⅟A - U*C*V*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by
      simp_rw [add_sub_assoc, add_mul, mul_sub, Matrix.mul_assoc]
    _ = (1 + U*C*V*⅟A) - (U*⅟(⅟C + V*⅟A*U)*V*⅟A + U*C*V*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) := by
      rw [mul_invOf_self, Matrix.one_mul]
      abel
    _ = 1 + U*C*V*⅟A - (U + U*C*V*⅟A*U)*⅟(⅟C + V*⅟A*U)*V*⅟A := by
      rw [sub_right_inj, Matrix.add_mul, Matrix.add_mul, Matrix.add_mul]
    _ = 1 + U*C*V*⅟A - U*C*(⅟C + V*⅟A*U)*⅟(⅟C + V*⅟A*U)*V*⅟A := by
      congr
      simp only [Matrix.mul_add, Matrix.mul_invOf_cancel_right, ← Matrix.mul_assoc]
    _ = 1 := by
      rw [Matrix.mul_invOf_cancel_right]
      abel
-- 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)
⊢ 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
have rw : 1 + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C * V -
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C * V =
  1
Tactic: rw [Matrix.invOf_mul_cancel_right]
-- 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 + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
⊢ (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
have 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
Tactic: simp only [Matrix.mul_sub, Matrix.add_mul, mul_invOf_self']