awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val : Invertible (diagonal v)
val_1 : Invertible v
pos : @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne (diagonal v) _ = diagonal v⁻¹ʳ
pos₁ :
  @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne (diagonal v) _ =
    diagonal (@Invertible.invOf _ MulZeroClass.toMul MulOne.toOne v _)
pos₂ pos₃ :
  diagonal (@Invertible.invOf _ (Pi.instMul (M := fun (a : n) ↦ α)) (Pi.instOne (M := fun (a : n) ↦ α)) v _) =
    diagonal (@Invertible.invOf _ MulZeroClass.toMul MulOne.toOne v _)
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ

Tactic:
rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_eq]

Premises used: Ring.inverse_invertible, Matrix.invOf_diagonal_eq
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
v : n → α
h : ¬IsUnit v
⊢ ¬IsUnit (diagonal v)

Tactic:
have := isUnit_diagonal.not.mpr h
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
v : n → α
h : ¬IsUnit v
this : ¬IsUnit (diagonal v)
neg : (diagonal v)⁻¹ʳ = diagonal 0
neg₁ : (diagonal v)⁻¹ʳ = diagonal fun (x : n) ↦ 0
neg₂ : (diagonal v)⁻¹ʳ = 0
neg₃ neg₄ : Eq (α := Matrix n n α) 0 0
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ

Tactic:
rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this]

Premises used: Matrix.diagonal_zero, Pi.zero_def, Ring.inverse_non_unit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Subsingleton m
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
rw : Eq (α := Matrix m m α) (diagonal fun (x : m) ↦ A.det⁻¹ʳ) (diagonal fun (i : m) ↦ (A i i)⁻¹ʳ)
⊢ A⁻¹ = diagonal fun (i : m) ↦ (A i i)⁻¹ʳ

Tactic:
rw [inv_def, adjugate_subsingleton, smul_one_eq_diagonal]

Premises used: Matrix.smul_one_eq_diagonal, Matrix.inv_def, Matrix.adjugate_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Subsingleton m
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
h : ∀ (i : m), A.det = A i i
⊢ Eq (α := Matrix m m α) (diagonal fun (x : m) ↦ A.det⁻¹ʳ) (diagonal fun (i : m) ↦ (A i i)⁻¹ʳ)

Tactic:
congr! with i
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Subsingleton m
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
i : m
⊢ A.det = A i i

Tactic:
det_eq_elem_of_subsingleton _ _

Premises used: Matrix.det_eq_elem_of_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Subsingleton m
inst_2 : Fintype m
inst_3 : DecidableEq m
A : Matrix m m α
i : m
⊢ A.det = A i i

Tactic:
exact det_eq_elem_of_subsingleton _ _

