awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Add α
inst_1 : Add γ
f : α → β → γ
hf : ∀ (a₁ a₂ : α) (b : β), f (a₁ + a₂) b = f a₁ b + f a₂ b
A₁ A₂ : Matrix l m α
B : Matrix n p β
⊢ kroneckerMap f (A₁ + A₂) B = kroneckerMap f A₁ B + kroneckerMap f A₂ B

Tactic:
ext fun _ _ => hf _ _ _

Premises used: Prod.fst, Prod.snd, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Add β
inst_1 : Add γ
f : α → β → γ
hf : ∀ (a : α) (b₁ b₂ : β), f a (b₁ + b₂) = f a b₁ + f a b₂
A : Matrix l m α
B₁ B₂ : Matrix n p β
⊢ kroneckerMap f A (B₁ + B₂) = kroneckerMap f A B₁ + kroneckerMap f A B₂

Tactic:
ext fun _ _ => hf _ _ _

Premises used: Prod.fst, Prod.snd, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : SMul R α
inst_1 : SMul R γ
f : α → β → γ
r : R
hf : ∀ (a : α) (b : β), f (r •> a) b = r •> f a b
A : Matrix l m α
B : Matrix n p β
⊢ kroneckerMap f (r •> A) B = r •> kroneckerMap f A B

Tactic:
ext fun _ _ => hf _ _

Premises used: Prod.fst, Prod.snd, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : SMul R β
inst_1 : SMul R γ
f : α → β → γ
r : R
hf : ∀ (a : α) (b : β), f a (r •> b) = r •> f a b
A : Matrix l m α
B : Matrix n p β
⊢ kroneckerMap f A (r •> B) = r •> kroneckerMap f A B

Tactic:
ext fun _ _ => hf _ _

Premises used: Prod.fst, Prod.snd, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Zero α
inst_1 : Zero β
inst_2 : Zero γ
inst_3 : DecidableEq l
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : α
b : β
a₁ :
  ∀ (i₁' : l) (i₂' : n) (j₁' : m) (j₂' : p),
    kroneckerMap f (single i₁ j₁ a) (single i₂ j₂ b) (i₁', i₂') (j₁', j₂') =
      single (i₁, i₂) (j₁, j₂) (f a b) (i₁', i₂') (j₁', j₂')
⊢ kroneckerMap f (single i₁ j₁ a) (single i₂ j₂ b) = single (i₁, i₂) (j₁, j₂) (f a b)

Tactic:
ext ⟨i₁', i₂'⟩ ⟨j₁', j₂'⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Zero α
inst_1 : Zero β
inst_2 : Zero γ
inst_3 : DecidableEq l
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : α
b : β
i₁' : l
i₂' : n
j₁' : m
j₂' : p
a₁ :
  f (if i₁ = i₁' ∧ j₁ = j₁' then a else 0) (if i₂ = i₂' ∧ j₂ = j₂' then b else 0) =
    if (i₁, i₂) = (i₁', i₂') ∧ (j₁, j₂) = (j₁', j₂') then f a b else 0
⊢ kroneckerMap f (single i₁ j₁ a) (single i₂ j₂ b) (i₁', i₂') (j₁', j₂') =
    single (i₁, i₂) (j₁, j₂) (f a b) (i₁', i₂') (j₁', j₂')

Tactic:
dsimp [single]

Premises used: Matrix.single
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Zero α
inst_1 : Zero β
inst_2 : Zero γ
inst_3 : DecidableEq l
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : α
b : β
i₁' : l
i₂' : n
j₁' : m
j₂' : p
⊢ f (if i₁ = i₁' ∧ j₁ = j₁' then a else 0) (if i₂ = i₂' ∧ j₂ = j₂' then b else 0) =
    if (i₁, i₂) = (i₁', i₂') ∧ (j₁, j₂) = (j₁', j₂') then f a b else 0

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Zero α
inst_1 : Zero β
inst_2 : Zero γ
inst_3 : DecidableEq m
inst_4 : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
a₁ :
  ∀ (i₁ : m) (i₂ : n) (j₁ : m) (j₂ : n),
    kroneckerMap f (diagonal a) (diagonal b) (i₁, i₂) (j₁, j₂) =
      diagonal (fun (mn : m × n) ↦ f (a mn.1) (b mn.2)) (i₁, i₂) (j₁, j₂)
