-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
Goal:
R : Type u_1
Rₛ : Type u_2
inst : CommSemiring R
S : Submonoid R
inst_1 : CommSemiring Rₛ
inst_2 : Algebra R Rₛ
inst_3 : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid Mₛ
inst_7 : Module R Mₛ
inst_8 : Module Rₛ Mₛ
inst_9 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_10 : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i_1 i : ι
rw :
  Eq (α := ι →₀ Rₛ)
    (Function.comp (α := M) (β := Mₛ)
        (⇑((↑R :
                {S : Type u_2} →
                  {M : Type u_4} →
                    {M₂ : Type (max u_2 u_5)} →
                      [inst : Semiring R] →
                        [inst_11 : Semiring S] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module R M] →
                                [inst_15 : Module R M₂] →
                                  [inst_16 : Module S M] →
                                    [inst_17 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (↑(repr (ofIsLocalizedModule Rₛ S f b)) : Mₛ →ₗ[Rₛ] ι →₀ Rₛ)) :
          (a : Mₛ) → ι →₀ Rₛ)
        ((⇑f : (a : M) → Mₛ) : (a : M) → Mₛ) ((b : (a : ι) → M) i : M) :
      ι →₀ Rₛ)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ Rₛ)
        ((b : (a : ι) → M) i) :
      ι →₀ Rₛ)
rw₁ :
  Eq (α := ι →₀ Rₛ)
    (((↑R :
              {S : Type u_2} →
                {M : Type u_4} →
                  {M₂ : Type (max u_2 u_5)} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (↑(repr (ofIsLocalizedModule Rₛ S f b)) : Mₛ →ₗ[Rₛ] ι →₀ Rₛ) :
          (a : Mₛ) → ι →₀ Rₛ)
        ((f : (a : M) → Mₛ) ((b : (a : ι) → M) i : M)) :
      ι →₀ Rₛ)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ Rₛ)
        ((b : (a : ι) → M) i) :
      ι →₀ Rₛ)
rw₂ :
  Eq (α := ι →₀ Rₛ)
    (((↑(repr (ofIsLocalizedModule Rₛ S f b)) : Mₛ →ₗ[Rₛ] ι →₀ Rₛ) : (a : Mₛ) → ι →₀ Rₛ)
        ((f : (a : M) → Mₛ) ((b : (a : ι) → M) i : M)) :
      ι →₀ Rₛ)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ Rₛ)
        ((b : (a : ι) → M) i) :
      ι →₀ Rₛ)
rw₃ :
  Eq (α := ι →₀ Rₛ)
    ((repr (ofIsLocalizedModule Rₛ S f b) : (a : Mₛ) → ι →₀ Rₛ) ((f : (a : M) → Mₛ) ((b : (a : ι) → M) i : M)) :
      ι →₀ Rₛ)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ Rₛ)
        ((b : (a : ι) → M) i) :
      ι →₀ Rₛ)
rw₄ :
  Eq (α := ι →₀ Rₛ)
    ((repr (ofIsLocalizedModule Rₛ S f b) : (a : Mₛ) → ι →₀ Rₛ) ((ofIsLocalizedModule Rₛ S f b : (a : ι) → Mₛ) i) :
      ι →₀ Rₛ)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ Rₛ)
        ((b : (a : ι) → M) i) :
      ι →₀ Rₛ)
rw₅ :
  Eq (α := ι →₀ Rₛ) (Finsupp.single i 1)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ Rₛ)
      ((b : (a : ι) → M) i))
rw₆ :
  Eq (α := ι →₀ Rₛ) (Finsupp.single i 1)
    (Function.comp (α := M) (β := ι →₀ R)
      (⇑(Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) : (a : ι →₀ R) → ι →₀ Rₛ)
      ((⇑(↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) : (a : M) → ι →₀ R) ((b : (a : ι) → M) i : M))
rw₇ :
  Eq (α := ι →₀ Rₛ) (Finsupp.single i 1)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) : (a : ι →₀ R) → ι →₀ Rₛ)
      (((↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) ((b : (a : ι) → M) i)))
⊢ Eq (α := ι →₀ Rₛ)
    (((↑R :
                {S : Type u_2} →
                  {M : Type u_4} →
                    {M₂ : Type (max u_2 u_5)} →
                      [inst : Semiring R] →
                        [inst_11 : Semiring S] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module R M] →
                                [inst_15 : Module R M₂] →
                                  [inst_16 : Module S M] →
                                    [inst_17 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (↑(repr (ofIsLocalizedModule Rₛ S f b)) : Mₛ →ₗ[Rₛ] ι →₀ Rₛ) ∘ₗ
            f :
          (a : M) → ι →₀ Rₛ)
        ((b : (a : ι) → M) i) :
      ι →₀ Rₛ)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ Rₛ)
        ((b : (a : ι) → M) i) :
      ι →₀ Rₛ)
have rw₈ : Eq (α := ι →₀ Rₛ) (Finsupp.single i 1)
  ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) : (a : ι →₀ R) → ι →₀ Rₛ)
    ((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i)))
Tactic: rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.coe_restrictScalars,
    LinearEquiv.coe_coe, ← b.ofIsLocalizedModule_apply Rₛ S f, repr_self, LinearMap.coe_comp,
    Function.comp_apply, LinearEquiv.coe_coe, repr_self, Finsupp.mapRange.linearMap_apply,
    Finsupp.mapRange_single, Algebra.linearMap_apply, map_one]