awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : NonAssocSemiring α
inst_7 : NonAssocSemiring β
inst_8 : CommRing γ
inst_9 : Module R α
inst_10 : Module S β
inst_11 : Module R γ
inst_12 : Module S γ
inst_13 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm :
  ∀ (a b : α) (a' b' : β),
    (((f : (a : α) → β →ₗ[S] γ) (a * b) : β →ₗ[S] γ) : (a : β) → γ) (a' * b') =
      HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) a' : γ)
        ((((f : (a : α) → β →ₗ[S] γ) b : β →ₗ[S] γ) : (a : β) → γ) b' : γ)
A : Matrix m m α
B : Matrix n n β
x : β
⊢ Eq.{u_7 + 1} (α := γ) (((f : (a : α) → β →ₗ[S] γ) 0 : (a : β) → γ) x : γ) (0 : γ)

Tactic:
exact LinearMap.map_zero₂ _ _

Premises used: LinearMap.map_zero₂
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : NonAssocSemiring α
inst_7 : NonAssocSemiring β
inst_8 : CommRing γ
inst_9 : Module R α
inst_10 : Module S β
inst_11 : Module R γ
inst_12 : Module S γ
inst_13 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm :
  ∀ (a b : α) (a' b' : β),
    (((f : (a : α) → β →ₗ[S] γ) (a * b) : β →ₗ[S] γ) : (a : β) → γ) (a' * b') =
      HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) a' : γ)
        ((((f : (a : α) → β →ₗ[S] γ) b : β →ₗ[S] γ) : (a : β) → γ) b' : γ)
A : Matrix m m α
B : Matrix n n β
x : α
⊢ Eq.{u_7 + 1} (α := γ) ((((f : (a : α) → β →ₗ[S] γ) x : β →ₗ[S] γ) : (a : β) → γ) 0 : γ) (0 : γ)

Tactic:
map_zero _

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : NonAssocSemiring α
inst_7 : NonAssocSemiring β
inst_8 : CommRing γ
inst_9 : Module R α
inst_10 : Module S β
inst_11 : Module R γ
inst_12 : Module S γ
inst_13 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm :
  ∀ (a b : α) (a' b' : β),
    (((f : (a : α) → β →ₗ[S] γ) (a * b) : β →ₗ[S] γ) : (a : β) → γ) (a' * b') =
      HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) a' : γ)
        ((((f : (a : α) → β →ₗ[S] γ) b : β →ₗ[S] γ) : (a : β) → γ) b' : γ)
A : Matrix m m α
B : Matrix n n β
x : α
⊢ Eq.{u_7 + 1} (α := γ) ((((f : (a : α) → β →ₗ[S] γ) x : β →ₗ[S] γ) : (a : β) → γ) 0 : γ) (0 : γ)

Tactic:
exact map_zero _

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : NonAssocSemiring α
inst_7 : NonAssocSemiring β
inst_8 : CommRing γ
inst_9 : Module R α
inst_10 : Module S β
inst_11 : Module R γ
inst_12 : Module S γ
inst_13 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm :
  ∀ (a b : α) (a' b' : β),
    (((f : (a : α) → β →ₗ[S] γ) (a * b) : β →ₗ[S] γ) : (a : β) → γ) (a' * b') =
      HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) a' : γ)
        ((((f : (a : α) → β →ₗ[S] γ) b : β →ₗ[S] γ) : (a : β) → γ) b' : γ)
A : Matrix m m α
B : Matrix n n β
simp_rw :
  HMul.hMul (α := γ) (∏ k : n, det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
      (∏ k : m, det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) =
    HPow.hPow (α := γ) (det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
        (Fintype.card n) *
      HPow.hPow (α := γ) (det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) (Fintype.card m)
simp_rw₁ :
  HPow.hPow (α := γ) (det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
        (Finset.card.{u_11} (α := n) Finset.univ) *
      HPow.hPow (α := γ) (det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b))
        (Finset.card.{u_10} (α := m) Finset.univ) =
    HPow.hPow (α := γ) (det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
        (Fintype.card n) *
      HPow.hPow (α := γ) (det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) (Fintype.card m)
⊢ HMul.hMul (α := γ)
      (det (n := m × n)
        (blockDiagonal fun (x : n) ↦ A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
      (det (n := n × m)
        (blockDiagonal fun (x : m) ↦ B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) =
    HPow.hPow (α := γ) (det (A.map fun (a : α) ↦ (((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) 1))
        (Fintype.card n) *
      HPow.hPow (α := γ) (det (B.map fun (b : β) ↦ ((f : (a : α) → β →ₗ[S] γ) 1 : (a : β) → γ) b)) (Fintype.card m)

Tactic:
simp_rw [det_blockDiagonal, Finset.prod_const, Finset.card_univ]

Premises used: Finset.card_univ, Finset.prod_const, Matrix.det_blockDiagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Mul α
A : Matrix l m α
B : Matrix n p α
i₁ : l
i₂ : n
j₁ : m
j₂ : p
⊢ kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B (i₁, i₂) (j₁, j₂) = A i₁ j₁ * B i₂ j₂

Tactic:
rfl

Premises used: Matrix.kroneckerMap, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : MulZeroClass α
B : Matrix n p α
⊢ Eq (α := Matrix (l × n) (m × p) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 0 B) 0

Tactic:
kroneckerMap_zero_left _ zero_mul B

Premises used: MulZeroClass.zero_mul, Matrix.kroneckerMap_zero_left
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : MulZeroClass α
A : Matrix l m α
⊢ Eq (α := Matrix (l × n) (m × p) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A 0) 0

Tactic:
kroneckerMap_zero_right _ mul_zero A

Premises used: MulZeroClass.mul_zero, Matrix.kroneckerMap_zero_right
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Distrib α
A₁ A₂ : Matrix l m α
B : Matrix n p α
⊢ kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (A₁ + A₂) B =
    HAdd.hAdd (α := Matrix (l × n) (m × p) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A₁ B)
      (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A₂ B)

Tactic:
kroneckerMap_add_left _ add_mul _ _ _

Premises used: add_mul, Matrix.kroneckerMap_add_left
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Distrib α
A : Matrix l m α
B₁ B₂ : Matrix n p α
⊢ kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A (B₁ + B₂) =
    HAdd.hAdd (α := Matrix (l × n) (m × p) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B₁)
      (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B₂)

Tactic:
kroneckerMap_add_right _ mul_add _ _ _

Premises used: Matrix.kroneckerMap_add_right, mul_add
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Mul α
inst_1 : SMul R α
inst_2 : IsScalarTower R α α
r : R
A : Matrix l m α
B : Matrix n p α
⊢ kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (r •> A) B = r •> kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B

Tactic:
kroneckerMap_smul_left _ _ (fun _ _ => smul_mul_assoc _ _ _) _ _

Premises used: smul_mul_assoc, Matrix.kroneckerMap_smul_left
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Mul α
inst_1 : SMul R α
inst_2 : SMulCommClass R α α
r : R
A : Matrix l m α
B : Matrix n p α
⊢ kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A (r •> B) = r •> kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B

Tactic:
kroneckerMap_smul_right _ _ (fun _ _ => mul_smul_comm _ _ _) _ _

Premises used: Matrix.kroneckerMap_smul_right, mul_smul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : MulZeroClass α
inst_1 : DecidableEq l
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : DecidableEq p
ia : l
ja : m
ib : n
jb : p
a b : α
⊢ kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (single ia ja a) (single ib jb b) = single (ia, ib) (ja, jb) (a * b)

Tactic:
kroneckerMap_single_single _ _ _ _ _ zero_mul mul_zero _ _

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Matrix.kroneckerMap_single_single
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
m : Type u_10
n : Type u_11
inst : MulZeroClass α
inst_1 : DecidableEq m
inst_2 : DecidableEq n
a : m → α
b : n → α
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (diagonal a) (diagonal b))
    (diagonal fun (mn : m × n) ↦ a mn.1 * b mn.2)

Tactic:
kroneckerMap_diagonal_diagonal _ zero_mul mul_zero _ _

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Matrix.kroneckerMap_diagonal_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : MulZeroClass α
inst_1 : DecidableEq n
A : Matrix l m α
b : n → α
⊢ Eq (α := Matrix (l × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A (diagonal b))
    (blockDiagonal fun (i : n) ↦ A <• b i)

Tactic:
kroneckerMap_diagonal_right _ mul_zero _ _

Premises used: Matrix.kroneckerMap_diagonal_right, MulZeroClass.mul_zero, Matrix.map, MulOpposite.unop
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : MulZeroClass α
inst_1 : DecidableEq l
a : l → α
B : Matrix m n α
⊢ Eq (α := Matrix (l × m) (l × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (diagonal a) B)
    ((reindex (Equiv.prodComm m l) (Equiv.prodComm n l) : (a : Matrix (m × l) (n × l) α) → Matrix (l × m) (l × n) α)
      (blockDiagonal fun (i : l) ↦ a i •> B))

Tactic:
kroneckerMap_diagonal_left _ zero_mul _ _

Premises used: MulZeroClass.zero_mul, Matrix.map, Matrix.kroneckerMap_diagonal_left
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq m
inst_2 : DecidableEq n
a b : ℕ
simp_rw :
  Eq (α := Matrix (m × n) (m × n) α) (diagonal fun (mn : m × n) ↦ (↑(a * b) : α)) (↑(a * b) : Matrix (m × n) (m × n) α)
⊢ Eq (α := Matrix (m × n) (m × n) α) (diagonal fun (mn : m × n) ↦ HMul.hMul (α := α) (↑a : α) (↑b : α))
    (↑(a * b) : Matrix (m × n) (m × n) α)

Tactic:
simp_rw [← Nat.cast_mul]

Premises used: Nat.cast_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq m
inst_2 : DecidableEq n
a b : ℕ
⊢ Eq (α := Matrix (m × n) (m × n) α) (diagonal fun (mn : m × n) ↦ (↑(a * b) : α)) (↑(a * b) : Matrix (m × n) (m × n) α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq n
A : Matrix l m α
b : ℕ
h : ∀ (x : n), A <• (↑b : α) = b •> A
⊢ Eq (α := Matrix (l × n) (m × n) α) (blockDiagonal fun (i : n) ↦ A <• (↑b : α)) (blockDiagonal fun (x : n) ↦ b •> A)

Tactic:
congr! 2
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq n
A : Matrix l m α
b : ℕ
x : n
h : ∀ (i : l) (j : m), (A <• (↑b : α)) i j = (b •> A) i j
⊢ A <• (↑b : α) = b •> A

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq n
A : Matrix l m α
b : ℕ
x : n
i : l
j : m
⊢ (A <• (↑b : α)) i j = (b •> A) i j

Tactic:
simp [(Nat.cast_commute b _).eq]

Premises used: Commute.eq, Nat.cast_commute
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq l
a : ℕ
B : Matrix m n α
h : Eq (α := l → Matrix m n α) (fun (i : l) ↦ (↑a : α) •> B) fun (x : l) ↦ a •> B
⊢ Eq (α := Matrix (l × m) (l × n) α)
    ((reindex (Equiv.prodComm m l) (Equiv.prodComm n l) : (a : Matrix (m × l) (n × l) α) → Matrix (l × m) (l × n) α)
        (blockDiagonal fun (i : l) ↦ (↑a : α) •> B) :
      Matrix (l × m) (l × n) α)
    ((reindex (Equiv.prodComm m l) (Equiv.prodComm n l) : (a : Matrix (m × l) (n × l) α) → Matrix (l × m) (l × n) α)
        (blockDiagonal fun (x : l) ↦ a •> B) :
      Matrix (l × m) (l × n) α)

Tactic:
congr! 2
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq l
a : ℕ
B : Matrix m n α
h : ∀ (x : l) (i : m) (j : n), ((↑a : α) •> B) i j = (a •> B) i j
⊢ Eq (α := l → Matrix m n α) (fun (i : l) ↦ (↑a : α) •> B) fun (x : l) ↦ a •> B

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq l
a : ℕ
B : Matrix m n α
x : l
i : m
j : n
⊢ ((↑a : α) •> B) i j = (a •> B) i j

Tactic:
simp [(Nat.cast_commute a _).eq]

Premises used: Commute.eq, Nat.cast_commute
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq n
A : Matrix l m α
b : ℕ
inst_2 : b.AtLeastTwo
⊢ Eq (α := Matrix (l × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A (OfNat.ofNat b))
    (blockDiagonal fun (x : n) ↦ A <• OfNat.ofNat b)

Tactic:
kronecker_diagonal _ _

Premises used: Matrix.diagonal, Matrix.kronecker_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : NonAssocSemiring α
inst_1 : DecidableEq l
a : ℕ
inst_2 : a.AtLeastTwo
B : Matrix m n α
⊢ Eq (α := Matrix (l × m) (l × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (OfNat.ofNat a) B)
    ((reindex (Equiv.prodComm m l) (Equiv.prodComm n l) : (a : Matrix (m × l) (n × l) α) → Matrix (l × m) (l × n) α)
      (blockDiagonal fun (x : l) ↦ OfNat.ofNat a •> B))

Tactic:
diagonal_kronecker _ _

Premises used: Matrix.diagonal_kronecker, Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
m : Type u_10
n : Type u_11
inst : MulZeroOneClass α
inst_1 : DecidableEq m
inst_2 : DecidableEq n
⊢ Eq (α := Matrix (m × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 1 1) 1

Tactic:
kroneckerMap_one_one _ zero_mul mul_zero (one_mul _)

Premises used: MulZeroClass.zero_mul, Matrix.kroneckerMap_one_one, MulZeroClass.mul_zero, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : MulZeroOneClass α
inst_1 : DecidableEq n
A : Matrix l m α
⊢ Eq (α := Matrix (l × n) (m × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A 1) (blockDiagonal fun (x : n) ↦ A)

Tactic:
(kronecker_diagonal _ _).trans <| congr_arg _ <| funext fun _ => Matrix.ext fun _ _ => mul_one _

Premises used: congr_arg, funext, mul_one, Matrix.ext, Matrix.kronecker_diagonal, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst : MulZeroOneClass α
inst_1 : DecidableEq l
B : Matrix m n α
⊢ Eq (α := Matrix (l × m) (l × n) α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) 1 B)
    ((reindex (Equiv.prodComm m l) (Equiv.prodComm n l) : (a : Matrix (m × l) (n × l) α) → Matrix (l × m) (l × n) α)
      (blockDiagonal fun (x : l) ↦ B))

Tactic:
(diagonal_kronecker _ _).trans <|
    congr_arg _ <| congr_arg _ <| funext fun _ => Matrix.ext fun _ _ => one_mul _

Premises used: congr_arg, funext, Matrix.diagonal_kronecker, Matrix.ext, one_mul, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
l' : Type u_15
m' : Type u_16
n' : Type u_17
inst : Fintype m
inst_1 : Fintype m'
inst_2 : CommSemiring α
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' α
B' : Matrix m' n' α
⊢ kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (A * B) (A' * B') =
    HMul.hMul (α := Matrix (l × l') (m × m') α) (β := Matrix (m × m') (n × n') α)
      (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A A') (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) B B')

Tactic:
kroneckerMapBilinear_mul_mul (Algebra.lmul ℕ α).toLinearMap mul_mul_mul_comm A B A' B'

Premises used: AlgHom.toLinearMap, Algebra.lmul, mul_mul_mul_comm, Nat, Matrix.kroneckerMapBilinear_mul_mul, Matrix.kroneckerMap
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
q : Type u_13
r : Type u_14
inst : Semigroup α
A : Matrix l m α
B : Matrix n p α
C : Matrix q r α
⊢ Eq (α := Matrix (l × n × q) (m × p × r) α)
    ((reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r) :
          (a : Matrix ((l × n) × q) ((m × p) × r) α) → Matrix (l × n × q) (m × p × r) α)
        (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B) C) :
      Matrix (l × n × q) (m × p × r) α)
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) B C) :
      Matrix (l × n × q) (m × p × r) α)

Tactic:
kroneckerMap_assoc₁ _ _ _ _ A B C mul_assoc

Premises used: Matrix.kroneckerMap_assoc₁, mul_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
q : Type u_13
r : Type u_14
inst : Semigroup α
A : Matrix l m α
B : Matrix n p α
C : Matrix q r α
⊢ Eq (α := Matrix (l × n × q) (m × p × r) α)
    (submatrix (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B) C)
      (⇑(Equiv.prodAssoc l n q).symm : (a : l × n × q) → (l × n) × q)
      (⇑(Equiv.prodAssoc m p r).symm : (a : m × p × r) → (m × p) × r))
    (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) B C))

Tactic:
kroneckerMap_assoc₁ _ _ _ _ A B C mul_assoc

Premises used: Matrix.submatrix, Matrix.kroneckerMap_assoc₁, mul_assoc, Matrix.kroneckerMap
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
m : Type u_10
n : Type u_11
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring α
A : Matrix m m α
B : Matrix n n α
⊢ trace (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B) = A.trace * B.trace

Tactic:
trace_kroneckerMapBilinear (Algebra.lmul ℕ α).toLinearMap _ _

Premises used: AlgHom.toLinearMap, Algebra.lmul, Nat, Matrix.kroneckerMap, Matrix.trace_kroneckerMapBilinear
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
m : Type u_10
n : Type u_11
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ det (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B) = A.det ^ Fintype.card n * B.det ^ Fintype.card m

Tactic:
(det_kroneckerMapBilinear (Algebra.lmul ℕ R).toLinearMap mul_mul_mul_comm _ _).trans ?_

Premises used: AlgHom.toLinearMap, Algebra.lmul, mul_mul_mul_comm, Matrix.det_kroneckerMapBilinear, Nat, Matrix.kroneckerMap, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
m : Type u_10
n : Type u_11
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing R
A : Matrix m m R
B : Matrix n n R
refine :
  HPow.hPow (α := R)
        (det
          (A.map fun (a : R) ↦
            (((AlgHom.toLinearMap (Algebra.lmul ℕ R) : (a : R) → R →ₗ[ℕ] R) a : R →ₗ[ℕ] R) : (a : R) → R) 1))
        (Fintype.card n) *
      HPow.hPow (α := R)
        (det (B.map fun (b : R) ↦ ((AlgHom.toLinearMap (Algebra.lmul ℕ R) : (a : R) → R →ₗ[ℕ] R) 1 : (a : R) → R) b))
        (Fintype.card m) =
    A.det ^ Fintype.card n * B.det ^ Fintype.card m
⊢ det (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B) = A.det ^ Fintype.card n * B.det ^ Fintype.card m

Tactic:
refine (det_kroneckerMapBilinear (Algebra.lmul ℕ R).toLinearMap mul_mul_mul_comm _ _).trans ?_

Premises used: AlgHom.toLinearMap, Algebra.lmul, mul_mul_mul_comm, Matrix.det_kroneckerMapBilinear, Nat, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
m : Type u_10
n : Type u_11
inst : Fintype m
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ HPow.hPow (α := R)
        (det
          (A.map fun (a : R) ↦
            (((AlgHom.toLinearMap (Algebra.lmul ℕ R) : (a : R) → R →ₗ[ℕ] R) a : R →ₗ[ℕ] R) : (a : R) → R) 1))
        (Fintype.card n) *
      HPow.hPow (α := R)
        (det (B.map fun (b : R) ↦ ((AlgHom.toLinearMap (Algebra.lmul ℕ R) : (a : R) → R →ₗ[ℕ] R) 1 : (a : R) → R) b))
        (Fintype.card m) =
    A.det ^ Fintype.card n * B.det ^ Fintype.card m

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommMagma R
inst_1 : StarMul R
x : Matrix l m R
y : Matrix n p R
a :
  ∀ (i : m × p) (j : l × n),
    Eq (α := R) ((kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y)ᴴ i j)
      (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) xᴴ yᴴ i j)
⊢ Eq (α := Matrix (m × p) (l × n) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y)ᴴ
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) xᴴ yᴴ)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommMagma R
inst_1 : StarMul R
x : Matrix l m R
y : Matrix n p R
i : m × p
j : l × n
⊢ Eq (α := R) ((kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y)ᴴ i j) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) xᴴ yᴴ i j)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Mul R
inst_1 : StarMul R
x : Matrix l m R
y : Matrix n p R
a :
  ∀ (i : m × p) (j : l × n),
    Eq (α := R) ((kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y)ᴴ i j)
      (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) yᴴ xᴴ) Prod.swap Prod.swap i j)
⊢ Eq (α := Matrix (m × p) (l × n) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y)ᴴ
    (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) yᴴ xᴴ) Prod.swap Prod.swap)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Mul R
inst_1 : StarMul R
x : Matrix l m R
y : Matrix n p R
i : m × p
j : l × n
⊢ Eq (α := R) ((kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y)ᴴ i j)
    (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) yᴴ xᴴ) Prod.swap Prod.swap i j)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
A : Matrix l m α
B : Matrix n p β
i₁ : l
i₂ : n
j₁ : m
j₂ : p
⊢ Eq (α := α ⊗[R] β) (kroneckerMap (tmul R) A B (i₁, i₂) (j₁, j₂)) (A i₁ j₁ ⊗ₜ[R] B i₂ j₂)

Tactic:
rfl

Premises used: Matrix.kroneckerMap, TensorProduct.tmul, AddCon.toQuotient, rfl