⊢ kroneckerMap f (diagonal a) (diagonal b) = diagonal fun (mn : m × n) ↦ f (a mn.1) (b mn.2)

Tactic:
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Zero α
inst_1 : Zero β
inst_2 : Zero γ
inst_3 : DecidableEq m
inst_4 : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
i₁ : m
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f (diagonal a) (diagonal b) (i₁, i₂) (j₁, j₂) =
    diagonal (fun (mn : m × n) ↦ f (a mn.1) (b mn.2)) (i₁, i₂) (j₁, j₂)

Tactic:
simp [diagonal, apply_ite f, ite_and, ite_apply, apply_ite (f (a i₁)), hf₁, hf₂]

Premises used: ite_apply, apply_ite, ite_and, Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
inst : Zero β
inst_1 : Zero γ
inst_2 : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
a :
  ∀ (i₁ : l) (i₂ : n) (j₁ : m) (j₂ : n),
    kroneckerMap f A (diagonal b) (i₁, i₂) (j₁, j₂) =
      blockDiagonal (fun (i : n) ↦ A.map fun (a : α) ↦ f a (b i)) (i₁, i₂) (j₁, j₂)
⊢ kroneckerMap f A (diagonal b) = blockDiagonal fun (i : n) ↦ A.map fun (a : α) ↦ f a (b i)

Tactic:
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
inst : Zero β
inst_1 : Zero γ
inst_2 : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
i₁ : l
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f A (diagonal b) (i₁, i₂) (j₁, j₂) =
    blockDiagonal (fun (i : n) ↦ A.map fun (a : α) ↦ f a (b i)) (i₁, i₂) (j₁, j₂)

Tactic:
simp [diagonal, blockDiagonal, apply_ite (f (A i₁ j₁)), hf]

Premises used: Matrix.blockDiagonal, apply_ite, Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
inst : Zero α
inst_1 : Zero γ
inst_2 : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
a₁ :
  ∀ (i₁ : l) (i₂ : m) (j₁ : l) (j₂ : n),
    kroneckerMap f (diagonal a) B (i₁, i₂) (j₁, j₂) =
      (reindex (Equiv.prodComm m l) (Equiv.prodComm n l) : (a : Matrix (m × l) (n × l) γ) → Matrix (l × m) (l × n) γ)
        (blockDiagonal fun (i : l) ↦ B.map fun (b : β) ↦ f (a i) b) (i₁, i₂) (j₁, j₂)
⊢ kroneckerMap f (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) ↦ B.map fun (b : β) ↦ f (a i) b)

Tactic:
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
inst : Zero α
inst_1 : Zero γ
inst_2 : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
i₁ : l
i₂ : m
j₁ : l
j₂ : n
⊢ kroneckerMap f (diagonal a) B (i₁, i₂) (j₁, j₂) =
    (reindex (Equiv.prodComm m l) (Equiv.prodComm n l) : (a : Matrix (m × l) (n × l) γ) → Matrix (l × m) (l × n) γ)
      (blockDiagonal fun (i : l) ↦ B.map fun (b : β) ↦ f (a i) b) (i₁, i₂) (j₁, j₂)

Tactic:
simp [diagonal, blockDiagonal, apply_ite f, ite_apply, hf]

Premises used: Matrix.blockDiagonal, ite_apply, apply_ite, Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Zero α
inst_1 : Zero β
inst_2 : Zero γ
inst_3 : One α
inst_4 : One β
inst_5 : One γ
inst_6 : DecidableEq m
inst_7 : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
hf₃ : f 1 1 = 1
⊢ Eq (α := Matrix (m × n) (m × n) γ) (diagonal fun (mn : m × n) ↦ f 1 1) 1

