-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
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
⊢ 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)
have 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)
              sorry)
            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)) sorry) :
            (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) sorry)
            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]