awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
A : Matrix n n α
inst_3 : Invertible A
B C : Matrix m n α
h : B * A⁻¹ = C
rw : B = B * A⁻¹ * A
⊢ B = C * A
have rw₁ : B = B
Tactic: rw [← h, inv_mul_cancel_right_of_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 α
A : Matrix n n α
inst_3 : Invertible A
B C : Matrix m n α
h : B = C * A
⊢ B * A⁻¹ = C
have rw : C * A * A⁻¹ = C
Tactic: rw [h, mul_inv_cancel_right_of_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 α
A : Matrix n n α
inst_3 : Invertible A
B C : Matrix m n α
h : B = C * A
rw : C * A * A⁻¹ = C
⊢ B * A⁻¹ = C
have rw₁ : C = C
Tactic: rw [h, mul_inv_cancel_right_of_invertible]
-- 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 α
inst_3 : Invertible A
u v : n → α
hM : u = A *ᵥ v
⊢ A⁻¹ *ᵥ u = v
have rw : A⁻¹ *ᵥ A *ᵥ v = v
Tactic: rw [hM, Matrix.mulVec_mulVec, Matrix.inv_mul_of_invertible, Matrix.one_mulVec]
-- 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 α
inst_3 : Invertible A
u v : n → α
hM : u = A *ᵥ v
rw : A⁻¹ *ᵥ A *ᵥ v = v
⊢ A⁻¹ *ᵥ u = v
have rw₁ : (A⁻¹ * A) *ᵥ v = v
Tactic: rw [hM, Matrix.mulVec_mulVec, Matrix.inv_mul_of_invertible, Matrix.one_mulVec]
-- 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 α
inst_3 : Invertible A
u v : n → α
hM : u = A *ᵥ v
rw : A⁻¹ *ᵥ A *ᵥ v = v
rw₁ : (A⁻¹ * A) *ᵥ v = v
⊢ A⁻¹ *ᵥ u = v
have rw₂ : 1 *ᵥ v = v
Tactic: rw [hM, Matrix.mulVec_mulVec, Matrix.inv_mul_of_invertible, Matrix.one_mulVec]
-- 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 α
inst_3 : Invertible A
u v : n → α
hM : u = A *ᵥ v
rw : A⁻¹ *ᵥ A *ᵥ v = v
rw₁ : (A⁻¹ * A) *ᵥ v = v
rw₂ : 1 *ᵥ v = v
⊢ A⁻¹ *ᵥ u = v
have rw₃ : v = v
Tactic: rw [hM, Matrix.mulVec_mulVec, Matrix.inv_mul_of_invertible, Matrix.one_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
⊢ (Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A) ↔ ∃ (B : Matrix n m R), B * A = 1
have intro : ∀ (val : Fintype n), (Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A) ↔ ∃ (B : Matrix n m R), B * A = 1
Tactic: cases nonempty_fintype n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
val : Fintype n
⊢ (Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A) ↔ ∃ (B : Matrix n m R), B * A = 1
have intro : ∀ (h : Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A), ∃ (B : Matrix n m R), B * A = 1
Tactic: refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨y ᵥ* B, by simp [hBA]⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
val : Fintype n
h : Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A
⊢ ∃ (B : Matrix n m R), B * A = 1
have intro : ∀ (rows : n → m → R)
  (hrows : ∀ (x : n), Eq (α := n → R) ((fun (v : m → R) ↦ v ᵥ* A) (rows x)) (Pi.single (M := fun (a : n) ↦ R) x 1)),
  ∃ (B : Matrix n m R), B * A = 1
Tactic: choose rows hrows using (h <| Pi.single · 1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
val : Fintype n
h : Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), Eq (α := n → R) ((fun (v : m → R) ↦ v ᵥ* A) (rows x)) (Pi.single (M := fun (a : n) ↦ R) x 1)
⊢ ∃ (B : Matrix n m R), B * A = 1
have intro : ∀ (i j : n), HMul.hMul (α := Matrix n m R) ((of : (a : n → m → R) → Matrix n m R) rows : Matrix n m R) A i j = 1 i j
Tactic: refine ⟨Matrix.of rows, Matrix.ext fun i j => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Finite n
A : Matrix m n R
val : Fintype n
h : Function.Surjective (β := n → R) fun (v : m → R) ↦ v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), Eq (α := n → R) ((fun (v : m → R) ↦ v ᵥ* A) (rows x)) (Pi.single (M := fun (a : n) ↦ R) x 1)
i j : n
⊢ HMul.hMul (α := Matrix n m R) ((of : (a : n → m → R) → Matrix n m R) rows : Matrix n m R) A i j = 1 i j
have intro : ((of : (a : n → m → R) → Matrix n m R) rows i ᵥ* A) j = (fun (v : m → R) ↦ v ᵥ* A) (rows i) j
Tactic: rw [mul_apply_eq_vecMul, one_eq_pi_single, ← hrows]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
⊢ Function.Surjective A.mulVec ↔ ∃ (B : Matrix n m R), A * B = 1
have intro : ∀ (val : Fintype m), Function.Surjective A.mulVec ↔ ∃ (B : Matrix n m R), A * B = 1
Tactic: cases nonempty_fintype m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
val : Fintype m
⊢ Function.Surjective A.mulVec ↔ ∃ (B : Matrix n m R), A * B = 1
have intro : ∀ (h : Function.Surjective A.mulVec), ∃ (B : Matrix n m R), A * B = 1
Tactic: refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B *ᵥ y, by simp [hBA]⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
val : Fintype m
h : Function.Surjective A.mulVec
⊢ ∃ (B : Matrix n m R), A * B = 1
have intro : ∀ (cols : m → n → R) (hcols : ∀ (x : m), A *ᵥ cols x = Pi.single (M := fun (a : m) ↦ R) x 1),
  ∃ (B : Matrix n m R), A * B = 1
Tactic: choose cols hcols using (h <| Pi.single · 1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
val : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single (M := fun (a : m) ↦ R) x 1
⊢ ∃ (B : Matrix n m R), A * B = 1
have intro : ∀ (i j : m), HMul.hMul (β := Matrix n m R) A ((of : (a : m → n → R) → Matrix m n R) cols)ᵀ i j = 1 i j
Tactic: refine ⟨(Matrix.of cols)ᵀ, Matrix.ext fun i j ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq m
inst_2 : Finite m
inst_3 : Fintype n
A : Matrix m n R
val : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single (M := fun (a : m) ↦ R) x 1
i j : m
⊢ HMul.hMul (β := Matrix n m R) A ((of : (a : m → n → R) → Matrix m n R) cols)ᵀ i j = 1 i j
have intro : HMul.hMul (β := Matrix n m R) A ((of : (a : m → n → R) → Matrix m n R) cols)ᵀ i j = (A *ᵥ cols j) i
Tactic: rw [one_eq_pi_single, Pi.single_comm, ← hcols j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
R : Type u_2
inst_1 : CommRing R
inst_2 : Fintype m
A : Matrix m m R
⊢ (Function.Surjective (β := m → R) fun (v : m → R) ↦ v ᵥ* A) ↔ IsUnit A
have rw : (∃ (B : Matrix m m R), B * A = 1) ↔ IsUnit A
Tactic: rw [vecMul_surjective_iff_exists_left_inverse, isUnit_iff_exists_inv']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
R : Type u_2
inst_1 : CommRing R
inst_2 : Fintype m
A : Matrix m m R
rw : (∃ (B : Matrix m m R), B * A = 1) ↔ IsUnit A
⊢ (Function.Surjective (β := m → R) fun (v : m → R) ↦ v ᵥ* A) ↔ IsUnit A
have rw₁ : (∃ (B : Matrix m m R), B * A = 1) ↔ ∃ (b : Matrix m m R), b * A = 1
Tactic: rw [vecMul_surjective_iff_exists_left_inverse, isUnit_iff_exists_inv']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
R : Type u_2
inst_1 : CommRing R
inst_2 : Fintype m
A : Matrix m m R
⊢ Function.Surjective A.mulVec ↔ IsUnit A
have rw : (∃ (B : Matrix m m R), A * B = 1) ↔ IsUnit A
Tactic: rw [mulVec_surjective_iff_exists_right_inverse, isUnit_iff_exists_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
R : Type u_2
inst_1 : CommRing R
inst_2 : Fintype m
A : Matrix m m R
rw : (∃ (B : Matrix m m R), A * B = 1) ↔ IsUnit A
⊢ Function.Surjective A.mulVec ↔ IsUnit A
have rw₁ : (∃ (B : Matrix m m R), A * B = 1) ↔ ∃ (b : Matrix m m R), A * b = 1
Tactic: rw [mulVec_surjective_iff_exists_right_inverse, isUnit_iff_exists_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
⊢ (Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A) ↔ IsUnit A
have refine_1 : ∀ (h : Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A), IsUnit A
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
refine_1 : ∀ (h : Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A), IsUnit A
⊢ (Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A) ↔ IsUnit A
have refine_2 : ∀ (h : IsUnit A), Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
h : Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
⊢ IsUnit A
have refine_1 : Function.Surjective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
Tactic: rw [← vecMul_surjective_iff_isUnit]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
⊢ Function.Injective A.mulVec ↔ IsUnit A
have rw : Function.Injective A.mulVec ↔ Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* Aᵀ
Tactic: rw [← isUnit_transpose, ← vecMul_injective_iff_isUnit]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
⊢ LinearIndependent K A.row ↔ IsUnit A
have rw : LinearIndependent K Aᵀ.col ↔ IsUnit A
Tactic: rw [← col_transpose, ← mulVec_injective_iff, ← coe_mulVecLin, mulVecLin_transpose,
    ← vecMul_injective_iff_isUnit, coe_vecMulLinear]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
rw : LinearIndependent K Aᵀ.col ↔ IsUnit A
⊢ LinearIndependent K A.row ↔ IsUnit A
have rw₁ : Function.Injective Aᵀ.mulVec ↔ IsUnit A
Tactic: rw [← col_transpose, ← mulVec_injective_iff, ← coe_mulVecLin, mulVecLin_transpose,
    ← vecMul_injective_iff_isUnit, coe_vecMulLinear]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
rw : LinearIndependent K Aᵀ.col ↔ IsUnit A
rw₁ : Function.Injective Aᵀ.mulVec ↔ IsUnit A
⊢ LinearIndependent K A.row ↔ IsUnit A
have rw₂ : Function.Injective (α := m → K) (β := m → K) (⇑Aᵀ.mulVecLin : (a : m → K) → m → K) ↔ IsUnit A
Tactic: rw [← col_transpose, ← mulVec_injective_iff, ← coe_mulVecLin, mulVecLin_transpose,
    ← vecMul_injective_iff_isUnit, coe_vecMulLinear]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
rw : LinearIndependent K Aᵀ.col ↔ IsUnit A
rw₁ : Function.Injective Aᵀ.mulVec ↔ IsUnit A
rw₂ : Function.Injective (α := m → K) (β := m → K) (⇑Aᵀ.mulVecLin : (a : m → K) → m → K) ↔ IsUnit A
⊢ LinearIndependent K A.row ↔ IsUnit A
have rw₃ : Function.Injective (α := m → K) (β := m → K) (⇑A.vecMulLinear : (a : m → K) → m → K) ↔ IsUnit A
Tactic: rw [← col_transpose, ← mulVec_injective_iff, ← coe_mulVecLin, mulVecLin_transpose,
    ← vecMul_injective_iff_isUnit, coe_vecMulLinear]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
rw : LinearIndependent K Aᵀ.col ↔ IsUnit A
rw₁ : Function.Injective Aᵀ.mulVec ↔ IsUnit A
rw₂ : Function.Injective (α := m → K) (β := m → K) (⇑Aᵀ.mulVecLin : (a : m → K) → m → K) ↔ IsUnit A
rw₃ : Function.Injective (α := m → K) (β := m → K) (⇑A.vecMulLinear : (a : m → K) → m → K) ↔ IsUnit A
⊢ LinearIndependent K A.row ↔ IsUnit A
have rw₄ : Function.Injective (α := m → K) (β := m → K) (⇑A.vecMulLinear : (a : m → K) → m → K) ↔
  Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
Tactic: rw [← col_transpose, ← mulVec_injective_iff, ← coe_mulVecLin, mulVecLin_transpose,
    ← vecMul_injective_iff_isUnit, coe_vecMulLinear]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
rw : LinearIndependent K Aᵀ.col ↔ IsUnit A
rw₁ : Function.Injective Aᵀ.mulVec ↔ IsUnit A
rw₂ : Function.Injective (α := m → K) (β := m → K) (⇑Aᵀ.mulVecLin : (a : m → K) → m → K) ↔ IsUnit A
rw₃ : Function.Injective (α := m → K) (β := m → K) (⇑A.vecMulLinear : (a : m → K) → m → K) ↔ IsUnit A
rw₄ :
  Function.Injective (α := m → K) (β := m → K) (⇑A.vecMulLinear : (a : m → K) → m → K) ↔
    Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
⊢ LinearIndependent K A.row ↔ IsUnit A
have rw₅ : (Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A) ↔ Function.Injective (β := m → K) fun (v : m → K) ↦ v ᵥ* A
Tactic: rw [← col_transpose, ← mulVec_injective_iff, ← coe_mulVecLin, mulVecLin_transpose,
    ← vecMul_injective_iff_isUnit, coe_vecMulLinear]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
⊢ LinearIndependent K A.col ↔ IsUnit A
have rw : LinearIndependent K Aᵀ.row ↔ IsUnit A
Tactic: rw [← row_transpose, linearIndependent_rows_iff_isUnit, isUnit_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
rw : LinearIndependent K Aᵀ.row ↔ IsUnit A
⊢ LinearIndependent K A.col ↔ IsUnit A
have rw₁ : IsUnit Aᵀ ↔ IsUnit A
Tactic: rw [← row_transpose, linearIndependent_rows_iff_isUnit, isUnit_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
inst : DecidableEq m
K : Type u_3
inst_1 : Field K
inst_2 : Fintype m
A : Matrix m m K
rw : LinearIndependent K Aᵀ.row ↔ IsUnit A
rw₁ : IsUnit Aᵀ ↔ IsUnit A
⊢ LinearIndependent K A.col ↔ IsUnit A
have rw₂ : IsUnit A ↔ IsUnit A
Tactic: rw [← row_transpose, linearIndependent_rows_iff_isUnit, isUnit_transpose]
-- 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 α
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
have pos : ∀ (h : IsUnit A.det), A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
Tactic: by_cases h : IsUnit A.det
-- 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 α
pos : ∀ (h : IsUnit A.det), A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
have neg : ∀ (h : ¬IsUnit A.det), A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
Tactic: by_cases h : IsUnit A.det
-- 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 α
h : IsUnit A.det
⊢ A⁻¹.det * A.det = 1
have rw : (A⁻¹ * A).det = 1
Tactic: rw [← det_mul, A.nonsing_inv_mul h, det_one]
-- 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 α
h : IsUnit A.det
rw : (A⁻¹ * A).det = 1
⊢ A⁻¹.det * A.det = 1
have rw₁ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 1) 1
Tactic: rw [← det_mul, A.nonsing_inv_mul h, det_one]
-- 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 α
h : IsUnit A.det
rw : (A⁻¹ * A).det = 1
rw₁ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 1) 1
⊢ A⁻¹.det * A.det = 1
have rw₂ : Eq.{v + 1} (α := α) 1 1
Tactic: rw [← det_mul, A.nonsing_inv_mul h, det_one]
-- 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 α
⊢ A⁻¹.det = A.det⁻¹ʳ
have pos : ∀ (h : IsUnit A.det), A⁻¹.det = A.det⁻¹ʳ
Tactic: by_cases h : IsUnit A.det
-- 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 α
pos : ∀ (h : IsUnit A.det), A⁻¹.det = A.det⁻¹ʳ
⊢ A⁻¹.det = A.det⁻¹ʳ
have neg : ∀ (h : ¬IsUnit A.det), A⁻¹.det = A.det⁻¹ʳ
Tactic: by_cases h : IsUnit A.det
-- 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 α
h : IsUnit A.det
⊢ A⁻¹.det = A.det⁻¹ʳ
have pos : ∀ (val : Invertible A.det), A⁻¹.det = A.det⁻¹ʳ
Tactic: cases h.nonempty_invertible
-- 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 α
h : IsUnit A.det
val : Invertible A.det
this : Invertible A := A.invertibleOfDetInvertible
⊢ A⁻¹.det = A.det⁻¹ʳ
have pos : A⁻¹.det = @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _
Tactic: rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]
-- 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 α
h : IsUnit A.det
val : Invertible A.det
this : Invertible A := A.invertibleOfDetInvertible
pos : A⁻¹.det = @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _
⊢ A⁻¹.det = A.det⁻¹ʳ
have pos₁ : (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _).det =
  @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _
Tactic: rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]
-- 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 α
h : IsUnit A.det
val : Invertible A.det
this : Invertible A := A.invertibleOfDetInvertible
pos : A⁻¹.det = @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _
pos₁ :
  (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _).det =
    @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _
⊢ A⁻¹.det = A.det⁻¹ʳ
have pos₂ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ =
  @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne A.det _
Tactic: rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]
-- 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 α
h : ¬IsUnit A.det
⊢ A⁻¹.det = A.det⁻¹ʳ
have neg : IsEmpty n → A⁻¹.det = A.det⁻¹ʳ
Tactic: cases isEmpty_or_nonempty n
-- 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 α
h : ¬IsUnit A.det
neg : IsEmpty n → A⁻¹.det = A.det⁻¹ʳ
⊢ A⁻¹.det = A.det⁻¹ʳ
have neg₁ : Nonempty n → A⁻¹.det = A.det⁻¹ʳ
Tactic: cases isEmpty_or_nonempty n
-- 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 α
h : ¬IsUnit A.det
h_1 : IsEmpty n
⊢ A⁻¹.det = A.det⁻¹ʳ
have neg : 1 = A.det⁻¹ʳ
Tactic: rw [det_isEmpty, det_isEmpty, Ring.inverse_one]
-- 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 α
h : ¬IsUnit A.det
h_1 : IsEmpty n
neg : 1 = A.det⁻¹ʳ
⊢ A⁻¹.det = A.det⁻¹ʳ
have neg₁ : Eq.{v + 1} (α := α) 1 1⁻¹ʳ
Tactic: rw [det_isEmpty, det_isEmpty, Ring.inverse_one]
-- 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 α
h : ¬IsUnit A.det
h_1 : IsEmpty n
neg : 1 = A.det⁻¹ʳ
neg₁ : Eq.{v + 1} (α := α) 1 1⁻¹ʳ
⊢ A⁻¹.det = A.det⁻¹ʳ
have neg₂ : Eq.{v + 1} (α := α) 1 1
Tactic: rw [det_isEmpty, det_isEmpty, Ring.inverse_one]
-- 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 α
h : ¬IsUnit A.det
h_1 : Nonempty n
⊢ A⁻¹.det = A.det⁻¹ʳ
have neg : A⁻¹.det = 0
Tactic: rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero ‹_›]
-- 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 α
h : ¬IsUnit A.det
h_1 : Nonempty n
neg : A⁻¹.det = 0
⊢ A⁻¹.det = A.det⁻¹ʳ
have neg₁ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 0) 0
Tactic: rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero ‹_›]
-- 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 α
h : ¬IsUnit A.det
h_1 : Nonempty n
neg : A⁻¹.det = 0
neg₁ : Eq.{v + 1} (α := α) (det.{v, u'} (n := n) 0) 0
⊢ A⁻¹.det = A.det⁻¹ʳ
have neg₂ : Eq.{v + 1} (α := α) 0 0
Tactic: rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero ‹_›]
-- 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 α
h : IsUnit A.det
⊢ A⁻¹⁻¹ = 1 * A⁻¹⁻¹
have rw : A⁻¹⁻¹ = A⁻¹⁻¹
Tactic: rw [Matrix.one_mul]
-- 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 α
h : IsUnit A.det
⊢ 1 * A⁻¹⁻¹ = A * A⁻¹ * A⁻¹⁻¹
have rw : 1 * A⁻¹⁻¹ = 1 * A⁻¹⁻¹
Tactic: rw [A.mul_nonsing_inv h]