awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
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'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
hM : Module.Finite R M
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
have have₁ have₂ :
  ∀
    (this :
      ∀ (x : M),
        ∃ (s : ↥S),
          HSMul.hSMul (β := N) s ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) s ((g₂ : (a : M) → N) x : N)),
    ∃ (s : ↥S), s • g₁ = s • g₂
have₃ :
  ∀ (s : (x : M) → ↥S)
    (hs :
      ∀ (x : M),
        HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N)),
    ∃ (s : ↥S), s • g₁ = s • g₂
have₄ :
  ∀ (s : (x : M) → ↥S)
    (hs :
      ∀ (x : M),
        HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N))
    (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤), ∃ (s : ↥S), s • g₁ = s • g₂
h₁ :
  ∀ (s : (x : M) → ↥S)
    (hs :
      ∀ (x : M),
        HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N))
    (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤), σ.prod s • g₁ = σ.prod s • g₂
h₂ :
  ∀ (s : (x : M) → ↥S)
    (hs :
      ∀ (x : M),
        HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N))
    (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤),
    (↑σ : Set M) ⊆ (↑(σ.prod s • g₁ - σ.prod s • g₂).ker : Set M)
⊢ ∃ (s : ↥S), s • g₁ = s • g₂
have h₃ : ∀ (s : (x : M) → ↥S)
  (hs :
    ∀ (x : M),
      HSMul.hSMul (β := N) (s x) ((g₁ : (a : M) → N) x : N) = HSMul.hSMul (β := N) (s x) ((g₂ : (a : M) → N) x : N))
  (σ : Finset M) (hσ : Eq (α := Submodule R M) (Submodule.span R (↑σ : Set M)) ⊤) ⦃x : M⦄ (hx : x ∈ (↑σ : Set M)),
  x ∈ (↑(σ.prod s • g₁ - σ.prod s • g₂).ker : Set M)
Tactic: classical
  have : ∀ x, ∃ s : S, s • g₁ x = s • g₂ x := fun x ↦
    IsLocalizedModule.exists_of_eq (S := S) (f := f) (LinearMap.congr_fun h x)
  choose s hs using this
  obtain ⟨σ, hσ⟩ := hM
  use σ.prod s
  rw [← sub_eq_zero, ← LinearMap.ker_eq_top, ← top_le_iff, ← hσ, Submodule.span_le]
  intro x hx
  simp only [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.sub_apply, LinearMap.smul_apply,
    sub_eq_zero, ← Finset.prod_erase_mul σ s hx, mul_smul, hs]
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
⊢ ∃ r ∈ S,
    ∀ (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)
have obtain : ∀ (l' : N →ₗ[R] M) (s₀ : ↥S) (H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g),
  ∃ r ∈ S,
    ∀ (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)
Tactic: obtain ⟨l', s₀, H⟩ := Module.FinitePresentation.exists_lift_of_isLocalizedModule S f
    (e.symm.toLinearMap.comp g)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g
⊢ g ∘ₗ l ∘ₗ l' = g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
have h : ∀ (a : N),
  Eq.{u_2 + 1} (α := N') ((g ∘ₗ l ∘ₗ l' : (a : N) → N') a : N')
    ((g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id : (a : N) → N') a : N')
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g
⊢ ∃ r ∈ S,
    ∀ (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)
have H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
Tactic: have H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id) := by
    ext a; simpa [-EmbeddingLike.apply_eq_iff_eq, e] using congr(e ($H a))
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
⊢ ∃ r ∈ S,
    ∀ (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)
have obtain : ∀ (s₁ : ↥S) (hs₁ : s₁ • l ∘ₗ l' = s₁ • HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id),
  ∃ r ∈ S,
    ∀ (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)
Tactic: obtain ⟨s₁, hs₁⟩ := Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule S g _ _ H₁
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
⊢ f ∘ₗ l' ∘ₗ l = f ∘ₗ HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
have rw : s₀ • ((↑e.symm : N' →ₗ[R] M') ∘ₗ (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) ∘ₗ f =
  f ∘ₗ HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
Tactic: rw [← LinearMap.comp_assoc, H, LinearMap.smul_comp, LinearMap.comp_assoc,
      ← IsLocalizedModule.map_comp S f g l, ← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
⊢ s₀ • ((↑e.symm : N' →ₗ[R] M') ∘ₗ (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) ∘ₗ f =
    f ∘ₗ HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
have change : s₀ • ((↑e.symm : N' →ₗ[R] M') ∘ₗ (↑e : M' →ₗ[R] N')) ∘ₗ f = f ∘ₗ HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
Tactic: change s₀ • (e.symm.toLinearMap ∘ₗ e.toLinearMap) ∘ₗ _ = _
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
⊢ ∃ r ∈ S,
    ∀ (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)
have H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
Tactic: have H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ (s₀ • LinearMap.id) := by
    rw [← LinearMap.comp_assoc, H, LinearMap.smul_comp, LinearMap.comp_assoc,
      ← IsLocalizedModule.map_comp S f g l, ← LinearMap.comp_assoc]
    change s₀ • (e.symm.toLinearMap ∘ₗ e.toLinearMap) ∘ₗ _ = _
    simp [LinearMap.comp_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
⊢ ∃ r ∈ S,
    ∀ (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)
have obtain : ∀ (s₂ : ↥S) (hs₂ : s₂ • l' ∘ₗ l = s₂ • HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id),
  ∃ r ∈ S,
    ∀ (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)
Tactic: obtain ⟨s₂, hs₂⟩ := Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule S f _ _ H₂
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
⊢ ∃ r ∈ S,
    ∀ (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)
have refine : ∀ (t : R) (ht : (↑s₀ : R) * (↑s₁ : R) * (↑s₂ : 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)
Tactic: refine ⟨s₀ * s₁ * s₂, (s₀ * s₁ * s₂).2, fun t ht ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
t : R
ht : (↑s₀ : R) * (↑s₁ : R) * (↑s₂ : R) ∣ t
Rₛ : Type u_3 := Localization (Submonoid.powers t)
lₛ : LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
  (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
hu :
  IsUnit (M := Rₛ)
    ((algebraMap R Rₛ : (a : R) → Rₛ)
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x) t ⋯) : R) :
      Rₛ)
⊢ 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)
have hu₀ : IsUnit (M := Rₛ) ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₀ : R) : Rₛ)
Tactic: have hu₀ : IsUnit (algebraMap R Rₛ s₀) := isUnit_of_dvd_unit
      (map_dvd (algebraMap R Rₛ) (dvd_trans ⟨s₁ * s₂, by simp [mul_assoc]⟩ ht)) hu