-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : FinitePresentation R M
inst_12 : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • (↑l : M' →ₗ[R] N') ∘ₗ f
this :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' : M' →ₗ[R] N') : (a : M') → N')
obtain :
  ∀ (r : R) (hr : r ∈ S)
    (hr' :
      ∀ (t : R),
        r ∣ t →
          Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) N)
            (⇑((LocalizedModule.map (Submonoid.powers t) :
                      (a : M →ₗ[R] N) →
                        LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                          LocalizedModule (Submonoid.powers t) N)
                    l' :
                  LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                    (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) N)) :
              (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) N)),
    ∃ (r : R) (hr : r ∈ S) (l' :
      LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r N),
      LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ
          (↑R :
              {S : Type u_3} →
                {M : Type (max u_3 u_4)} →
                  {M₂ : Type (max u_3 u_5)} →
                    [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₂)
            (↑l' : LocalizedModule.Away r M →ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r N) =
        (↑l : M' →ₗ[R] N') ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
⊢ ∃ (r : R) (hr : r ∈ S) (l' : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r N),
    LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ
        (↑R :
            {S : Type u_3} →
              {M : Type (max u_3 u_4)} →
                {M₂ : Type (max u_3 u_5)} →
                  [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₂)
          (↑l' : LocalizedModule.Away r M →ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r N) =
      (↑l : M' →ₗ[R] N') ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯

Tactic:
obtain ⟨r, hr, hr'⟩ := exists_bijective_map_powers S f g _ this

Premises used: exists_bijective_map_powers