-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
mpr :
  (M.map (⇑(algebraMap A K) : (a : A) → K) *ᵥ
        Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑(algebraMap A K) : (a : A) → K) fun (i : n) ↦ f (v i) ⋯)
      i =
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i
mpr₁ :
  ((fun (j : n) ↦ M.map (⇑(algebraMap A K) : (a : A) → K) i j) ⬝ᵥ
      Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑(algebraMap A K) : (a : A) → K) fun (i : n) ↦ f (v i) ⋯) =
    (fun (j : n) ↦ (RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M i j) ⬝ᵥ
      HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v
mpr₂ :
  Eq.{u_5 + 1} (α := K)
    (∑ x : n,
      HMul.hMul (α := K) (M.map (⇑(algebraMap A K) : (a : A) → K) i x)
        (Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑(algebraMap A K) : (a : A) → K) (fun (i : n) ↦ f (v i) ⋯)
          x))
    (∑ x : n,
      HMul.hMul (α := K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M i x : K)
        (HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v x))
mpr₃ :
  Eq.{u_5 + 1} (α := K)
    (∑ x : n,
      HMul.hMul (α := K) (β := K) (M.map (⇑(algebraMap A K) : (a : A) → K) i x : K)
        ((algebraMap A K : (a : A) → K) (f (v x) ⋯) : K))
    (∑ x : n,
      HMul.hMul (α := K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M i x : K)
        (HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v x))
⊢ (algebraMap A K : (a : A) → K) ((M *ᵥ fun (i : n) ↦ f (v i) ⋯) i) =
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i
have mpr₄ : Eq.{u_5 + 1} (α := K) (∑ x : n, M.map (⇑(algebraMap A K) : (a : A) → K) i x * b • v x)
  (∑ x : n,
    HMul.hMul (α := K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M i x : K)
      (HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v x))
Tactic: simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf,
          RingHom.mapMatrix_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_def]