-- 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:
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
⊢ ¬IsUnit (kroneckerMap (fun x1 x2 => x1 * x2) A B).det

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

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 (kroneckerMap (fun x1 x2 => x1 * x2) A B).det
⊢ IsUnit A.det

Proof state:
case pos.h
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⁻¹ = 1

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

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
hB : IsUnit B.det
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

Tactic:
apply inv_eq_right_inv

Result:
case pos.h
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⁻¹ = 1

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
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

Tactic:
by_cases hA : IsUnit A.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
⊢ (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
⊢ (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
h✝ : Nonempty n
⊢ (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 => ?_) hA
  rw [det_kronecker] at hAB
  exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left 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
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⁻¹

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⁻¹

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:
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
⊢ (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
⊢ (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
hB : ¬IsUnit B.det
h✝ : Nonempty m
⊢ ¬IsUnit (kroneckerMap (fun x1 x2 => x1 * x2) A B).det

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

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
hB : ¬IsUnit B.det
h✝ : Nonempty m
hAB : IsUnit (kroneckerMap (fun x1 x2 => x1 * x2) A B).det
⊢ IsUnit B.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 (kroneckerMap (fun x1 x2 => x1 * x2) A B).det
⊢ IsUnit B.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
hB : ¬IsUnit B.det
h✝ : Nonempty m
hAB : IsUnit (A.det ^ Fintype.card n * B.det ^ Fintype.card m)
⊢ IsUnit B.det

Proof state:
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⁻¹

Tactic:
subsingleton

Result:
no goals

Proof state:
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⁻¹

Tactic:
subsingleton

Result:
no goals