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 α
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))
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))
⊢ 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 (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 α
B : Matrix n n α
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have pos : ∀ (hA : IsUnit A.det),
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
Tactic: by_cases hA : IsUnit A.det
-- 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 α
B : Matrix n n α
pos :
  ∀ (hA : IsUnit A.det),
    Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
      (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have neg : ∀ (hA : ¬IsUnit A.det),
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
Tactic: by_cases hA : IsUnit A.det
-- 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 α
B : Matrix n n α
hA : ¬IsUnit A.det
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have neg : IsEmpty n →
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
Tactic: cases isEmpty_or_nonempty n
-- 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 α
B : Matrix n n α
hA : ¬IsUnit A.det
neg :
  IsEmpty n →
    Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
      (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have neg₁ : Nonempty n →
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
Tactic: cases isEmpty_or_nonempty n
-- 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 α
B : Matrix n n α
hA : ¬IsUnit A.det
h : Nonempty n
⊢ ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))
have refine : ∀ (hAB : IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))), IsUnit A.det
Tactic: refine mt (fun hAB => ?_) hA
-- 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 α
B : Matrix n n α
hA : ¬IsUnit A.det
h : Nonempty n
hAB : IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))
⊢ IsUnit A.det
have hAB₁ : IsUnit (A.det ^ Fintype.card n * B.det ^ Fintype.card m)
Tactic: rw [det_kronecker] at hAB
Cleared hypotheses: hAB
-- 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 α
B : Matrix n n α
hA : ¬IsUnit A.det
h : Nonempty n
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have hAB : ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))
Tactic: have hAB : ¬IsUnit (A ⊗ₖ B).det := by
      refine mt (fun hAB => ?_) hA
      rw [det_kronecker] at hAB
      exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)
-- 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 α
B : Matrix n n α
hA : ¬IsUnit A.det
h : Nonempty n
hAB : ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have neg : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
  (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 0 B⁻¹)
Tactic: rw [nonsing_inv_apply_not_isUnit _ hA, zero_kronecker, nonsing_inv_apply_not_isUnit _ hAB]
-- 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 α
B : Matrix n n α
hA : ¬IsUnit A.det
h : Nonempty n
hAB : ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))
neg :
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 0 B⁻¹)
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have neg₁ : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹ 0
Tactic: rw [nonsing_inv_apply_not_isUnit _ hA, zero_kronecker, nonsing_inv_apply_not_isUnit _ hAB]
-- 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 α
B : Matrix n n α
hA : ¬IsUnit A.det
h : Nonempty n
hAB : ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))
neg :
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 0 B⁻¹)
neg₁ : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹ 0
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have neg₂ : Eq (α := Matrix (m × n) (m × n) α) 0 0
Tactic: rw [nonsing_inv_apply_not_isUnit _ hA, zero_kronecker, nonsing_inv_apply_not_isUnit _ hAB]
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have pos : ∀ (hB : IsUnit B.det),
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
Tactic: by_cases hB : IsUnit B.det
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
pos :
  ∀ (hB : IsUnit B.det),
    Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
      (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have neg : ∀ (hB : ¬IsUnit B.det),
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
Tactic: by_cases hB : IsUnit B.det
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have neg : IsEmpty m →
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
Tactic: cases isEmpty_or_nonempty m
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
neg :
  IsEmpty m →
    Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
      (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have neg₁ : Nonempty m →
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
Tactic: cases isEmpty_or_nonempty m
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h : Nonempty m
⊢ ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))
have refine : ∀ (hAB : IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))), IsUnit B.det
Tactic: refine mt (fun hAB => ?_) hB
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h : Nonempty m
hAB : IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))
⊢ IsUnit B.det
have hAB₁ : IsUnit (A.det ^ Fintype.card n * B.det ^ Fintype.card m)
Tactic: rw [det_kronecker] at hAB
Cleared hypotheses: hAB
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h : Nonempty m
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have hAB : ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))
Tactic: have hAB : ¬IsUnit (A ⊗ₖ B).det := by
      refine mt (fun hAB => ?_) hB
      rw [det_kronecker] at hAB
      exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_right hAB)
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h : Nonempty m
hAB : ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have neg : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
  (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ 0)
Tactic: rw [nonsing_inv_apply_not_isUnit _ hB, kronecker_zero, nonsing_inv_apply_not_isUnit _ hAB]
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h : Nonempty m
hAB : ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))
neg :
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ 0)
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have neg₁ : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹ 0
Tactic: rw [nonsing_inv_apply_not_isUnit _ hB, kronecker_zero, nonsing_inv_apply_not_isUnit _ hAB]
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h : Nonempty m
hAB : ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))
neg :
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ 0)
neg₁ : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹ 0
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have neg₂ : Eq (α := Matrix (m × n) (m × n) α) 0 0
Tactic: rw [nonsing_inv_apply_not_isUnit _ hB, kronecker_zero, nonsing_inv_apply_not_isUnit _ hAB]
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : IsUnit B.det
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)
have pos : HMul.hMul (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹) =
  1
Tactic: apply inv_eq_right_inv
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : IsUnit B.det
⊢ HMul.hMul (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)
      (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹) =
    1
