-- Module: Mathlib.RingTheory.Localization.Free
Goal:
R : Type u_4
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
Rₛ : Type u_3
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
inst_8 : Module Rₛ M'
inst_9 : IsScalarTower R Rₛ M'
inst_10 : IsLocalization S Rₛ
inst_11 : FinitePresentation R M
I : Type u_6
inst_12 : Finite I
b : Basis I Rₛ M'
this_1 : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)
he :
  Eq (α := LocalizedModule (Submonoid.powers r) M →ₗ[R] I →₀ Rₛ)
    (LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯ ∘ₗ
      (↑R :
          {S : Type u_4} →
            {M : Type (max u_4 u_5)} →
              {M₂ : Type (max u_4 u_6)} →
                [inst : Semiring R] →
                  [inst_13 : Semiring S] →
                    [inst_14 : AddCommMonoid M] →
                      [inst_15 : AddCommMonoid M₂] →
                        [inst_16 : Module R M] →
                          [inst_17 : Module R M₂] →
                            [inst_18 : Module S M] →
                              [inst_19 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑e : LocalizedModule.Away r M →ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)))
    ((↑(LinearEquiv.restrictScalars R b.repr) : M' →ₗ[R] I →₀ Rₛ) ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯)
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] Finsupp.{u_6, u_4} I (Localization (Submonoid.powers r)) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
i : I
this :
  Eq (α := LocalizedModule (Submonoid.powers r) (I →₀ R))
    ((e'.symm : (a : I →₀ Localization (Submonoid.powers r)) → LocalizedModule (Submonoid.powers r) (I →₀ R))
        (Finsupp.single i 1) :
      LocalizedModule (Submonoid.powers r) (I →₀ R))
    (LocalizedModule.mk (Finsupp.single i 1) 1 : LocalizedModule (Submonoid.powers r) (I →₀ R))
refine_2 :
  Eq.{u_1 + 1} (α := M')
    ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
        ((e.symm : (a : LocalizedModule.Away r (I →₀ R)) → LocalizedModule.Away r M)
            ((e'.symm : (a : I →₀ Localization (Submonoid.powers r)) → LocalizedModule (Submonoid.powers r) (I →₀ R))
              (Finsupp.single i 1)) :
          LocalizedModule.Away r M) :
      M')
    ((b : (a : I) → M') i : M')
⊢ Eq.{u_1 + 1} (α := M')
    ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
        (({
                repr :=
                  e ≪≫ₗ
                    let __spread.0 := e';
                    let __LinearMap :
                      LinearMap (R := Localization (Submonoid.powers r))
                        (RingHom.id (Localization (Submonoid.powers r))) (LocalizedModule.Away r (I →₀ R))
                        (Finsupp.{u_6, u_4} I (Localization (Submonoid.powers r))) :=
                      (↑(LinearEquiv.extendScalarsOfIsLocalization (Submonoid.powers r)
                            (Localization (Submonoid.powers r)) e') :
                        LocalizedModule (Submonoid.powers r) (I →₀ R) →ₗ[Localization (Submonoid.powers r)]
                          I →₀ Localization (Submonoid.powers r));
                    { toLinearMap := __LinearMap, invFun := __spread.0.invFun, left_inv := ⋯, right_inv := ⋯ } } :
              (a : I) → LocalizedModule.Away r M)
            i :
          LocalizedModule.Away r M) :
      M')
    ((b : (a : I) → M') i : M')

Tactic:
change LocalizedModule.lift _ _ _ (e.symm (e'.symm _)) = _

Premises used: LocalizedModule.lift, LinearEquiv.symm, DFunLike.coe