awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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'))
⊢ IsLocalizedModule S (IsLocalizedModule.map S f g)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
⊢ IsLocalizedModule S (IsLocalizedModule.map S f g)
have 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₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
⊢ 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'))
have 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')
Tactic: rw [Module.End.isUnit_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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 (α := 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')
have 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')
Tactic: have := (Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units (S := S) (f := g) s)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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.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')
have 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')
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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')
⊢ 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')
have 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')
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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')
h : M' →ₗ[R] N'
⊢ ∃ (a : 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')
        a =
      h
have h₁ : (((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')
    ((↑sorry.unit⁻¹ : End R N') ∘ₗ h) =
  h
Tactic: use ((IsLocalizedModule.map_units (S := S) (f := g) s).unit⁻¹).1 ∘ₗ h
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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')
h : 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')
      ((↑⋯.unit⁻¹ : End R N') ∘ₗ h) =
    h
have h₁ : ∀ (x : M'),
  Eq.{u_2 + 1} (α := 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')
              ((↑sorry.unit⁻¹ : End R N') ∘ₗ h) :
            M' →ₗ[R] N') :
          (a : M') → N')
        x :
      N')
    ((h : (a : M') → N') x : N')
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
h : M' →ₗ[R] N'
⊢ ∃ (x : (M →ₗ[R] N) × ↥S), x.2 • h = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') x.1
have surj : ∀ (h' : M →ₗ[R] N) (s : ↥S) (e : g ∘ₗ h' = s • h ∘ₗ f),
  ∃ (x : (M →ₗ[R] N) × ↥S), x.2 • h = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') x.1
Tactic: obtain ⟨h', s, e⟩ := Module.FinitePresentation.exists_lift_of_isLocalizedModule S g (h ∘ₗ f)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
⊢ ∃ (x : (M →ₗ[R] N) × ↥S), x.2 • h = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') x.1
have surj : (h', s).2 • h = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') (h', s).1
Tactic: refine ⟨⟨h', s⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
⊢ (h', s).2 • h = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') (h', s).1
have surj : ((h', s).2 • h) ∘ₗ f = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') (h', s).1 ∘ₗ f
Tactic: apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
⊢ g ∘ₗ h' = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') (h', s).1 ∘ₗ f
have h₁ : ∀ (x : M),
  Eq.{u_2 + 1} (α := N') ((g ∘ₗ h' : (a : M) → N') x : N')
    (((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') (h', s).1 ∘ₗ f : (a : M) → N') x : N')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
h₁ h₂ : M →ₗ[R] N
e :
  Eq (α := M' →ₗ[R] N') ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h₁ : M' →ₗ[R] N')
    ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h₂ : M' →ₗ[R] N')
⊢ ∃ (c : ↥S), c • h₁ = c • h₂
have exists_of_eq : g ∘ₗ h₁ = g ∘ₗ h₂
Tactic: apply Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule S g
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
h₁ h₂ : M →ₗ[R] N
e :
  Eq (α := M' →ₗ[R] N') ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h₁ : M' →ₗ[R] N')
    ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h₂ : M' →ₗ[R] N')
⊢ g ∘ₗ h₁ = g ∘ₗ h₂
have exists_of_eq : ∀ (x : M), Eq.{u_2 + 1} (α := N') ((g ∘ₗ h₁ : (a : M) → N') x : N') ((g ∘ₗ h₂ : (a : M) → N') x : N')
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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'
⊢ ∃ r ∈ S, IsLocalizedModule.Away r f
have this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
Tactic: have : IsLocalizedModule S (.id (R := R) (M := M')) :=
    ⟨IsLocalizedModule.map_units f, fun y ↦ ⟨⟨y, 1⟩, by simp⟩, by simpa using ⟨1, S.one_mem⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := M') (β := M')
    (⇑((map S f LinearMap.id : (a : M →ₗ[R] M') → M' →ₗ[R] M') f : M' →ₗ[R] M') : (a : M') → M')
have h : Eq.{u_1 + 1} (α := M' →ₗ[R] M') ((map S f LinearMap.id : (a : M →ₗ[R] M') → M' →ₗ[R] M') f : M' →ₗ[R] M')
  (LinearMap.id : M' →ₗ[R] M')
Tactic: convert! show Function.Bijective LinearMap.id from Function.bijective_id
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
⊢ Eq.{u_1 + 1} (α := M' →ₗ[R] M') ((map S f LinearMap.id : (a : M →ₗ[R] M') → M' →ₗ[R] M') f : M' →ₗ[R] M')
    (LinearMap.id : M' →ₗ[R] M')
have h : ∀ (x : ↥S),
  IsUnit.{u_1} (M := Module.End R M')
    ((algebraMap R (Module.End R M') : (a : R) → Module.End R M') (↑x : R) : Module.End R M')
Tactic: apply IsLocalizedModule.ext S f
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
h :
  ∀ (x : ↥S),
    IsUnit.{u_1} (M := Module.End R M')
      ((algebraMap R (Module.End R M') : (a : R) → Module.End R M') (↑x : R) : Module.End R M')
⊢ Eq.{u_1 + 1} (α := M' →ₗ[R] M') ((map S f LinearMap.id : (a : M →ₗ[R] M') → M' →ₗ[R] M') f : M' →ₗ[R] M')
    (LinearMap.id : M' →ₗ[R] M')
have h₁ : (map S f LinearMap.id : (a : M →ₗ[R] M') → M' →ₗ[R] M') f ∘ₗ f = LinearMap.id ∘ₗ f
Tactic: apply IsLocalizedModule.ext S f
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 ∈ S, IsLocalizedModule.Away r f
have obtain : ∀ (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')),
  ∃ r ∈ S, IsLocalizedModule.Away r f
Tactic: obtain ⟨r, hrp, H⟩ := exists_bijective_map_powers S
      f (.id (R := R) (M := M')) f <| by
    convert! show Function.Bijective LinearMap.id from Function.bijective_id
    apply IsLocalizedModule.ext S f
    · exact IsLocalizedModule.map_units f
    · simp [IsLocalizedModule.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
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')
⊢ ∃ r ∈ S, IsLocalizedModule.Away r f
have hrp' : Submonoid.powers r ≤ S
Tactic: have hrp' : .powers r ≤ S := by simpa [Submonoid.powers_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
have refine_1 : ∀ (y : M'), ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1
Tactic: refine ⟨r, hrp, ⟨fun x ↦ IsLocalizedModule.map_units f ⟨x, hrp' x.2⟩, ?_, ?_⟩⟩