-- Module: Mathlib.LinearAlgebra.Center
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)
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)
pos :
  ∀ (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)) (hj : i = 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) ((f : (a : V) → V) ((b : (a : ι) → V) i : V)) : ι →₀ R) : (a : ι) → R) i : R)
neg neg₁ :
  ∀ (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)) (hj : ¬i = 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)
      (0 : 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)

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

Premises used: LinearIndependent.pair_iff, zero_smul, Module.Basis.ext_elem_iff, Finsupp.single_apply, smul_eq_mul, mul_one, add_zero, Classical.not_forall, DFunLike.coe, Finsupp.smul_single, Module.Basis.coord_apply, Module.Basis.repr_self, map_smul