-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
hfv :
  HMul.hMul (α := R) (β := R) ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R) =
    0
this :
  ∀ (x : V),
    x =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
rw :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R)
      ((f : (a : V) → R)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
            ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R)
                i :
              R)
            ((b : (a : Fin (finrank R V)) → V) i : V)) :
        R)
      v =
    0
rw₁ :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R)
      ((f : (a : V) → R)
          (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
            ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R)
                i :
              R)
            ((b : (a : Fin (finrank R V)) → V) i : V)) :
        R)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)) =
    0
rw₂ :
  HSMul.hSMul (α := R) (β := R)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R) •
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V) =
    0
rw₃ :
  HMul.hMul (α := R) (β := R)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R) •
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V) =
    0
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : V) → R) x : R) v = 0
have rw₄ : HSMul.hSMul (β := V)
    (HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R))
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R))
    ((b : (a : Fin (finrank R V)) → V) i : V) =
  0
Tactic: rw [this x, this v, map_smul, smul_eq_mul, ← mul_smul, mul_assoc, hfv, mul_zero, zero_smul]