have pos : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (A * A⁻¹) (B * B⁻¹)) 1
Tactic: rw [← mul_kronecker_mul, ← one_kronecker_one, mul_nonsing_inv _ hA, mul_nonsing_inv _ hB]
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : IsUnit B.det
pos : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (A * A⁻¹) (B * B⁻¹)) 1
⊢ HMul.hMul (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)
      (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹) =
    1
have pos₁ : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (A * A⁻¹) (B * B⁻¹))
  (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 1 1)
Tactic: rw [← mul_kronecker_mul, ← one_kronecker_one, mul_nonsing_inv _ hA, mul_nonsing_inv _ hB]
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : IsUnit B.det
pos : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (A * A⁻¹) (B * B⁻¹)) 1
pos₁ :
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (A * A⁻¹) (B * B⁻¹))
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 1 1)
⊢ HMul.hMul (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)
      (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹) =
    1
have pos₂ : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 1 (B * B⁻¹))
  (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 1 1)
Tactic: rw [← mul_kronecker_mul, ← one_kronecker_one, mul_nonsing_inv _ hA, mul_nonsing_inv _ hB]
-- 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 α
B : Matrix n n α
hA : IsUnit A.det
hB : IsUnit B.det
pos : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (A * A⁻¹) (B * B⁻¹)) 1
pos₁ :
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (A * A⁻¹) (B * B⁻¹))
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 1 1)
pos₂ :
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 1 (B * B⁻¹))
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 1 1)
⊢ HMul.hMul (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)
      (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹) =
    1
have pos₃ : Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 1 1)
  (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 1 1)
Tactic: rw [← mul_kronecker_mul, ← one_kronecker_one, mul_nonsing_inv _ hA, mul_nonsing_inv _ hB]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M * N * M⁻¹).det = N.det
have rw : ((↑h.unit : Matrix m m α) * N * (↑h.unit : Matrix m m α)⁻¹).det = N.det
Tactic: rw [← h.unit_spec, ← coe_units_inv, det_units_conj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
rw : ((↑h.unit : Matrix m m α) * N * (↑h.unit : Matrix m m α)⁻¹).det = N.det
⊢ (M * N * M⁻¹).det = N.det
have rw₁ : ((↑h.unit : Matrix m m α) * N * (↑h.unit⁻¹ : Matrix m m α)).det = N.det
Tactic: rw [← h.unit_spec, ← coe_units_inv, det_units_conj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
rw : ((↑h.unit : Matrix m m α) * N * (↑h.unit : Matrix m m α)⁻¹).det = N.det
rw₁ : ((↑h.unit : Matrix m m α) * N * (↑h.unit⁻¹ : Matrix m m α)).det = N.det
⊢ (M * N * M⁻¹).det = N.det
have rw₂ : N.det = N.det
Tactic: rw [← h.unit_spec, ← coe_units_inv, det_units_conj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M⁻¹ * N * M).det = N.det
have rw : ((↑h.unit : Matrix m m α)⁻¹ * N * (↑h.unit : Matrix m m α)).det = N.det
Tactic: rw [← h.unit_spec, ← coe_units_inv, det_units_conj']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
rw : ((↑h.unit : Matrix m m α)⁻¹ * N * (↑h.unit : Matrix m m α)).det = N.det
⊢ (M⁻¹ * N * M).det = N.det
have rw₁ : ((↑h.unit⁻¹ : Matrix m m α) * N * (↑h.unit : Matrix m m α)).det = N.det
Tactic: rw [← h.unit_spec, ← coe_units_inv, det_units_conj']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
rw : ((↑h.unit : Matrix m m α)⁻¹ * N * (↑h.unit : Matrix m m α)).det = N.det
rw₁ : ((↑h.unit⁻¹ : Matrix m m α) * N * (↑h.unit : Matrix m m α)).det = N.det
⊢ (M⁻¹ * N * M).det = N.det
have rw₂ : N.det = N.det
Tactic: rw [← h.unit_spec, ← coe_units_inv, det_units_conj']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M * N * M⁻¹).trace = N.trace
have rw : ((↑h.unit : Matrix m m α) * N * (↑h.unit : Matrix m m α)⁻¹).trace = N.trace
Tactic: rw [← h.unit_spec, ← coe_units_inv, trace_units_conj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
rw : ((↑h.unit : Matrix m m α) * N * (↑h.unit : Matrix m m α)⁻¹).trace = N.trace
⊢ (M * N * M⁻¹).trace = N.trace
have rw₁ : ((↑h.unit : Matrix m m α) * N * (↑h.unit⁻¹ : Matrix m m α)).trace = N.trace
Tactic: rw [← h.unit_spec, ← coe_units_inv, trace_units_conj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
rw : ((↑h.unit : Matrix m m α) * N * (↑h.unit : Matrix m m α)⁻¹).trace = N.trace
rw₁ : ((↑h.unit : Matrix m m α) * N * (↑h.unit⁻¹ : Matrix m m α)).trace = N.trace
⊢ (M * N * M⁻¹).trace = N.trace
have rw₂ : N.trace = N.trace
Tactic: rw [← h.unit_spec, ← coe_units_inv, trace_units_conj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M⁻¹ * N * M).trace = N.trace
have rw : ((↑h.unit : Matrix m m α)⁻¹ * N * (↑h.unit : Matrix m m α)).trace = N.trace
Tactic: rw [← h.unit_spec, ← coe_units_inv, trace_units_conj']