Tactic:
simp only [hf₃, diagonal_one]

Premises used: Matrix.diagonal_one
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
l' : Type u_15
m' : Type u_16
n' : Type u_17
p' : Type u_18
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
a :
  ∀ (i : l') (i' : n') (j : m') (j' : p'),
    kroneckerMap f ((reindex el em : (a : Matrix l m α) → Matrix l' m' α) M)
        ((reindex en ep : (a : Matrix n p β) → Matrix n' p' β) N) (i, i') (j, j') =
      (reindex (el.prodCongr en) (em.prodCongr ep) : (a : Matrix (l × n) (m × p) γ) → Matrix (l' × n') (m' × p') γ)
        (kroneckerMap f M N) (i, i') (j, j')
⊢ Eq (α := Matrix (l' × n') (m' × p') γ)
    (kroneckerMap f ((reindex el em : (a : Matrix l m α) → Matrix l' m' α) M)
      ((reindex en ep : (a : Matrix n p β) → Matrix n' p' β) N))
    ((reindex (el.prodCongr en) (em.prodCongr ep) : (a : Matrix (l × n) (m × p) γ) → Matrix (l' × n') (m' × p') γ)
      (kroneckerMap f M N))

Tactic:
ext ⟨i, i'⟩ ⟨j, j'⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
l' : Type u_15
m' : Type u_16
n' : Type u_17
p' : Type u_18
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
i : l'
i' : n'
j : m'
j' : p'
⊢ kroneckerMap f ((reindex el em : (a : Matrix l m α) → Matrix l' m' α) M)
      ((reindex en ep : (a : Matrix n p β) → Matrix n' p' β) N) (i, i') (j, j') =
    (reindex (el.prodCongr en) (em.prodCongr ep) : (a : Matrix (l × n) (m × p) γ) → Matrix (l' × n') (m' × p') γ)
      (kroneckerMap f M N) (i, i') (j, j')

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
l' : Type u_15
m' : Type u_16
n' : Type u_17
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
M : Matrix l m α
N : Matrix n n' β
⊢ Eq (α := Matrix (l' × n) (m' × n') γ) (kroneckerMap f ((reindex el em : (a : Matrix l m α) → Matrix l' m' α) M) N)
    ((reindex (el.prodCongr (Equiv.refl n)) (em.prodCongr (Equiv.refl n')) :
        (a : Matrix (l × n) (m × n') γ) → Matrix (l' × n) (m' × n') γ)
      (kroneckerMap f M N))

Tactic:
kroneckerMap_reindex _ _ _ (Equiv.refl _) (Equiv.refl _) _ _

Premises used: Matrix.submatrix, Matrix.kroneckerMap_reindex, Equiv.refl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
l' : Type u_15
m' : Type u_16
n' : Type u_17
f : α → β → γ
em : m ≃ m'
en : n ≃ n'
M : Matrix l l' α
N : Matrix m n β
⊢ Eq (α := Matrix (l × m') (l' × n') γ) (kroneckerMap f M ((reindex em en : (a : Matrix m n β) → Matrix m' n' β) N))
    ((reindex ((Equiv.refl l).prodCongr em) ((Equiv.refl l').prodCongr en) :
        (a : Matrix (l × m) (l' × n) γ) → Matrix (l × m') (l' × n') γ)
      (kroneckerMap f M N))

Tactic:
kroneckerMap_reindex _ (Equiv.refl _) (Equiv.refl _) _ _ _ _

Premises used: Matrix.submatrix, Matrix.kroneckerMap_reindex, Equiv.refl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
q : Type u_13
r : Type u_14
δ : Type u_19
ξ : Type u_20
ω : Type u_21
ω' : Type u_22
f : α → β → γ
g : γ → δ → ω
f' : α → ξ → ω'
g' : β → δ → ξ
A : Matrix l m α
B : Matrix n p β
D : Matrix q r δ
φ : ω ≃ ω'
hφ : ∀ (a : α) (b : β) (d : δ), (φ : (a : ω) → ω') (g (f a b) d) = f' a (g' b d)
⊢ (Equiv.trans (reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)) φ.mapMatrix :
        (a : Matrix ((l × n) × q) ((m × p) × r) ω) → Matrix (l × n × q) (m × p × r) ω')
      (kroneckerMap g (kroneckerMap f A B) D) =
    kroneckerMap f' A (kroneckerMap g' B D)

Tactic:
ext fun _ _ => hφ _ _ _

Premises used: Prod.fst, Equiv.symm, Prod.snd, DFunLike.coe, Matrix.ext, Equiv.prodAssoc
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
q : Type u_13
r : Type u_14
δ : Type u_19
ξ : Type u_20
ω : Type u_21
f : α → β → γ
g : γ → δ → ω
f' : α → ξ → ω
g' : β → δ → ξ
A : Matrix l m α
B : Matrix n p β
D : Matrix q r δ
h : ∀ (a : α) (b : β) (d : δ), g (f a b) d = f' a (g' b d)
⊢ (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 g (kroneckerMap f A B) D) =
    kroneckerMap f' A (kroneckerMap g' B D)

Tactic:
ext fun _ _ => h _ _ _

Premises used: Prod.fst, Equiv.symm, Prod.snd, DFunLike.coe, Matrix.ext, Equiv.prodAssoc
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
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 : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype m'
inst_4 : NonUnitalNonAssocSemiring α
inst_5 : NonUnitalNonAssocSemiring β
inst_6 : NonUnitalNonAssocSemiring γ
inst_7 : Module R α
inst_8 : Module R γ
inst_9 : Module S β
inst_10 : Module S γ
inst_11 : 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 l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
a :
  ∀ (i : l) (i' : l') (j : n) (j' : n'),
    (((kroneckerMapBilinear f : (a : Matrix l n α) → Matrix l' n' β →ₗ[S] Matrix (l × l') (n × n') γ) (A * B) :
            Matrix l' n' β →ₗ[S] Matrix (l × l') (n × n') γ) :
          (a : Matrix l' n' β) → Matrix (l × l') (n × n') γ)
        (A' * B') (i, i') (j, j') =
      HMul.hMul (α := Matrix (l × l') (m × m') γ) (β := Matrix (m × m') (n × n') γ)
        ((((kroneckerMapBilinear f : (a : Matrix l m α) → Matrix l' m' β →ₗ[S] Matrix (l × l') (m × m') γ) A :
                Matrix l' m' β →ₗ[S] Matrix (l × l') (m × m') γ) :
              (a : Matrix l' m' β) → Matrix (l × l') (m × m') γ)
            A' :
          Matrix (l × l') (m × m') γ)
        ((((kroneckerMapBilinear f : (a : Matrix m n α) → Matrix m' n' β →ₗ[S] Matrix (m × m') (n × n') γ) B :
                Matrix m' n' β →ₗ[S] Matrix (m × m') (n × n') γ) :
              (a : Matrix m' n' β) → Matrix (m × m') (n × n') γ)
            B' :
          Matrix (m × m') (n × n') γ)
        (i, i') (j, j')
⊢ (((kroneckerMapBilinear f : (a : Matrix l n α) → Matrix l' n' β →ₗ[S] Matrix (l × l') (n × n') γ) (A * B) :
          Matrix l' n' β →ₗ[S] Matrix (l × l') (n × n') γ) :
        (a : Matrix l' n' β) → Matrix (l × l') (n × n') γ)
      (A' * B') =
    HMul.hMul (α := Matrix (l × l') (m × m') γ) (β := Matrix (m × m') (n × n') γ)
      ((((kroneckerMapBilinear f : (a : Matrix l m α) → Matrix l' m' β →ₗ[S] Matrix (l × l') (m × m') γ) A :
              Matrix l' m' β →ₗ[S] Matrix (l × l') (m × m') γ) :
            (a : Matrix l' m' β) → Matrix (l × l') (m × m') γ)
          A' :
        Matrix (l × l') (m × m') γ)
      ((((kroneckerMapBilinear f : (a : Matrix m n α) → Matrix m' n' β →ₗ[S] Matrix (m × m') (n × n') γ) B :
              Matrix m' n' β →ₗ[S] Matrix (m × m') (n × n') γ) :
            (a : Matrix m' n' β) → Matrix (m × m') (n × n') γ)
          B' :
        Matrix (m × m') (n × n') γ)

Tactic:
ext ⟨i, i'⟩ ⟨j, j'⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
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 : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype m'
inst_4 : NonUnitalNonAssocSemiring α
inst_5 : NonUnitalNonAssocSemiring β
inst_6 : NonUnitalNonAssocSemiring γ
inst_7 : Module R α
inst_8 : Module R γ
inst_9 : Module S β
inst_10 : Module S γ
inst_11 : 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 l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
i : l
i' : l'
j : n
j' : n'
a :
  Eq.{u_7 + 1} (α := γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ j_1 : m, A i j_1 * B j_1 j) : (a : β) → γ) (∑ j : m', A' i' j * B' j j') : γ)
    (∑ x : m,
        ∑ x_1 : m',
          HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) (A i x) : β →ₗ[S] γ) : (a : β) → γ) (A' i' x_1) : γ)
            ((((f : (a : α) → β →ₗ[S] γ) (B x j) : β →ₗ[S] γ) : (a : β) → γ) (B' x_1 j') : γ) :
      γ)
⊢ (((kroneckerMapBilinear f : (a : Matrix l n α) → Matrix l' n' β →ₗ[S] Matrix (l × l') (n × n') γ) (A * B) :
          Matrix l' n' β →ₗ[S] Matrix (l × l') (n × n') γ) :
        (a : Matrix l' n' β) → Matrix (l × l') (n × n') γ)
      (A' * B') (i, i') (j, j') =
    HMul.hMul (α := Matrix (l × l') (m × m') γ) (β := Matrix (m × m') (n × n') γ)
      ((((kroneckerMapBilinear f : (a : Matrix l m α) → Matrix l' m' β →ₗ[S] Matrix (l × l') (m × m') γ) A :
              Matrix l' m' β →ₗ[S] Matrix (l × l') (m × m') γ) :
            (a : Matrix l' m' β) → Matrix (l × l') (m × m') γ)
          A' :
        Matrix (l × l') (m × m') γ)
      ((((kroneckerMapBilinear f : (a : Matrix m n α) → Matrix m' n' β →ₗ[S] Matrix (m × m') (n × n') γ) B :
              Matrix m' n' β →ₗ[S] Matrix (m × m') (n × n') γ) :
            (a : Matrix m' n' β) → Matrix (m × m') (n × n') γ)
          B' :
        Matrix (m × m') (n × n') γ)
      (i, i') (j, j')

Tactic:
simp only [kroneckerMapBilinear_apply_apply, mul_apply, ← Finset.univ_product_univ,
    Finset.sum_product, kroneckerMap_apply]

Premises used: Matrix.mul_apply, Matrix.kroneckerMapBilinear_apply_apply, Finset.univ_product_univ, Matrix.kroneckerMap_apply, Finset.sum_product
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
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 : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype m'
inst_4 : NonUnitalNonAssocSemiring α
inst_5 : NonUnitalNonAssocSemiring β
inst_6 : NonUnitalNonAssocSemiring γ
inst_7 : Module R α
inst_8 : Module R γ
inst_9 : Module S β
inst_10 : Module S γ
inst_11 : 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 l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
i : l
i' : l'
j : n
j' : n'
a :
  Eq.{u_7 + 1} (α := γ)
    ((∑ x : m, (f : (a : α) → β →ₗ[S] γ) (A i x * B x j) : (a : β) → γ) (∑ j : m', A' i' j * B' j j') : γ)
    (∑ x : m,
        ∑ x_1 : m',
          HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) (A i x) : β →ₗ[S] γ) : (a : β) → γ) (A' i' x_1) : γ)
            ((((f : (a : α) → β →ₗ[S] γ) (B x j) : β →ₗ[S] γ) : (a : β) → γ) (B' x_1 j') : γ) :
      γ)
a₁ :
  Eq.{u_7 + 1} (α := γ)
    (∑ d : m, (((f : (a : α) → β →ₗ[S] γ) (A i d * B d j) : β →ₗ[S] γ) : (a : β) → γ) (∑ j : m', A' i' j * B' j j'))
    (∑ x : m,
      ∑ x_1 : m',
        HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) (A i x) : β →ₗ[S] γ) : (a : β) → γ) (A' i' x_1) : γ)
          ((((f : (a : α) → β →ₗ[S] γ) (B x j) : β →ₗ[S] γ) : (a : β) → γ) (B' x_1 j') : γ))
a₂ :
  Eq.{u_7 + 1} (α := γ)
    (∑ x : m,
      ∑ x_1 : m', (((f : (a : α) → β →ₗ[S] γ) (A i x * B x j) : β →ₗ[S] γ) : (a : β) → γ) (A' i' x_1 * B' x_1 j'))
    (∑ x : m,
      ∑ x_1 : m',
        HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) (A i x) : β →ₗ[S] γ) : (a : β) → γ) (A' i' x_1) : γ)
          ((((f : (a : α) → β →ₗ[S] γ) (B x j) : β →ₗ[S] γ) : (a : β) → γ) (B' x_1 j') : γ))
