awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
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'
⊢ (((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')
have 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') : γ) :
    γ)
Tactic: simp only [kroneckerMapBilinear_apply_apply, mul_apply, ← Finset.univ_product_univ,
    Finset.sum_product, kroneckerMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
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'
⊢ 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') : γ) :
      γ)
have 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') : γ) :
    γ)
Tactic: simp_rw [map_sum f, LinearMap.sum_apply, map_sum, h_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
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') : γ) :
      γ)
⊢ 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') : γ) :
      γ)
have 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') : γ))
Tactic: simp_rw [map_sum f, LinearMap.sum_apply, map_sum, h_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
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') : γ))
⊢ 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') : γ) :
      γ)
have 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') : γ))
Tactic: simp_rw [map_sum f, LinearMap.sum_apply, map_sum, h_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
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 : AddCommMonoid α
inst_5 : AddCommMonoid β
inst_6 : AddCommMonoid γ
inst_7 : Module R α
inst_8 : Module R γ
inst_9 : Module S β
inst_10 : Module S γ
inst_11 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
A : Matrix m m α
B : Matrix n n β
⊢ Eq.{u_7 + 1} (α := γ)
    (trace (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) γ)
          B) :
      γ)
    ((((f : (a : α) → β →ₗ[S] γ) A.trace : β →ₗ[S] γ) : (a : β) → γ) B.trace : γ)
have simp_rw : Eq.{u_7 + 1} (α := γ)
  (∑ i : m × n,
      diag
        ((((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) γ)
          B)
        i :
    γ)
  (((f : (a : α) → β →ₗ[S] γ) (∑ i : m, A.diag i) : (a : β) → γ) (∑ i : n, B.diag i) : γ)
Tactic: simp_rw [Matrix.trace, Matrix.diag, kroneckerMapBilinear_apply_apply, LinearMap.map_sum₂,
    map_sum, ← Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
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 : AddCommMonoid α
inst_5 : AddCommMonoid β
inst_6 : AddCommMonoid γ
inst_7 : Module R α
inst_8 : Module R γ
inst_9 : Module S β
inst_10 : Module S γ
inst_11 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
A : Matrix m m α
B : Matrix n n β
simp_rw :
  Eq.{u_7 + 1} (α := γ)
    (∑ i : m × n,
        diag
          ((((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) γ)
            B)
          i :
      γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ i : m, A.diag i) : (a : β) → γ) (∑ i : n, B.diag i) : γ)
⊢ Eq.{u_7 + 1} (α := γ)
    (trace (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) γ)
          B) :
      γ)
    ((((f : (a : α) → β →ₗ[S] γ) A.trace : β →ₗ[S] γ) : (a : β) → γ) B.trace : γ)
have simp_rw₁ : Eq.{u_7 + 1} (α := γ)
  (∑ x : 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) γ)
        B x x :
    γ)
  (((f : (a : α) → β →ₗ[S] γ) (∑ x : m, A x x) : (a : β) → γ) (∑ x : n, B x x) : γ)
Tactic: simp_rw [Matrix.trace, Matrix.diag, kroneckerMapBilinear_apply_apply, LinearMap.map_sum₂,
    map_sum, ← Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
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 : AddCommMonoid α
inst_5 : AddCommMonoid β
inst_6 : AddCommMonoid γ
inst_7 : Module R α
inst_8 : Module R γ
inst_9 : Module S β
inst_10 : Module S γ
inst_11 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
A : Matrix m m α
B : Matrix n n β
simp_rw :
  Eq.{u_7 + 1} (α := γ)
    (∑ i : m × n,
        diag
          ((((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) γ)
            B)
          i :
      γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ i : m, A.diag i) : (a : β) → γ) (∑ i : n, B.diag i) : γ)
simp_rw₁ :
  Eq.{u_7 + 1} (α := γ)
    (∑ x : 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) γ)
          B x x :
      γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ x : m, A x x) : (a : β) → γ) (∑ x : n, B x x) : γ)
⊢ Eq.{u_7 + 1} (α := γ)
    (trace (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) γ)
          B) :
      γ)
    ((((f : (a : α) → β →ₗ[S] γ) A.trace : β →ₗ[S] γ) : (a : β) → γ) B.trace : γ)
