-- 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 : 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 :
  Eq.{u_7 + 1} (α := γ)
    (det (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))
    (det (n := m × n)
      ((((kroneckerMapBilinear f : (a : Matrix m m α) → Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) (A * 1) :
            Matrix n n β →ₗ[S] Matrix (m × n) (m × n) γ) :
          (a : Matrix n n β) → Matrix (m × n) (m × n) γ)
        (1 * B)))
rw₁ :
  Eq.{u_7 + 1} (α := γ)
    (det (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))
    (det (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 * B)))
⊢ det (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) =
    (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
have rw₂ : Eq.{u_7 + 1} (α := γ)
  (det (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))
  (det (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))
Tactic: rw [← kroneckerMapBilinear_mul_mul f h_comm, Matrix.mul_one, Matrix.one_mul]