Premises used: Matrix.det_eq_elem_of_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
obtain : ∀ (val : Invertible A), (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
obtain ⟨_⟩ := hA.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val : Invertible A
obtain : ∀ (val : Invertible C), (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
obtain ⟨_⟩ := hC.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val : Invertible A
val_1 : Invertible C
obtain : ∀ (iAC : Invertible (C⁻¹ + V * A⁻¹ * U)), (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
obtain ⟨iAC⟩ := hAC.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val : Invertible A
val_1 : Invertible C
iAC : Invertible (C⁻¹ + V * A⁻¹ * U)
simp :
  ∀
    (iAC :
      Invertible
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
          V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)),
    (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
simp only [← invOf_eq_nonsing_inv] at iAC

Premises used: Matrix.invOf_eq_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val : Invertible A
val_1 : Invertible C
iAC :
  Invertible
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
      V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
this : Invertible (A + U * C * V) := A.invertibleAddMulMul U C V
simp :
  @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)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
simp only [← invOf_eq_nonsing_inv]

Premises used: Matrix.invOf_eq_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val : Invertible A
val_1 : Invertible C
iAC :
  Invertible
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
      V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
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:
apply invOf_add_mul_mul

Premises used: Matrix.invOf_add_mul_mul
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
obtain : ∀ (val : Invertible A), (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹

Tactic:
obtain ⟨_⟩ := hA.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
val : Invertible A
obtain :
  ∀ (ih : Invertible (C + C * V * A⁻¹ * U * C)),
    (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹

Tactic:
obtain ⟨ih⟩ := h.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
val : Invertible A
ih : Invertible (C + C * V * A⁻¹ * U * C)
simp :
  ∀ (ih : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)),
    (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹

Tactic:
simp only [← invOf_eq_nonsing_inv] at ih

Premises used: Matrix.invOf_eq_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
val : Invertible A
ih : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
this : Invertible (A + U * C * V) := A.invertibleAddMulMul' U C V
simp :
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (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 _
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹

Tactic:
simp only [← invOf_eq_nonsing_inv]

Premises used: Matrix.invOf_eq_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
val : Invertible A
ih : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
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 * C *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
                (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
            C *
          V *
        @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _

Tactic:
apply invOf_add_mul_mul'

Premises used: Matrix.invOf_add_mul_mul'
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
pos : ∀ (h : IsUnit A.det), A⁻¹⁻¹⁻¹ = A⁻¹
neg : ∀ (h : ¬IsUnit A.det), A⁻¹⁻¹⁻¹ = A⁻¹
⊢ A⁻¹⁻¹⁻¹ = A⁻¹

Tactic:
by_cases h : IsUnit A.det

Premises used: IsUnit, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
pos pos₁ : A⁻¹ = A⁻¹
⊢ A⁻¹⁻¹⁻¹ = A⁻¹

Tactic:
rw [nonsing_inv_nonsing_inv _ h]

Premises used: Matrix.nonsing_inv_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹⁻¹⁻¹ = A⁻¹

Tactic:
simp [nonsing_inv_apply_not_isUnit _ h]

Premises used: Matrix.nonsing_inv_apply_not_isUnit
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
h : IsUnit A ↔ IsUnit B
⊢ A⁻¹ + B⁻¹ = A⁻¹ * (A + B) * B⁻¹

Tactic:
simpa only [nonsing_inv_eq_ringInverse] using Ring.inverse_add_inverse h

Premises used: Ring.inverse_add_inverse, Matrix.nonsing_inv_eq_ringInverse
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
h : IsUnit A ↔ IsUnit B
⊢ A⁻¹ - B⁻¹ = A⁻¹ * (B - A) * B⁻¹

Tactic:
simpa only [nonsing_inv_eq_ringInverse] using Ring.inverse_sub_inverse h

Premises used: Ring.inverse_sub_inverse, Matrix.nonsing_inv_eq_ringInverse
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
simp : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • B.adjugate * A.det⁻¹ʳ • A.adjugate
⊢ (A * B)⁻¹ = B⁻¹ * A⁻¹

Tactic:
simp only [inv_def]

Premises used: Matrix.inv_def
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
rw : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • (B.adjugate * A.det⁻¹ʳ • A.adjugate)
rw₁ : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • A.det⁻¹ʳ • (B.adjugate * A.adjugate)
rw₂ : (A * B).det⁻¹ʳ • (A * B).adjugate = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
rw₃ : (A.det * B.det)⁻¹ʳ • (A * B).adjugate = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
rw₄ : (A.det * B.det)⁻¹ʳ • (B.adjugate * A.adjugate) = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
rw₅ rw₆ : (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate) = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • B.adjugate * A.det⁻¹ʳ • A.adjugate

Tactic:
rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
    Ring.mul_inverse_rev]

Premises used: Matrix.mul_smul, smul_smul, Matrix.adjugate_mul_distrib, Matrix.det_mul, Matrix.smul_mul, Ring.mul_inverse_rev
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
rw : Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod (List.map Inv.inv []))
rw₁ : Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod [])
rw₂ : Eq (α := Matrix n n α) 1⁻¹ 1
rw₃ rw₄ : Eq (α := Matrix n n α) 1 1
⊢ Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod (List.map Inv.inv (List.reverse [])))

Tactic:
rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]

Premises used: inv_one, List.prod_nil, List.reverse_nil, List.map_nil
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
Xs : List (Matrix n n α)
rw : (A :: Xs).prod⁻¹ = (List.map Inv.inv (Xs.reverse.concat A)).prod
rw₁ : (A :: Xs).prod⁻¹ = ((List.map Inv.inv Xs.reverse).concat A⁻¹).prod
rw₂ : (A :: Xs).prod⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
rw₃ : (A * Xs.prod)⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
rw₄ : Xs.prod⁻¹ * A⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
rw₅ rw₆ : (List.map Inv.inv Xs.reverse).prod * A⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
⊢ (A :: Xs).prod⁻¹ = (List.map Inv.inv (A :: Xs).reverse).prod

Tactic:
rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons,
      mul_inv_rev, list_prod_inv_reverse Xs]

