awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ A.det • b ᵥ* A⁻¹ = (Aᵀ.cramer : (a : n → α) → n → α) b
have rw₄ : Eq (α := n → α) ((Aᵀ.cramer : (a : n → α) → n → α) b : n → α) ((Aᵀ.cramer : (a : n → α) → n → α) b : n → α)
Tactic: rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
    Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ 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
have rw : Eq (α := Matrix n n α)
  ((A * @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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ 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
have 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
Tactic: rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
⊢ 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
have rw₂ : Eq (α := Matrix n n α) 1 1
Tactic: rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (hypothesis)
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)
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
          _)
        (⇑e₂.symm : (a : m) → n) (⇑e₁.symm : (a : m) → n) =
    1
have 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)
Tactic: have : A = (A.submatrix e₁ e₂).submatrix e₁.symm e₂.symm := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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)
have 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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
have 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: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) _)
      (⇑e₂.symm : (a : m) → n) (⇑e₁.symm : (a : m) → n)
have 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: congr
      rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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)
have 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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)
        (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
          _)
        (⇑e₂.symm : (a : m) → n) (⇑e₁.symm : (a : m) → n) =
    1
have conv : HMul.hMul (α := Matrix m m α)
    (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))
    (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)) =
  1
Tactic: conv in _ * _ =>
      congr
      rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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)
⊢ HMul.hMul (α := Matrix m m α)
      (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))
      (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)) =
    1
have rw : Eq (α := Matrix m m α)
  ((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))
          _)).submatrix
    (⇑e₁.symm : (a : m) → n) (⇑e₁.symm : (a : m) → n))
  1
Tactic: rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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)
rw :
  Eq (α := Matrix m m α)
    ((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))
            _)).submatrix
      (⇑e₁.symm : (a : m) → n) (⇑e₁.symm : (a : m) → n))
    1
⊢ HMul.hMul (α := Matrix m m α)
      (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))
      (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)) =
    1
have rw₁ : Eq (α := Matrix m m α)
  (submatrix.{v, u, u', u', u} (m := n) (n := n) 1 (⇑e₁.symm : (a : m) → n) (⇑e₁.symm : (a : m) → n)) 1
Tactic: rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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)
rw :
  Eq (α := Matrix m m α)
    ((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))
            _)).submatrix
      (⇑e₁.symm : (a : m) → n) (⇑e₁.symm : (a : m) → n))
    1
rw₁ :
  Eq (α := Matrix m m α)
    (submatrix.{v, u, u', u', u} (m := n) (n := n) 1 (⇑e₁.symm : (a : m) → n) (⇑e₁.symm : (a : m) → n)) 1
⊢ HMul.hMul (α := Matrix m m α)
      (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))
      (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)) =
    1
have rw₂ : Eq (α := Matrix m m α) 1 1
Tactic: rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 m m α
e₁ e₂ : n ≃ m
inst_5 : Invertible A
inst_6 : Invertible (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
⊢ Eq (α := Matrix n n α)
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) _)
    ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _).submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
have rw : Eq (α := Matrix n n α)
  (@Invertible.invOf _ MulOne.toMul MulOne.toOne (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) _)
  ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _).submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
Tactic: rw [@Invertible.congr _ _ _ _ _ (submatrixEquivInvertible A e₁ e₂) rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 m m α
e₁ e₂ : n ≃ m
⊢ Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
have pos : ∀ (h : IsUnit A),
  Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
Tactic: by_cases h : IsUnit A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 m m α
e₁ e₂ : n ≃ m
pos :
  ∀ (h : IsUnit A),
    Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
      (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
⊢ Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
have neg : ∀ (h : ¬IsUnit A),
  Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
Tactic: by_cases h : IsUnit A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 m m α
e₁ e₂ : n ≃ m
h : IsUnit A
⊢ Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
have pos : ∀ (val : Invertible A),
  Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
Tactic: cases h.nonempty_invertible
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val : Invertible A
this : Invertible (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) :=
  A.submatrixEquivInvertible e₁ e₂
⊢ Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
have pos : Eq (α := Matrix n n α)
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) _)
  (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
Tactic: rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val : Invertible A
this : Invertible (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) :=
  A.submatrixEquivInvertible e₁ e₂
pos :
  Eq (α := Matrix n n α)
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) _)
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
⊢ Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
have pos₁ : Eq (α := Matrix n n α)
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) _)
  ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _).submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
Tactic: rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val : Invertible A
this : Invertible (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) :=
  A.submatrixEquivInvertible e₁ e₂
pos :
  Eq (α := Matrix n n α)
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) _)
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
pos₁ :
  Eq (α := Matrix n n α)
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) _)
    ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _).submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
⊢ Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
have pos₂ : Eq (α := Matrix n n α)
  ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _).submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
  ((@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _).submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
Tactic: rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (hypothesis)
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 m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
⊢ Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
have this : ¬IsUnit (M := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
Tactic: have := (isUnit_submatrix_equiv e₁ e₂).not.mpr h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
this : ¬IsUnit (M := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
⊢ Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
have neg : Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹ʳ
  (A⁻¹ʳ.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
Tactic: simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this,
      submatrix_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
this : ¬IsUnit (M := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
neg :
  Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹ʳ
    (A⁻¹ʳ.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
⊢ Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
have neg₁ : Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹ʳ
  (submatrix.{v, u', u, u, u'} (m := m) (n := m) 0 (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
Tactic: simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this,
      submatrix_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
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 m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
this : ¬IsUnit (M := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))
neg :
  Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹ʳ
    (A⁻¹ʳ.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
neg₁ :
  Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹ʳ
    (submatrix.{v, u', u, u, u'} (m := m) (n := m) 0 (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
⊢ Eq (α := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))⁻¹
    (A⁻¹.submatrix (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
have neg₂ : Eq (α := Matrix n n α) 0 (submatrix.{v, u', u, u, u'} (m := m) (n := m) 0 (⇑e₂ : (a : n) → m) (⇑e₁ : (a : n) → m))
Tactic: simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this,
      submatrix_zero, Pi.zero_apply]