awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ 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

Tactic:
conv in _ * _ =>
      congr
      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)
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
rw₂ rw₃ : Eq (α := Matrix m m α) 1 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

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:
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))
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))
⊢ 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 [@Invertible.congr _ _ _ _ _ (submatrixEquivInvertible A e₁ e₂) rfl]

Premises used: Invertible.congr, rfl
-- 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 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 _ 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:
rfl
-- 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 m m α
e₁ e₂ : n ≃ m
⊢ IsUnit (M := Matrix n n α) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m)) ↔ IsUnit A

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
    (submatrixEquivInvertibleEquivInvertible A _ _).nonempty_congr]

Premises used: Matrix.submatrixEquivInvertibleEquivInvertible, nonempty_invertible_iff_isUnit, Equiv.nonempty_congr
-- 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 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))
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))
⊢ 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

Premises used: IsUnit
-- 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 m m α
e₁ e₂ : n ≃ m
h : IsUnit A
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))
⊢ 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

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 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))
pos₂ 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))

Tactic:
rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq A]

Premises used: Matrix.invOf_eq_nonsing_inv, Matrix.invOf_submatrix_equiv_eq
-- 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 m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
⊢ ¬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
-- 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 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))
neg₃ : Eq (α := Matrix n n α) 0 (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))

Tactic:
simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this,
      submatrix_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, Matrix.nonsing_inv_eq_ringInverse, Ring.inverse_non_unit, Matrix.submatrix_zero
-- 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
e₁ e₂ : n ≃ m
A : Matrix n n α
⊢ Eq (α := Matrix m m α) (((reindex e₁ e₂ : (a : Matrix n n α) → Matrix m m α) A)⁻¹ : Matrix m m α)
    ((reindex e₂ e₁ : (a : Matrix n n α) → Matrix m m α) A⁻¹ : Matrix m m α)

Tactic:
inv_submatrix_equiv A e₁.symm e₂.symm

Premises used: Matrix.submatrix, Matrix.inv_submatrix_equiv, Equiv.symm
-- 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 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⁻¹)
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⁻¹)
⊢ 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

Premises used: IsUnit, Matrix.det
-- 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 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⁻¹)
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⁻¹)
⊢ 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

Premises used: isEmpty_or_nonempty
-- 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 m m α
B : Matrix n n α
hA : ¬IsUnit A.det
h : 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:
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 m m α
B : Matrix n n α
hA : ¬IsUnit A.det
h : Nonempty n
⊢ ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))

Tactic:
mt (fun hAB => ?_) hA

Premises used: mt
-- 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 m m α
B : Matrix n n α
hA : ¬IsUnit A.det
h : Nonempty n
refine : ∀ (hAB : IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))), IsUnit A.det
⊢ ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))

Tactic:
refine mt (fun hAB => ?_) hA

Premises used: mt
-- 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 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 ^ Fintype.card n * B.det ^ Fintype.card m)

Tactic:
rw [det_kronecker] at hAB

Premises used: Matrix.det_kronecker
-- 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 m m α
B : Matrix n n α
hA : ¬IsUnit A.det
h : Nonempty n
hAB : IsUnit (A.det ^ Fintype.card n * B.det ^ Fintype.card m)
⊢ IsUnit A.det

Tactic:
(isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)

Premises used: isUnit_pow_iff, isUnit_of_mul_isUnit_left, Fintype.card_ne_zero, Iff.mp
-- 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 m m α
B : Matrix n n α
hA : ¬IsUnit A.det
h : Nonempty n
hAB : IsUnit (A.det ^ Fintype.card n * B.det ^ Fintype.card m)
⊢ IsUnit A.det

Tactic:
exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)

Premises used: isUnit_pow_iff, isUnit_of_mul_isUnit_left, Fintype.card_ne_zero, Iff.mp
-- 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 m m α
B : Matrix n n α
hA : ¬IsUnit A.det
h : Nonempty n
⊢ ¬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)
-- 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 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
neg₂ neg₃ : Eq (α := Matrix (m × n) (m × n) α) 0 0
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)

Tactic:
rw [nonsing_inv_apply_not_isUnit _ hA, zero_kronecker, nonsing_inv_apply_not_isUnit _ hAB]

Premises used: Matrix.zero_kronecker, Matrix.nonsing_inv_apply_not_isUnit
-- 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 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⁻¹)
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⁻¹)
⊢ 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

Premises used: IsUnit, Matrix.det
-- 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 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⁻¹)
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⁻¹)
⊢ 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

Premises used: isEmpty_or_nonempty
-- 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 m m α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h : 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:
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 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))

Tactic:
mt (fun hAB => ?_) hB

Premises used: mt
-- 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 m m α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h : Nonempty m
refine : ∀ (hAB : IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))), IsUnit B.det
⊢ ¬IsUnit (M := α) (det (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B))

Tactic:
refine mt (fun hAB => ?_) hB

Premises used: mt
-- 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 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 (A.det ^ Fintype.card n * B.det ^ Fintype.card m)

Tactic:
rw [det_kronecker] at hAB

Premises used: Matrix.det_kronecker
-- 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 m m α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h : Nonempty m
hAB : IsUnit (A.det ^ Fintype.card n * B.det ^ Fintype.card m)
⊢ IsUnit B.det

Tactic:
(isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_right hAB)

Premises used: isUnit_pow_iff, isUnit_of_mul_isUnit_right, Fintype.card_ne_zero, Iff.mp
-- 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 m m α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h : Nonempty m
hAB : IsUnit (A.det ^ Fintype.card n * B.det ^ Fintype.card m)
⊢ IsUnit B.det

Tactic:
exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_right hAB)

Premises used: isUnit_pow_iff, isUnit_of_mul_isUnit_right, Fintype.card_ne_zero, Iff.mp
-- 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 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))

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)
-- 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 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
neg₂ neg₃ : Eq (α := Matrix (m × n) (m × n) α) 0 0
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)

Tactic:
rw [nonsing_inv_apply_not_isUnit _ hB, kronecker_zero, nonsing_inv_apply_not_isUnit _ hAB]

Premises used: Matrix.nonsing_inv_apply_not_isUnit, Matrix.kronecker_zero
-- 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 m m α
B : Matrix n n α
hA : IsUnit A.det
hB : IsUnit B.det
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
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B)⁻¹
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A⁻¹ B⁻¹)

Tactic:
apply inv_eq_right_inv

Premises used: Matrix.inv_eq_right_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 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)
pos₃ pos₄ :
  Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 1 1)
    (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

Tactic:
rw [← mul_kronecker_mul, ← one_kronecker_one, mul_nonsing_inv _ hA, mul_nonsing_inv _ hB]

Premises used: Matrix.mul_kronecker_mul, Matrix.one_kronecker_one, Matrix.mul_nonsing_inv