have simp_rw₂ : Eq.{u_7 + 1} (α := γ)
  (∑ x : m × n,
      kroneckerMap (fun (r : α) (s : β) ↦ (((f : (a : α) → β →ₗ[S] γ) r : β →ₗ[S] γ) : (a : β) → γ) s) A B x x :
    γ)
  (((f : (a : α) → β →ₗ[S] γ) (∑ x : m, A x x) : (a : β) → γ) (∑ x : n, B x x) : γ)
Tactic: simp_rw [Matrix.trace, Matrix.diag, kroneckerMapBilinear_apply_apply, LinearMap.map_sum₂,
    map_sum, ← Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
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 : AddCommMonoid α
inst_5 : AddCommMonoid β
inst_6 : AddCommMonoid γ
inst_7 : Module R α
inst_8 : Module R γ
inst_9 : Module S β
inst_10 : Module S γ
inst_11 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
A : Matrix m m α
B : Matrix n n β
simp_rw :
  Eq.{u_7 + 1} (α := γ)
    (∑ i : m × n,
        diag
          ((((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) γ)
            B)
          i :
      γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ i : m, A.diag i) : (a : β) → γ) (∑ i : n, B.diag i) : γ)
simp_rw₁ :
  Eq.{u_7 + 1} (α := γ)
    (∑ x : 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) γ)
          B x x :
      γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ x : m, A x x) : (a : β) → γ) (∑ x : n, B x x) : γ)
simp_rw₂ :
  Eq.{u_7 + 1} (α := γ)
    (∑ x : m × n,
        kroneckerMap (fun (r : α) (s : β) ↦ (((f : (a : α) → β →ₗ[S] γ) r : β →ₗ[S] γ) : (a : β) → γ) s) A B x x :
      γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ x : m, A x x) : (a : β) → γ) (∑ x : n, B x x) : γ)
⊢ Eq.{u_7 + 1} (α := γ)
    (trace (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) γ)
          B) :
      γ)
    ((((f : (a : α) → β →ₗ[S] γ) A.trace : β →ₗ[S] γ) : (a : β) → γ) B.trace : γ)
have simp_rw₃ : Eq.{u_7 + 1} (α := γ)
  (∑ x : m × n,
    kroneckerMap (fun (r : α) (s : β) ↦ (((f : (a : α) → β →ₗ[S] γ) r : β →ₗ[S] γ) : (a : β) → γ) s) A B x x)
  (∑ i : m, (((f : (a : α) → β →ₗ[S] γ) (A i i) : β →ₗ[S] γ) : (a : β) → γ) (∑ x : n, B x x))
Tactic: simp_rw [Matrix.trace, Matrix.diag, kroneckerMapBilinear_apply_apply, LinearMap.map_sum₂,
    map_sum, ← Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
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 : AddCommMonoid α
inst_5 : AddCommMonoid β
inst_6 : AddCommMonoid γ
inst_7 : Module R α
inst_8 : Module R γ
inst_9 : Module S β
inst_10 : Module S γ
inst_11 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
A : Matrix m m α
B : Matrix n n β
simp_rw :
  Eq.{u_7 + 1} (α := γ)
    (∑ i : m × n,
        diag
          ((((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) γ)
            B)
          i :
      γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ i : m, A.diag i) : (a : β) → γ) (∑ i : n, B.diag i) : γ)
simp_rw₁ :
  Eq.{u_7 + 1} (α := γ)
    (∑ x : 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) γ)
          B x x :
      γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ x : m, A x x) : (a : β) → γ) (∑ x : n, B x x) : γ)
simp_rw₂ :
  Eq.{u_7 + 1} (α := γ)
    (∑ x : m × n,
        kroneckerMap (fun (r : α) (s : β) ↦ (((f : (a : α) → β →ₗ[S] γ) r : β →ₗ[S] γ) : (a : β) → γ) s) A B x x :
      γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ x : m, A x x) : (a : β) → γ) (∑ x : n, B x x) : γ)
simp_rw₃ :
  Eq.{u_7 + 1} (α := γ)
    (∑ x : m × n,
      kroneckerMap (fun (r : α) (s : β) ↦ (((f : (a : α) → β →ₗ[S] γ) r : β →ₗ[S] γ) : (a : β) → γ) s) A B x x)
    (∑ i : m, (((f : (a : α) → β →ₗ[S] γ) (A i i) : β →ₗ[S] γ) : (a : β) → γ) (∑ x : n, B x x))
