-- 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))
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))
⊢ 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,
    ∑ y : n,
      kroneckerMap (fun (r : α) (s : β) ↦ (((f : (a : α) → β →ₗ[S] γ) r : β →ₗ[S] γ) : (a : β) → γ) s) A B (x, y)
        (x, y))
  (∑ 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]