awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
⊢ Submonoid.powers r ≤ S

Tactic:
simpa [Submonoid.powers_le]

Premises used: Submonoid.powers_le
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
⊢ Submonoid.powers r ≤ S

Tactic:
have hrp' : .powers r ≤ S := by simpa [Submonoid.powers_le]
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
hrp' : Submonoid.powers r ≤ S
⊢ ∃ r ∈ S, IsLocalizedModule.Away r f

Tactic:
⟨r, hrp, ⟨fun x ↦ IsLocalizedModule.map_units f ⟨x, hrp' x.2⟩, ?_, ?_⟩⟩

Premises used: IsLocalizedModule.mk, Subtype.mk, And.intro, Exists.intro, IsLocalizedModule.map_units, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
hrp' : Submonoid.powers r ≤ S
refine_1 : ∀ (y : M'), ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1
refine_2 :
  ∀ {x₁ x₂ : M},
    Eq.{u_1 + 1} (α := M') ((f : (a : M) → M') x₁ : M') ((f : (a : M) → M') x₂ : M') →
      ∃ (c : ↥(Submonoid.powers r)), c • x₁ = c • x₂
⊢ ∃ r ∈ S, IsLocalizedModule.Away r f

Tactic:
refine ⟨r, hrp, ⟨fun x ↦ IsLocalizedModule.map_units f ⟨x, hrp' x.2⟩, ?_, ?_⟩⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
hrp' : Submonoid.powers r ≤ S
y : M'
refine_1 :
  ∀ (x : LocalizedModule (Submonoid.powers r) M)
    (hx :
      Eq (α := LocalizedModule (Submonoid.powers r) M')
        ((((LocalizedModule.map (Submonoid.powers r) :
                    (a : M →ₗ[R] M') →
                      LocalizedModule (Submonoid.powers r) M →ₗ[Localization (Submonoid.powers r)]
                        LocalizedModule (Submonoid.powers r) M')
                  f :
                LinearMap (R := Localization (Submonoid.powers r)) (RingHom.id (Localization (Submonoid.powers r)))
                  (LocalizedModule (Submonoid.powers r) M) (LocalizedModule (Submonoid.powers r) M')) :
              (a : LocalizedModule (Submonoid.powers r) M) → LocalizedModule (Submonoid.powers r) M')
            x :
          LocalizedModule (Submonoid.powers r) M')
        ((LocalizedModule.mkLinearMap (Submonoid.powers r) M' : (a : M') → LocalizedModule (Submonoid.powers r) M') y :
          LocalizedModule (Submonoid.powers r) M')),
    ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1
⊢ ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1

Tactic:
obtain ⟨x, hx⟩ := (H _ dvd_rfl).2 (LocalizedModule.mkLinearMap _ _ y)

Premises used: And.right, LocalizedModule.mkLinearMap, dvd_rfl, DFunLike.coe
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
hrp' : Submonoid.powers r ≤ S
y : M'
x : M
n : ℕ
hx :
  Eq (α := LocalizedModule (Submonoid.powers r) M')
    ((((LocalizedModule.map (Submonoid.powers r) :
                (a : M →ₗ[R] M') →
                  LocalizedModule (Submonoid.powers r) M →ₗ[Localization (Submonoid.powers r)]
                    LocalizedModule (Submonoid.powers r) M')
              f :
            LinearMap (R := Localization (Submonoid.powers r)) (RingHom.id (Localization (Submonoid.powers r)))
              (LocalizedModule (Submonoid.powers r) M) (LocalizedModule (Submonoid.powers r) M')) :
          (a : LocalizedModule (Submonoid.powers r) M) → LocalizedModule (Submonoid.powers r) M')
        (Function.uncurry (mk' (LocalizedModule.mkLinearMap (Submonoid.powers r) M))
          (x,
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x)
              ((fun (x : ℕ) ↦ r ^ x) n) ⋯)) :
      LocalizedModule (Submonoid.powers r) M')
    ((LocalizedModule.mkLinearMap (Submonoid.powers r) M' : (a : M') → LocalizedModule (Submonoid.powers r) M') y :
      LocalizedModule (Submonoid.powers r) M')
⊢ ∃ (m : ℕ), r ^ (m + n) • y = (f : (a : M) → M') (r ^ m • x)

Tactic:
simpa [LocalizedModule.map, IsLocalizedModule.mk_eq_mk', -IsLocalizedModule.mk'_one,
        pow_add, mul_smul, IsLocalizedModule.mk'_eq_mk'_iff, Submonoid.mem_powers_iff,
        Submonoid.smul_def] using hx

Premises used: LocalizedModule.map, IsLocalizedModule.mk'_eq_mk'_iff, pow_add, IsLocalizedModule.mk'_one, Submonoid.smul_def, IsLocalizedModule.mk_eq_mk', Submonoid.mem_powers_iff, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
hrp' : Submonoid.powers r ≤ S
y : M'
x : M
n : ℕ
hx :
  Eq (α := LocalizedModule (Submonoid.powers r) M')
    ((((LocalizedModule.map (Submonoid.powers r) :
                (a : M →ₗ[R] M') →
                  LocalizedModule (Submonoid.powers r) M →ₗ[Localization (Submonoid.powers r)]
                    LocalizedModule (Submonoid.powers r) M')
              f :
            LinearMap (R := Localization (Submonoid.powers r)) (RingHom.id (Localization (Submonoid.powers r)))
              (LocalizedModule (Submonoid.powers r) M) (LocalizedModule (Submonoid.powers r) M')) :
          (a : LocalizedModule (Submonoid.powers r) M) → LocalizedModule (Submonoid.powers r) M')
        (Function.uncurry (mk' (LocalizedModule.mkLinearMap (Submonoid.powers r) M))
          (x,
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x)
              ((fun (x : ℕ) ↦ r ^ x) n) ⋯)) :
      LocalizedModule (Submonoid.powers r) M')
    ((LocalizedModule.mkLinearMap (Submonoid.powers r) M' : (a : M') → LocalizedModule (Submonoid.powers r) M') y :
      LocalizedModule (Submonoid.powers r) M')
refine_1 :
  ∀ (m : ℕ) (hm : r ^ (m + n) • y = (f : (a : M) → M') (r ^ m • x)),
    ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1
⊢ ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1

Tactic:
obtain ⟨m, hm⟩ : ∃ m, r ^ (m + n) • y = f (r ^ m • x) := by
      simpa [LocalizedModule.map, IsLocalizedModule.mk_eq_mk', -IsLocalizedModule.mk'_one,
        pow_add, mul_smul, IsLocalizedModule.mk'_eq_mk'_iff, Submonoid.mem_powers_iff,
        Submonoid.smul_def] using hx
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
hrp' : Submonoid.powers r ≤ S
y : M'
x : M
n : ℕ
hx :
  Eq (α := LocalizedModule (Submonoid.powers r) M')
    ((((LocalizedModule.map (Submonoid.powers r) :
                (a : M →ₗ[R] M') →
                  LocalizedModule (Submonoid.powers r) M →ₗ[Localization (Submonoid.powers r)]
                    LocalizedModule (Submonoid.powers r) M')
              f :
            LinearMap (R := Localization (Submonoid.powers r)) (RingHom.id (Localization (Submonoid.powers r)))
              (LocalizedModule (Submonoid.powers r) M) (LocalizedModule (Submonoid.powers r) M')) :
          (a : LocalizedModule (Submonoid.powers r) M) → LocalizedModule (Submonoid.powers r) M')
        (Function.uncurry (mk' (LocalizedModule.mkLinearMap (Submonoid.powers r) M))
          (x,
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x)
              ((fun (x : ℕ) ↦ r ^ x) n) ⋯)) :
      LocalizedModule (Submonoid.powers r) M')
    ((LocalizedModule.mkLinearMap (Submonoid.powers r) M' : (a : M') → LocalizedModule (Submonoid.powers r) M') y :
      LocalizedModule (Submonoid.powers r) M')
m : ℕ
hm : r ^ (m + n) • y = (f : (a : M) → M') (r ^ m • x)
⊢ ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1

Tactic:
⟨⟨_, ⟨_, _, rfl⟩⟩, hm⟩

Premises used: Prod.mk, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
hrp' : Submonoid.powers r ≤ S
y : M'
x : M
n : ℕ
hx :
  Eq (α := LocalizedModule (Submonoid.powers r) M')
    ((((LocalizedModule.map (Submonoid.powers r) :
                (a : M →ₗ[R] M') →
                  LocalizedModule (Submonoid.powers r) M →ₗ[Localization (Submonoid.powers r)]
                    LocalizedModule (Submonoid.powers r) M')
              f :
            LinearMap (R := Localization (Submonoid.powers r)) (RingHom.id (Localization (Submonoid.powers r)))
              (LocalizedModule (Submonoid.powers r) M) (LocalizedModule (Submonoid.powers r) M')) :
          (a : LocalizedModule (Submonoid.powers r) M) → LocalizedModule (Submonoid.powers r) M')
        (Function.uncurry (mk' (LocalizedModule.mkLinearMap (Submonoid.powers r) M))
          (x,
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x)
              ((fun (x : ℕ) ↦ r ^ x) n) ⋯)) :
      LocalizedModule (Submonoid.powers r) M')
    ((LocalizedModule.mkLinearMap (Submonoid.powers r) M' : (a : M') → LocalizedModule (Submonoid.powers r) M') y :
      LocalizedModule (Submonoid.powers r) M')
m : ℕ
hm : r ^ (m + n) • y = (f : (a : M) → M') (r ^ m • x)
⊢ ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1

Tactic:
exact ⟨⟨_, ⟨_, _, rfl⟩⟩, hm⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
hrp' : Submonoid.powers r ≤ S
x₁ x₂ : M
hx : Eq.{u_1 + 1} (α := M') ((f : (a : M) → M') x₁ : M') ((f : (a : M) → M') x₂ : M')
⊢ Eq (α := LocalizedModule (Submonoid.powers r) M')
    ((((LocalizedModule.map (Submonoid.powers r) :
                (a : M →ₗ[R] M') →
                  LocalizedModule (Submonoid.powers r) M →ₗ[Localization (Submonoid.powers r)]
                    LocalizedModule (Submonoid.powers r) M')
              f :
            LinearMap (R := Localization (Submonoid.powers r)) (RingHom.id (Localization (Submonoid.powers r)))
              (LocalizedModule (Submonoid.powers r) M) (LocalizedModule (Submonoid.powers r) M')) :
          (a : LocalizedModule (Submonoid.powers r) M) → LocalizedModule (Submonoid.powers r) M')
        ((LocalizedModule.mkLinearMap (Submonoid.powers r) M : (a : M) → LocalizedModule (Submonoid.powers r) M) x₁) :
      LocalizedModule (Submonoid.powers r) M')
    ((((LocalizedModule.map (Submonoid.powers r) :
                (a : M →ₗ[R] M') →
                  LocalizedModule (Submonoid.powers r) M →ₗ[Localization (Submonoid.powers r)]
                    LocalizedModule (Submonoid.powers r) M')
              f :
            LinearMap (R := Localization (Submonoid.powers r)) (RingHom.id (Localization (Submonoid.powers r)))
              (LocalizedModule (Submonoid.powers r) M) (LocalizedModule (Submonoid.powers r) M')) :
          (a : LocalizedModule (Submonoid.powers r) M) → LocalizedModule (Submonoid.powers r) M')
        ((LocalizedModule.mkLinearMap (Submonoid.powers r) M : (a : M) → LocalizedModule (Submonoid.powers r) M) x₂) :
      LocalizedModule (Submonoid.powers r) M')

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
hrp' : Submonoid.powers r ≤ S
⊢ ∀ {x₁ x₂ : M},
    Eq.{u_1 + 1} (α := M') ((f : (a : M) → M') x₁ : M') ((f : (a : M) → M') x₂ : M') →
      ∃ (c : ↥(Submonoid.powers r)), c • x₁ = c • x₂

Tactic:
exact fun {x₁ x₂} hx ↦ IsLocalizedModule.exists_of_eq (f := LocalizedModule.mkLinearMap
      (.powers r) _) ((H _ dvd_rfl).1 (by simp [hx]))

Premises used: IsLocalizedModule.exists_of_eq, And.left, dvd_rfl
-- 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
inst_5 : FinitePresentation R M
f : M →ₗ[R] N
⊢ Eq (α := LocalizedModule S M →ₗ[R] LocalizedModule S N)
    ((linearEquivMap S : (a : LocalizedModule S (M →ₗ[R] N)) → LocalizedModule S M →ₗ[R] LocalizedModule S N)
        ((LocalizedModule.mkLinearMap S (M →ₗ[R] N) : (a : M →ₗ[R] N) → LocalizedModule S (M →ₗ[R] N)) f) :
      LocalizedModule S M →ₗ[R] LocalizedModule S N)
    ((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N) :
          (a : M →ₗ[R] N) → LocalizedModule S M →ₗ[R] LocalizedModule S N)
        f :
      LocalizedModule S M →ₗ[R] LocalizedModule S N)

Tactic:
IsLocalizedModule.linearEquiv_apply S _ _ f

Premises used: IsLocalizedModule.linearEquiv_apply