-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
h :
  ∀ (j' : η) (i' : ιs j'),
    Eq.{u_2 + 1} (α := R)
      (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
                (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
              (j : η) × ιs j →₀ R) :
            (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
pos :
  ∀ (j' : η) (i' : ιs j') (hj : j = j'),
    Eq.{u_2 + 1} (α := R)
      (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
                (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
              (j : η) × ιs j →₀ R) :
            (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
neg neg₁ :
  ∀ (j' : η) (i' : ιs j') (hj : ¬j = j'),
    Eq.{u_2 + 1} (α := R)
      (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
                (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
              (j : η) × ιs j →₀ R) :
            (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
neg₂ :
  ∀ (j' : η) (i' : ιs j') (hj : ¬j = j'),
    Eq.{u_2 + 1} (α := R)
      (((({ toFun := fun (f : (i : η) → Ms i) (i : η) ↦ ((s i).repr : (a : Ms i) → ιs i →₀ R) (f i), map_add' := ⋯,
                    map_smul' := ⋯,
                    invFun := fun (f : (i : η) → Finsupp.{u_5, u_2} (ιs i) R) (i : η) ↦
                      ((s i).repr.symm : (a : ιs i →₀ R) → Ms i) (f i),
                    left_inv := ⋯, right_inv := ⋯ } :
                  (a : (j : η) → Ms j) → (i : η) → ιs i →₀ R)
                (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) j' :
              Finsupp.{u_5, u_2} (ιs j') R) :
            (a : ιs j') → R)
          i' :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
neg₃ :
  ∀ (j' : η) (i' : ιs j') (hj : ¬j = j'),
    Eq.{u_2 + 1} (α := R)
      (((((s j').repr : (a : Ms j') → ιs j' →₀ R) (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i) j') :
              Finsupp.{u_5, u_2} (ιs j') R) :
            (a : ιs j') → R)
          i' :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
neg₄ :
  ∀ (j' : η) (i' : ιs j') (hj : ¬j = j'),
    Sigma.mk (β := fun (j : η) ↦ ιs j) j' i' ≠ Sigma.mk (β := fun (j : η) ↦ ιs j) j i
neg₅ : ∀ (hj : ¬j = j), False
⊢ Eq (α := (j : η) × ιs j →₀ R)
    (((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
        (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
      (j : η) × ιs j →₀ R)
    (Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (j : η) × ιs j →₀ R)

Tactic:
classical
  ext ⟨j', i'⟩
  by_cases hj : j = j'
  · subst hj
    simp only [Pi.basis, LinearEquiv.trans_apply,
      LinearEquiv.piCongrRight, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
      Basis.repr_symm_apply, LinearEquiv.coe_mk]
    symm
    simp [Finsupp.single_apply]
  simp only [Pi.basis, LinearEquiv.trans_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
    LinearEquiv.piCongrRight]
  dsimp
  rw [Pi.single_eq_of_ne (Ne.symm hj), map_zero, Finsupp.zero_apply,
    Finsupp.single_eq_of_ne]
  rintro ⟨⟩
  contradiction

Premises used: LinearEquiv.coe_mk, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply, Finsupp.single_eq_of_ne, Pi.basis, map_zero, LinearEquiv.trans_apply, Finsupp.zero_apply, LinearEquiv.piCongrRight, Finsupp.single_apply, Module.Basis.repr_symm_apply