-- Mathlib/Data/Matrix/Kronecker.lean
theorem inv_kronecker [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing R]
    (A : Matrix m m R) (B : Matrix n n R) : (A ⊗ₖ B)⁻¹ = A⁻¹ ⊗ₖ B⁻¹

Proof state:
case neg
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit A.det
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

Tactic:
cases isEmpty_or_nonempty n

Result:
case neg.inl
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit A.det
h✝ : IsEmpty n
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

case neg.inr
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit A.det
h✝ : Nonempty n
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

Proof state:
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit A.det
h✝ : Nonempty n
hAB : IsUnit (kroneckerMap (fun x1 x2 => x1 * x2) A B).det
⊢ IsUnit A.det

Tactic:
rw [det_kronecker] at hAB

Result:
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit A.det
h✝ : Nonempty n
hAB : IsUnit (A.det ^ Fintype.card n * B.det ^ Fintype.card m)
⊢ IsUnit A.det

Proof state:
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
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)

Result:
no goals

Proof state:
case neg
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
hB : ¬IsUnit B.det
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

Tactic:
cases isEmpty_or_nonempty m

Result:
case neg.inl
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
hB : ¬IsUnit B.det
h✝ : IsEmpty m
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

case neg.inr
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
hB : ¬IsUnit B.det
h✝ : Nonempty m
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

Proof state:
case pos
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
hB : IsUnit B.det
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

case neg
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
hB : ¬IsUnit B.det
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

Tactic:
swap

Result:
case neg
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
hB : ¬IsUnit B.det
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

case pos
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
hB : IsUnit B.det
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

Proof state:
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
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)

Result:
no goals

Proof state:
case neg.inr
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
hB : ¬IsUnit B.det
h✝ : Nonempty m
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = 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)

Result:
case neg.inr
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
hB : ¬IsUnit B.det
h✝ : Nonempty m
hAB : ¬IsUnit (kroneckerMap (fun x1 x2 => x1 * x2) A B).det
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

Proof state:
case neg.inr
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
hB : ¬IsUnit B.det
h✝ : Nonempty m
hAB : ¬IsUnit (kroneckerMap (fun x1 x2 => x1 * x2) A B).det
⊢ (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]

Result:
no goals

Proof state:
case neg.inr
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : ¬IsUnit A.det
h✝ : Nonempty n
hAB : ¬IsUnit (kroneckerMap (fun x1 x2 => x1 * x2) A B).det
⊢ (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]

Result:
no goals

Proof state:
case pos
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

Tactic:
by_cases hB : IsUnit B.det

Result:
case pos
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
hB : IsUnit B.det
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

case neg
R : Type u_1
m : Type u_9
n : Type u_10
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
hA : IsUnit A.det
hB : ¬IsUnit B.det
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