-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
inst_3 : Fintype ι
inst_4 : DecidableEq M
i : ι
bi : M
hbi : Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) bi
h :
  Eq.{u_11 + 1} (α := R)
    (((single
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                ((b : (a : ι) → M) i) ⋯)
              1 :
            Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
          (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
        ((Equiv.symm
                ((Equiv.refl M).subtypeEquiv (p :=
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M))) (q :=
                  Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ))
                  ⋯) :
              (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → (↑(range (⇑b : (a : ι) → M)) : Type u_12))
            (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
              hbi) :
          (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12)) :
      R)
    (((single
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
                ((b : (a : ι) → M) i) ⋯)
              1 :
            Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R) :
          (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → R)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
          hbi) :
      R)
⊢ Eq.{u_11 + 1} (α := R)
    ((((repr b.reindexFinsetRange : (a : M) → ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ) →₀ R)
              ((b : (a : ι) → M) i) :
            Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R) :
          (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → R)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
          hbi) :
      R)
    (((single
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
                ((b : (a : ι) → M) i) ⋯)
              1 :
            Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R) :
          (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → R)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
          hbi) :
      R)

Tactic:
rw [reindexFinsetRange, repr_reindex, Finsupp.mapDomain_equiv_apply, reindexRange_repr_self]

Premises used: Module.Basis.reindexFinsetRange, Module.Basis.reindexRange_repr_self, Module.Basis.repr_reindex, Finsupp.mapDomain_equiv_apply