-- Mathlib/Algebra/Module/FinitePresentation.lean
/--
Let `M` `N` be a finitely presented `R`-modules.
Any `Mₛ ≃ₗ[R] Nₛ` between the localizations at `S : Submonoid R` can be lifted to an
isomorphism between `Mᵣ ≃ₗ[R] Nᵣ` for some `r ∈ S`.
-/
lemma Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule
    [Module.FinitePresentation R M] [Module.FinitePresentation R N]
    (l : M' ≃ₗ[R] N') :
    ∃ (r : R) (hr : r ∈ S)
      (l' : LocalizedModule (.powers r) M ≃ₗ[Localization (.powers r)]
        LocalizedModule (.powers r) N),
      (LocalizedModule.lift (.powers r) g fun s ↦ map_units g ⟨s.1, SetLike.le_def.mp
        (Submonoid.powers_le.mpr hr) s.2⟩) ∘ₗ l'.toLinearMap =
        l ∘ₗ (LocalizedModule.lift (.powers r) f fun s ↦ map_units f ⟨s.1, SetLike.le_def.mp
        (Submonoid.powers_le.mpr hr) s.2⟩)

Proof state:
case intro.intro.intro.intro
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this✝ : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
rs : Submonoid R := Submonoid.powers (r * ↑s)
Rᵣₛ : Type u_3 := Localization rs
hsu : IsUnit ((algebraMap R Rᵣₛ) ↑s)
this : Function.Bijective ⇑(↑hsu.unit⁻¹ • (LocalizedModule.map rs) l')
⊢ LocalizedModule.lift (Submonoid.powers (r * ↑s)) g ⋯ ∘ₗ
      ↑R ↑(LinearEquiv.ofBijective (↑hsu.unit⁻¹ • (LocalizedModule.map rs) l') this) =
    ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers (r * ↑s)) f ⋯

Tactic:
apply IsLocalizedModule.ext rs (LocalizedModule.mkLinearMap rs M) fun x ↦ map_units g
  ⟨x.1, SetLike.le_def.mp (Submonoid.powers_le.mpr (mul_mem hr s.2)) x.2⟩

Result:
case intro.intro.intro.intro.h
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this✝ : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
rs : Submonoid R := Submonoid.powers (r * ↑s)
Rᵣₛ : Type u_3 := Localization rs
hsu : IsUnit ((algebraMap R Rᵣₛ) ↑s)
this : Function.Bijective ⇑(↑hsu.unit⁻¹ • (LocalizedModule.map rs) l')
⊢ (LocalizedModule.lift (Submonoid.powers (r * ↑s)) g ⋯ ∘ₗ
        ↑R ↑(LinearEquiv.ofBijective (↑hsu.unit⁻¹ • (LocalizedModule.map rs) l') this)) ∘ₗ
      LocalizedModule.mkLinearMap rs M =
    (↑l ∘ₗ LocalizedModule.lift (Submonoid.powers (r * ↑s)) f ⋯) ∘ₗ LocalizedModule.mkLinearMap rs M

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
⊢ (map S f g) l' = (s • LinearMap.id) ∘ₗ ↑l

Tactic:
apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)

Result:
case h
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
⊢ (map S f g) l' ∘ₗ f = ((s • LinearMap.id) ∘ₗ ↑l) ∘ₗ f

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
⊢ Function.Bijective ⇑((map S f g) l')

Tactic:
have : IsLocalizedModule.map S f g l' = (s • LinearMap.id) ∘ₗ l := by
  apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
  apply LinearMap.ext fun x ↦ ?_
  simp only [LinearMap.coe_comp, Function.comp_apply, IsLocalizedModule.map_apply,
    Basis.coe_repr_symm, LinearMap.coe_restrictScalars]
  rw [← LinearMap.comp_apply, H]
  simp

Result:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this : (map S f g) l' = (s • LinearMap.id) ∘ₗ ↑l
⊢ Function.Bijective ⇑((map S f g) l')

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this : (map S f g) l' = (s • LinearMap.id) ∘ₗ ↑l
⊢ Function.Bijective ⇑((map S f g) l')

Tactic:
rw [this]

Result:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this : (map S f g) l' = (s • LinearMap.id) ∘ₗ ↑l
⊢ Function.Bijective ⇑((s • LinearMap.id) ∘ₗ ↑l)