⊢ Eq.{u_7 + 1} (α := γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ j_1 : m, A i j_1 * B j_1 j) : (a : β) → γ) (∑ j : m', A' i' j * B' j j') : γ)
    (∑ x : m,
        ∑ x_1 : m',
          HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) (A i x) : β →ₗ[S] γ) : (a : β) → γ) (A' i' x_1) : γ)
            ((((f : (a : α) → β →ₗ[S] γ) (B x j) : β →ₗ[S] γ) : (a : β) → γ) (B' x_1 j') : γ) :
      γ)

Tactic:
simp_rw [map_sum f, LinearMap.sum_apply, map_sum, h_comm]

Premises used: map_sum, LinearMap.sum_apply
-- 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 β
rw : ∀ (x : β), Eq.{u_7 + 1} (α := γ) (((f : (a : α) → β →ₗ[S] γ) 0 : (a : β) → γ) x : γ) (0 : γ)
rw₁ : ∀ (x : α), Eq.{u_7 + 1} (α := γ) ((((f : (a : α) → β →ₗ[S] γ) x : β →ₗ[S] γ) : (a : β) → γ) 0 : γ) (0 : γ)
⊢ (HMul.hMul (α := Matrix (m × n) (m × n) γ) (β := Matrix (m × n) (m × n) γ)
        ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) A :
                Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
              (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
            1 :
          Matrix (m × n) (m × n) γ)
        (((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) 1 :
              (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
            B :
          Matrix (m × n) (m × n) γ)).det =
    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))

Tactic:
rw [det_mul, ← diagonal_one, ← diagonal_one, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_right _ fun _ => _, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_left _ fun _ => _, det_reindex_self]

Premises used: Matrix.kroneckerMap_diagonal_right, Matrix.kroneckerMapBilinear_apply_apply, Matrix.det_mul, Matrix.diagonal_one, Matrix.det_reindex_self, Matrix.kroneckerMap_diagonal_left
-- 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:
LinearMap.map_zero₂ _ _

Premises used: LinearMap.map_zero₂