-- Mathlib/Algebra/Module/FinitePresentation.lean
/--
Let `M` be a finite `R`-module, and `N` be a finitely presented `R`-module.
If `l : M →ₗ[R] N` is a linear map whose localization at `S : Submonoid R` is bijective,
then `l` is already bijective under the localization at some `r ∈ S`.
-/
lemma exists_bijective_map_powers [Module.Finite R M] [Module.FinitePresentation R N]
    (l : M →ₗ[R] N) (hf : Function.Bijective (IsLocalizedModule.map S f g l)) :
    ∃ r, r ∈ S ∧ ∀ t, r ∣ t → Function.Bijective (LocalizedModule.map (.powers t) l)

Proof state:
case a
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✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id)
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • s₀ • LinearMap.id
t : R
ht : ↑s₀ * ↑s₁ * ↑s₂ ∣ t
Rₛ : Type u_3 := Localization (Submonoid.powers t)
lₛ : LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) N :=
  (LocalizedModule.map (Submonoid.powers t)) l
hu₀ : IsUnit ((algebraMap R Rₛ) ↑s₀)
hu₁ : IsUnit ((algebraMap R Rₛ) ↑s₁)
hu₂ : IsUnit ((algebraMap R Rₛ) ↑s₂)
lₛ' : LocalizedModule (Submonoid.powers t) N →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) M :=
  (LocalizedModule.map (Submonoid.powers t)) l'
⊢ ((algebraMap Rₛ
          (Module.End Rₛ
            (LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
              LocalizedModule (Submonoid.powers t) M)))
        ((algebraMap R Rₛ) ↑s₂))
      ((↑hu₀.unit⁻¹ • lₛ') ∘ₗ lₛ) =
    ((algebraMap Rₛ
          (Module.End Rₛ
            (LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
              LocalizedModule (Submonoid.powers t) M)))
        ((algebraMap R Rₛ) ↑s₂))
      LinearMap.id

Tactic:
apply ((Module.End_isUnit_iff _).mp (hu₀.map (algebraMap Rₛ (Module.End Rₛ _)))).1

Result:
case a.a
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✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id)
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • s₀ • LinearMap.id
t : R
ht : ↑s₀ * ↑s₁ * ↑s₂ ∣ t
Rₛ : Type u_3 := Localization (Submonoid.powers t)
lₛ : LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) N :=
  (LocalizedModule.map (Submonoid.powers t)) l
hu₀ : IsUnit ((algebraMap R Rₛ) ↑s₀)
hu₁ : IsUnit ((algebraMap R Rₛ) ↑s₁)
hu₂ : IsUnit ((algebraMap R Rₛ) ↑s₂)
lₛ' : LocalizedModule (Submonoid.powers t) N →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) M :=
  (LocalizedModule.map (Submonoid.powers t)) l'
⊢ ((algebraMap Rₛ
          (Module.End Rₛ
            (LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
              LocalizedModule (Submonoid.powers t) M)))
        ((algebraMap R Rₛ) ↑s₀))
      (((algebraMap Rₛ
            (Module.End Rₛ
              (LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                LocalizedModule (Submonoid.powers t) M)))
          ((algebraMap R Rₛ) ↑s₂))
        ((↑hu₀.unit⁻¹ • lₛ') ∘ₗ lₛ)) =
    ((algebraMap Rₛ
          (Module.End Rₛ
            (LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
              LocalizedModule (Submonoid.powers t) M)))
        ((algebraMap R Rₛ) ↑s₀))
      (((algebraMap Rₛ
            (Module.End Rₛ
              (LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                LocalizedModule (Submonoid.powers t) M)))
          ((algebraMap R Rₛ) ↑s₂))
        LinearMap.id)

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✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id)
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • s₀ • LinearMap.id
t : R
ht : ↑s₀ * ↑s₁ * ↑s₂ ∣ t
Rₛ : Type u_3 := Localization (Submonoid.powers t)
lₛ : LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) N :=
  (LocalizedModule.map (Submonoid.powers t)) l
hu₀ : IsUnit ((algebraMap R Rₛ) ↑s₀)
hu₁ : IsUnit ((algebraMap R Rₛ) ↑s₁)
hu₂ : IsUnit ((algebraMap R Rₛ) ↑s₂)
lₛ' : LocalizedModule (Submonoid.powers t) N →ₗ[Localization (Submonoid.powers t)]
  LocalizedModule (Submonoid.powers t) M :=
  (LocalizedModule.map (Submonoid.powers t)) l'
H_left : (↑hu₀.unit⁻¹ • lₛ') ∘ₗ lₛ = LinearMap.id
H_right : lₛ ∘ₗ (↑hu₀.unit⁻¹ • lₛ') = LinearMap.id
eₛ : LocalizedModule (Submonoid.powers t) M ≃ₗ[Rₛ] LocalizedModule (Submonoid.powers t) N :=
  let __spread.0 := lₛ;
  { toLinearMap := __spread.0, invFun := ↑hu₀.unit⁻¹ • ⇑lₛ', left_inv := ⋯, right_inv := ⋯ }
⊢ Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l)

Tactic:
exact eₛ.bijective

Result:
no goals

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✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
⊢ s₀ • (↑e.symm ∘ₗ ↑e) ∘ₗ f = f ∘ₗ (s₀ • LinearMap.id)

Tactic:
simp [LinearMap.comp_smul]

Result:
no goals