Premises used: List.prod_concat, Matrix.mul_inv_rev, List.reverse_cons', List.map_concat, List.prod_cons
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
rw : A.det • A⁻¹ *ᵥ b = A.adjugate *ᵥ b
rw₁ : A.det • ((↑h.unit⁻¹ : α) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
rw₂ : (A.det • (↑h.unit⁻¹ : α) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
rw₃ : ((A.det * (↑h.unit⁻¹ : α)) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
rw₄ : HSMul.hSMul (α := α) 1 A.adjugate *ᵥ b = A.adjugate *ᵥ b
rw₅ rw₆ : A.adjugate *ᵥ b = A.adjugate *ᵥ b
⊢ A.det • A⁻¹ *ᵥ b = (A.cramer : (a : n → α) → n → α) b

Tactic:
rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec, smul_smul,
    h.mul_val_inv, one_smul]

Premises used: IsUnit.mul_val_inv, smul_smul, Matrix.nonsing_inv_apply, one_smul, Matrix.smul_mulVec, Matrix.cramer_eq_adjugate_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
rw : A.det • b ᵥ* A⁻¹ᵀᵀ = (Aᵀ.cramer : (a : n → α) → n → α) b
rw₁ : A.det • A⁻¹ᵀ *ᵥ b = (Aᵀ.cramer : (a : n → α) → n → α) b
rw₂ : A.det • Aᵀ⁻¹ *ᵥ b = (Aᵀ.cramer : (a : n → α) → n → α) b
rw₃ : Aᵀ.det • Aᵀ⁻¹ *ᵥ b = (Aᵀ.cramer : (a : n → α) → n → α) b
rw₄ rw₅ : Eq (α := n → α) ((Aᵀ.cramer : (a : n → α) → n → α) b : n → α) ((Aᵀ.cramer : (a : n → α) → n → α) b : n → α)
⊢ A.det • b ᵥ* A⁻¹ = (Aᵀ.cramer : (a : n → α) → n → α) b

Tactic:
rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
    Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]

Premises used: Matrix.det_smul_inv_mulVec_eq_cramer, Matrix.det_transpose, Matrix.transpose_transpose, Matrix.isUnit_det_transpose, Inv.inv, Matrix.transpose, Matrix.transpose_nonsing_inv, Matrix.vecMul_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A_1 B : Matrix n n α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst_5 : Invertible A
rw :
  Eq (α := Matrix n n α)
    ((A * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _).submatrix (⇑e₁ : (a : n) → m)
      (⇑e₁ : (a : n) → m))
    1
rw₁ : Eq (α := Matrix n n α) (submatrix.{v, u', u, u, u'} (m := m) (n := m) 1 (⇑e₁ : (a : n) → m) (⇑e₁ : (a : n) → m)) 1
rw₂ rw₃ : Eq (α := Matrix n n α) 1 1
⊢ HMul.hMul (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
      ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _).submatrix (⇑e₂ : (a : n) → m)
        (⇑e₁ : (a : n) → m)) =
    1

Tactic:
rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]

Premises used: mul_invOf_self, Matrix.submatrix_one_equiv, Matrix.submatrix_mul_equiv
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A_1 B : Matrix n n α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst_5 : Invertible (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
⊢ A =
    submatrix.{v, u, u', u', u} (m := n) (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
      (⇑e₁.symm : (a : m) → n) (⇑e₂.symm : (a : m) → n)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A_1 B : Matrix n n α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst_5 : Invertible (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
⊢ A =
    submatrix.{v, u, u', u', u} (m := n) (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
      (⇑e₁.symm : (a : m) → n) (⇑e₂.symm : (a : m) → n)

Tactic:
have : A = (A.submatrix e₁ e₂).submatrix e₁.symm e₂.symm := by simp
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A_1 B : Matrix n n α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst_5 : Invertible (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
this :
  A =
    submatrix.{v, u, u', u', u} (m := n) (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
      (⇑e₁.symm : (a : m) → n) (⇑e₂.symm : (a : m) → n)
a : A
a₁ :
  submatrix.{v, u, u', u', u} (m := n) (n := n)
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) _)
    (⇑e₂.symm : (a : m) → n) (⇑e₁.symm : (a : m) → n)
| A *
    submatrix.{v, u, u', u', u} (m := n) (n := n)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) _)
      (⇑e₂.symm : (a : m) → n) (⇑e₁.symm : (a : m) → n)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A_1 B : Matrix n n α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst_5 : Invertible (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
this :
  A =
    submatrix.{v, u, u', u', u} (m := n) (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
      (⇑e₁.symm : (a : m) → n) (⇑e₂.symm : (a : m) → n)
a :
  submatrix.{v, u, u', u', u} (m := n) (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
    (⇑e₁.symm : (a : m) → n) (⇑e₂.symm : (a : m) → n)
| A

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A_1 B : Matrix n n α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst_5 : Invertible (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
this :
  A =
    submatrix.{v, u, u', u', u} (m := n) (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
      (⇑e₁.symm : (a : m) → n) (⇑e₂.symm : (a : m) → n)
a :
  submatrix.{v, u, u', u', u} (m := n) (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
    (⇑e₁.symm : (a : m) → n) (⇑e₂.symm : (a : m) → n)
a₁ :
  submatrix.{v, u, u', u', u} (m := n) (n := n)
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) _)
    (⇑e₂.symm : (a : m) → n) (⇑e₁.symm : (a : m) → n)
| A *
    submatrix.{v, u, u', u', u} (m := n) (n := n)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) _)
      (⇑e₂.symm : (a : m) → n) (⇑e₁.symm : (a : m) → n)

Tactic:
congr
      rw [this]