⊢ Eq.{u_7 + 1} (α := γ)
    (trace (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) γ)
          B) :
      γ)
    ((((f : (a : α) → β →ₗ[S] γ) A.trace : β →ₗ[S] γ) : (a : β) → γ) B.trace : γ)
have simp_rw₄ : Eq.{u_7 + 1} (α := γ)
  (∑ x : m × n,
    kroneckerMap (fun (r : α) (s : β) ↦ (((f : (a : α) → β →ₗ[S] γ) r : β →ₗ[S] γ) : (a : β) → γ) s) A B x x)
  (∑ x : m, ∑ x_1 : n, (((f : (a : α) → β →ₗ[S] γ) (A x x) : β →ₗ[S] γ) : (a : β) → γ) (B x_1 x_1))
Tactic: simp_rw [Matrix.trace, Matrix.diag, kroneckerMapBilinear_apply_apply, LinearMap.map_sum₂,
    map_sum, ← Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
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 : AddCommMonoid α
inst_5 : AddCommMonoid β
inst_6 : AddCommMonoid γ
inst_7 : Module R α
inst_8 : Module R γ
inst_9 : Module S β
inst_10 : Module S γ
inst_11 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
A : Matrix m m α
B : Matrix n n β
simp_rw :
  Eq.{u_7 + 1} (α := γ)
    (∑ i : m × n,
        diag
          ((((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) γ)
            B)
          i :
      γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ i : m, A.diag i) : (a : β) → γ) (∑ i : n, B.diag i) : γ)
simp_rw₁ :
  Eq.{u_7 + 1} (α := γ)
    (∑ x : 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) γ)
          B x x :
      γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ x : m, A x x) : (a : β) → γ) (∑ x : n, B x x) : γ)
simp_rw₂ :
  Eq.{u_7 + 1} (α := γ)
    (∑ x : m × n,
        kroneckerMap (fun (r : α) (s : β) ↦ (((f : (a : α) → β →ₗ[S] γ) r : β →ₗ[S] γ) : (a : β) → γ) s) A B x x :
      γ)
    (((f : (a : α) → β →ₗ[S] γ) (∑ x : m, A x x) : (a : β) → γ) (∑ x : n, B x x) : γ)
simp_rw₃ :
  Eq.{u_7 + 1} (α := γ)
    (∑ x : m × n,
      kroneckerMap (fun (r : α) (s : β) ↦ (((f : (a : α) → β →ₗ[S] γ) r : β →ₗ[S] γ) : (a : β) → γ) s) A B x x)
    (∑ i : m, (((f : (a : α) → β →ₗ[S] γ) (A i i) : β →ₗ[S] γ) : (a : β) → γ) (∑ x : n, B x x))
simp_rw₄ :
  Eq.{u_7 + 1} (α := γ)
    (∑ x : m × n,
      kroneckerMap (fun (r : α) (s : β) ↦ (((f : (a : α) → β →ₗ[S] γ) r : β →ₗ[S] γ) : (a : β) → γ) s) A B x x)
    (∑ x : m, ∑ x_1 : n, (((f : (a : α) → β →ₗ[S] γ) (A x x) : β →ₗ[S] γ) : (a : β) → γ) (B x_1 x_1))
⊢ Eq.{u_7 + 1} (α := γ)
    (trace (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) γ)
          B) :
      γ)
    ((((f : (a : α) → β →ₗ[S] γ) A.trace : β →ₗ[S] γ) : (a : β) → γ) B.trace : γ)
have simp_rw₅ : Eq.{u_7 + 1} (α := γ)
  (∑ x ∈ SProd.sprod (α := Finset m) (β := Finset n) Finset.univ Finset.univ,
    kroneckerMap (fun (r : α) (s : β) ↦ (((f : (a : α) → β →ₗ[S] γ) r : β →ₗ[S] γ) : (a : β) → γ) s) A B x x)
  (∑ x : m, ∑ x_1 : n, (((f : (a : α) → β →ₗ[S] γ) (A x x) : β →ₗ[S] γ) : (a : β) → γ) (B x_1 x_1))
Tactic: simp_rw [Matrix.trace, Matrix.diag, kroneckerMapBilinear_apply_apply, LinearMap.map_sum₂,
    map_sum, ← Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply]