-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Module.Finite R M₁
inst_4 : Free R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : Module.Finite R M₂
inst_8 : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (Sum.{u_3, u_4} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₂)) R (M₁ × M₂) := b₁.prod b₂
rw :
  (f₁.prodMap f₂).charpoly (M := M₁ × M₂) =
    Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
        ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁) *
      f₂.charpoly
rw₁ :
  (f₁.prodMap f₂).charpoly (M := M₁ × M₂) =
    HMul.hMul (α := R[X])
      (Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
        ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁))
      (Matrix.charpoly.{u_1, u_4} (n := ChooseBasisIndex R M₂)
        ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂))
rw₂ :
  Matrix.charpoly (n := Sum.{u_3, u_4} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₂))
      ((toMatrix b b :
          (a : M₁ × M₂ →ₗ[R] M₁ × M₂) →
            Matrix (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) R)
        (f₁.prodMap f₂)) =
    HMul.hMul (α := R[X])
      (Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
        ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁))
      (Matrix.charpoly.{u_1, u_4} (n := ChooseBasisIndex R M₂)
        ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂))
rw₃ :
  Matrix.charpoly (n := Sum.{u_3, u_4} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₂))
      (fromBlocks ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁) 0
        0 ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂)) =
    HMul.hMul (α := R[X])
      (Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
        ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁))
      (Matrix.charpoly.{u_1, u_4} (n := ChooseBasisIndex R M₂)
        ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂))
⊢ (f₁.prodMap f₂).charpoly (M := M₁ × M₂) = f₁.charpoly * f₂.charpoly
have rw₄ : HMul.hMul (α := R[X])
    (Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
      ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁))
    (Matrix.charpoly.{u_1, u_4} (n := ChooseBasisIndex R M₂)
      ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂)) =
  HMul.hMul (α := R[X])
    (Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
      ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁))
    (Matrix.charpoly.{u_1, u_4} (n := ChooseBasisIndex R M₂)
      ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂))
Tactic: rw [← charpoly_toMatrix f₁ b₁, ← charpoly_toMatrix f₂ b₂, ← charpoly_toMatrix (f₁.prodMap f₂) b,
    toMatrix_prodMap b₁ b₂ f₁ f₂, Matrix.charpoly_fromBlocks_zero₁₂]