-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst_4 : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
i : ι
rw rw₁ rw₂ rw₃ :
  ∀ (j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
      ((((b.repr : (a : V) → ι →₀ R)
                (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
                  ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
                  ((b : (a : ι) → V) i : V)) :
              ι →₀ R) :
            (a : ι) → R)
          j :
        R)
rw₄ :
  ∀ (j : ι)
    (h :
      ∀ (v : V),
        ∃ (x : R) (x_1 : R) (_ : x • v + HSMul.hSMul (β := V) x_1 ((f : (a : V) → V) v : V) = 0), ¬(x = 0 ∧ x_1 = 0)),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
      ((((b.repr : (a : V) → ι →₀ R)
                (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
                  ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
                  ((b : (a : ι) → V) i : V)) :
              ι →₀ R) :
            (a : ι) → R)
          j :
        R)
rw₅ :
  ∀ (j : ι)
    (h :
      ∀ (v : V),
        ∃ (x : R) (x_1 : R) (_ : x • v + HSMul.hSMul (β := V) x_1 ((f : (a : V) → V) v : V) = 0), ¬(x = 0 ∧ x_1 = 0))
    (s t : R)
    (h :
      HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) +
          HSMul.hSMul (β := V) t ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) =
        0)
    (h' : ¬(s = 0 ∧ t = 0)),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
      ((((b.repr : (a : V) → ι →₀ R)
                (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
                  ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R)
                  ((b : (a : ι) → V) i : V)) :
              ι →₀ R) :
            (a : ι) → R)
          j :
        R)
⊢ (f : (a : V) → V) ((b : (a : ι) → V) i : V) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V)
      ((b.coord i : (a : V) → R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) : R) ((b : (a : ι) → V) i : V)
have rw₆ : ∀ (j : ι)
  (h :
    ∀ (v : V),
      ∃ (x : R) (x_1 : R) (_ : x • v + HSMul.hSMul (β := V) x_1 ((f : (a : V) → V) v : V) = 0), ¬(x = 0 ∧ x_1 = 0))
  (s t : R)
  (h :
    HSMul.hSMul (β := V) s ((b : (a : ι) → V) i : V) +
        HSMul.hSMul (β := V) t ((f : (a : V) → V) ((b : (a : ι) → V) i : V) : V) =
      0)
  (h' : ¬(s = 0 ∧ t = 0)),
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) j : R)
    (if i = j then
        (((b.repr : (a : V) → ι →₀ R) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) i
      else 0 :
      R)
Tactic: classical
    rw [b.ext_elem_iff]
    intro j
    simp only [LinearIndependent.pair_iff, not_forall] at h
    obtain ⟨s, t, ⟨h, h'⟩⟩ := h (b i)
    simp only [Basis.coord_apply, _root_.map_smul, Basis.repr_self, smul_single,
      smul_eq_mul, mul_one, Finsupp.single_apply]
    split_ifs with hj
    · simp [hj]
    · have : t = 0 ∨ b.repr (f (b i)) j = 0 := by
        rw [b.ext_elem_iff] at h
        simpa [single_eq_of_ne' hj] using h j
      apply Or.resolve_left this
      contrapose h'
      refine ⟨?_, h'⟩
      simp only [h', zero_smul, add_zero] at h
      contrapose hj
      apply b.linearIndependent.eq_of_smul_apply_eq_smul_apply s 0 i j hj
      simpa using h
Cleared hypotheses: h