awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h :
  (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' ∘ₗ f =
    (HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')) ∘ₗ f
⊢ (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' = HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')

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

Premises used: IsLocalizedModule.ext, IsLocalizedModule.map_units
-- 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
apply :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := N') (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' ∘ₗ f : (a : M) → N') x : N')
      (((HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')) ∘ₗ f : (a : M) → N') x : N')
⊢ (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' ∘ₗ f =
    (HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')) ∘ₗ f

Tactic:
apply LinearMap.ext fun x ↦ ?_

Premises used: LinearMap.ext
-- 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
x : M
simp :
  Eq.{u_2 + 1} (α := N') ((g : (a : N) → N') ((l' : (a : M) → N) x : N) : N')
    ((HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id : (a : N') → N')
        (((↑l : M' →ₗ[R] N') : (a : M') → N') ((f : (a : M) → M') x : M') : N') :
      N')
⊢ Eq.{u_2 + 1} (α := N') (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' ∘ₗ f : (a : M) → N') x : N')
    (((HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')) ∘ₗ f : (a : M) → N') x : N')

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, IsLocalizedModule.map_apply]

Premises used: IsLocalizedModule.map_apply, LinearMap.coe_comp, Function.comp_apply
-- 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
x : M
rw :
  Eq.{u_2 + 1} (α := N') ((s • (↑l : M' →ₗ[R] N') ∘ₗ f : (a : M) → N') x : N')
    ((HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id : (a : N') → N')
        (((↑l : M' →ₗ[R] N') : (a : M') → N') ((f : (a : M) → M') x : M') : N') :
      N')
⊢ Eq.{u_2 + 1} (α := N') ((g : (a : N) → N') ((l' : (a : M) → N) x : N) : N')
    ((HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id : (a : N') → N')
        (((↑l : M' →ₗ[R] N') : (a : M') → N') ((f : (a : M) → M') x : M') : N') :
      N')

Tactic:
rw [← LinearMap.comp_apply, H]

Premises used: LinearMap.comp_apply
-- 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
x : M
⊢ Eq.{u_2 + 1} (α := N') ((s • (↑l : M' →ₗ[R] N') ∘ₗ f : (a : M) → N') x : N')
    ((HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id : (a : N') → N')
        (((↑l : M' →ₗ[R] N') : (a : M') → N') ((f : (a : M) → M') x : M') : N') :
      N')

Tactic:
simp
-- 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
⊢ (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' = HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')

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]
      rw [← LinearMap.comp_apply, H]
      simp
-- 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 :
  (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' = HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')
rw :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑(HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')) : (a : M') → N')
⊢ 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')

Tactic:
rw [this]
-- 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 :
  (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' = HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑(HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')) : (a : M') → N')

Tactic:
((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units g s)).comp l.bijective

Premises used: LinearEquiv.bijective, Module.End.isUnit_iff, Iff.mp, IsLocalizedModule.map_units, Function.Bijective.comp
-- 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 :
  (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' = HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑(HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')) : (a : M') → N')

Tactic:
exact ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units g s)).comp l.bijective

Premises used: LinearEquiv.bijective, Module.End.isUnit_iff, Iff.mp, IsLocalizedModule.map_units, Function.Bijective.comp
-- 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
⊢ 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')

Tactic:
have : Function.Bijective (IsLocalizedModule.map S f g l') := by
    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]
      rw [← LinearMap.comp_apply, H]
      simp
    rw [this]
    exact ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units g s)).comp l.bijective
-- 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')
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)
rs : Submonoid R := Submonoid.powers (r * (↑s : R))
Rᵣₛ : Type u_3 := Localization (M := R) rs
⊢ IsUnit (M := Rᵣₛ) ((algebraMap R Rᵣₛ : (a : R) → Rᵣₛ) (↑s : R) : Rᵣₛ)

Tactic:
have hsu : IsUnit (algebraMap R Rᵣₛ s) := isUnit_of_dvd_unit
      (hu := IsLocalization.map_units (M := rs) Rᵣₛ ⟨_, Submonoid.mem_powers _⟩)
      (map_dvd (algebraMap R Rᵣₛ) ⟨r, mul_comm _ _⟩)
-- 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')
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)
rs : Submonoid R := Submonoid.powers (r * (↑s : R))
Rᵣₛ : Type u_3 := Localization (M := R) rs
hsu : IsUnit (M := Rᵣₛ) ((algebraMap R Rᵣₛ : (a : R) → Rᵣₛ) (↑s : R) : Rᵣₛ)
⊢ Function.Bijective (α := LocalizedModule rs M) (β := LocalizedModule rs N)
    (⇑(HSMul.hSMul (β :=
          LinearMap (R := Localization (M := R) rs) (RingHom.id (Localization (M := R) rs)) (LocalizedModule rs M)
            (LocalizedModule rs N))
          (↑hsu.unit⁻¹ : Rᵣₛ)
          ((LocalizedModule.map rs : (a : M →ₗ[R] N) → LocalizedModule rs M →ₗ[Localization rs] LocalizedModule rs N)
              l' :
            LinearMap (R := Localization (M := R) rs) (RingHom.id (Localization (M := R) rs)) (LocalizedModule rs M)
              (LocalizedModule rs N))) :
      (a : LocalizedModule rs M) → LocalizedModule rs N)

Tactic:
have : Function.Bijective ((hsu.unit⁻¹).1 • LocalizedModule.map rs l') :=
    ((Module.End.isUnit_iff _).mp ((hsu.unit⁻¹).isUnit.map (algebraMap _ (End Rᵣₛ
      (LocalizedModule rs N))))).comp (hr' (r * s) (dvd_mul_right _ _))
-- 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_1 :
  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')
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)
rs : Submonoid R := Submonoid.powers (r * (↑s : R))
Rᵣₛ : Type u_3 := Localization (M := R) rs
hsu : IsUnit (M := Rᵣₛ) ((algebraMap R Rᵣₛ : (a : R) → Rᵣₛ) (↑s : R) : Rᵣₛ)
this :
  Function.Bijective (α := LocalizedModule rs M) (β := LocalizedModule rs N)
    (⇑(HSMul.hSMul (β :=
          LinearMap (R := Localization (M := R) rs) (RingHom.id (Localization (M := R) rs)) (LocalizedModule rs M)
            (LocalizedModule rs N))
          (↑hsu.unit⁻¹ : Rᵣₛ)
          ((LocalizedModule.map rs : (a : M →ₗ[R] N) → LocalizedModule rs M →ₗ[Localization rs] LocalizedModule rs N)
              l' :
            LinearMap (R := Localization (M := R) rs) (RingHom.id (Localization (M := R) rs)) (LocalizedModule rs M)
              (LocalizedModule rs N))) :
      (a : LocalizedModule rs M) → LocalizedModule rs N)
x : M
⊢ ∀ (x : M),
    (g : (a : N) → N') ((l' : (a : M) → N) x : N) =
      HSMul.hSMul (β := N') (↑s : R) ((l : (a : M') → N') ((f : (a : M) → M') x : M') : N')

Tactic:
have : ∀ x, g (l' x) = s.1 • (l (f x)) := LinearMap.congr_fun H
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
map_units :
  ∀ (x : ↥S),
    IsUnit (M := End R (M' →ₗ[R] N'))
      ((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑x : R) : End R (M' →ₗ[R] N'))
surj :
  ∀ (y : M' →ₗ[R] N'),
    ∃ (x : (M →ₗ[R] N) × ↥S), x.2 • y = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') x.1
exists_of_eq :
  ∀ {x₁ x₂ : M →ₗ[R] N},
    Eq (α := M' →ₗ[R] N') ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') x₁ : M' →ₗ[R] N')
        ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') x₂ : M' →ₗ[R] N') →
      ∃ (c : ↥S), c • x₁ = c • x₂
⊢ IsLocalizedModule S (IsLocalizedModule.map S f g)

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
s : ↥S
map_units :
  Function.Bijective (α := M' →ₗ[R] N') (β := M' →ₗ[R] N')
    (⇑((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N')) :
      (a : M' →ₗ[R] N') → M' →ₗ[R] N')
⊢ IsUnit (M := End R (M' →ₗ[R] N'))
    ((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N'))

Tactic:
rw [Module.End.isUnit_iff]

Premises used: Module.End.isUnit_iff
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
s : ↥S
⊢ Function.Bijective.{u_2 + 1, u_2 + 1} (α := N') (β := N')
    (⇑((algebraMap R (End R N') : (a : R) → End R N') (↑s : R) : End R N') : (a : N') → N')

Tactic:
have := (Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units (S := S) (f := g) s)
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
s : ↥S
this :
  Function.Bijective.{u_2 + 1, u_2 + 1} (α := N') (β := N')
    (⇑((algebraMap R (End R N') : (a : R) → End R N') (↑s : R) : End R N') : (a : N') → N')
map_units :
  Function.Injective (α := M' →ₗ[R] N') (β := M' →ₗ[R] N')
    (⇑((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N')) :
      (a : M' →ₗ[R] N') → M' →ₗ[R] N')
map_units₁ :
  Function.Surjective (α := M' →ₗ[R] N') (β := M' →ₗ[R] N')
    (⇑((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N')) :
      (a : M' →ₗ[R] N') → M' →ₗ[R] N')
⊢ Function.Bijective (α := M' →ₗ[R] N') (β := M' →ₗ[R] N')
    (⇑((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N')) :
      (a : M' →ₗ[R] N') → M' →ₗ[R] N')

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
s : ↥S
this :
  Function.Bijective.{u_2 + 1, u_2 + 1} (α := N') (β := N')
    (⇑((algebraMap R (End R N') : (a : R) → End R N') (↑s : R) : End R N') : (a : N') → N')
⊢ Function.Injective (α := M' →ₗ[R] N') (β := M' →ₗ[R] N')
    (⇑((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N')) :
      (a : M' →ₗ[R] N') → M' →ₗ[R] N')

Tactic:
fun _ _ e ↦ LinearMap.ext fun m ↦ this.left (LinearMap.congr_fun e m)

Premises used: LinearMap.ext, And.left, LinearMap.congr_fun, Function.Injective
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
s : ↥S
this :
  Function.Bijective.{u_2 + 1, u_2 + 1} (α := N') (β := N')
    (⇑((algebraMap R (End R N') : (a : R) → End R N') (↑s : R) : End R N') : (a : N') → N')
⊢ Function.Injective (α := M' →ₗ[R] N') (β := M' →ₗ[R] N')
    (⇑((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N')) :
      (a : M' →ₗ[R] N') → M' →ₗ[R] N')

Tactic:
exact fun _ _ e ↦ LinearMap.ext fun m ↦ this.left (LinearMap.congr_fun e m)

Premises used: LinearMap.ext, And.left