Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: 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ₛ) ↑⟨t, ⋯⟩)
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
⊢ Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l)

Tactic:
have H_right : lₛ ∘ₗ ((hu₀.unit⁻¹).1 • lₛ') = LinearMap.id := by
    apply ((Module.End.isUnit_iff _).mp (hu₁.map (algebraMap Rₛ (Module.End Rₛ _)))).1
    apply ((Module.End.isUnit_iff _).mp (hu₀.map (algebraMap Rₛ (Module.End Rₛ _)))).1
    simp only [Module.algebraMap_end_apply, algebraMap_smul, LinearMap.map_smul_of_tower]
    rw [LinearMap.comp_smul, ← smul_assoc s₀.1, Algebra.smul_def s₀.1, IsUnit.mul_val_inv, one_smul]
    apply LinearMap.restrictScalars_injective R
    apply IsLocalizedModule.ext (.powers t) (LocalizedModule.mkLinearMap (.powers t) N)
      (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap (.powers t) N))
    ext x
    have : s₁.1 • l (l' x) = s₁.1 • s₀.1 • x := congr($hs₁ x)
    simp [lₛ, lₛ', LocalizedModule.smul'_mk, this]

Goal state after:
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ₛ) ↑⟨t, ⋯⟩)
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
⊢ Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l)