awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have this₁ : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
Tactic: have (r : s) : IsScalarTower R S (Sᵣ r) := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this_1 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
this : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have this₁ : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S) (Sᵣ r)
Tactic: have : ∀ r, IsLocalization.Away (algebraMap R S r.val) (Sᵣ r) := ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this_1 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
this_2 : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
this_3 :
  ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S) (Sᵣ r)
this : (r : (↑s : Type u_1)) → Algebra.{u_3, u_4} (Rᵣ r) (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ localizationAlgebra (Submonoid.powers (↑r : R)) S
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have this₁ : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_3, u_4} R (Rᵣ r) (Sᵣ r)
Tactic: have (r : s) : IsScalarTower R (Rᵣ r) (Sᵣ r) :=
    .of_algebraMap_eq <| by simp [RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this_1 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
this_2 : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
this_3 :
  ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S) (Sᵣ r)
this_4 : (r : (↑s : Type u_1)) → Algebra.{u_3, u_4} (Rᵣ r) (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ localizationAlgebra (Submonoid.powers (↑r : R)) S
this : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_3, u_4} R (Rᵣ r) (Sᵣ r)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have apply : ∀ (r : (↑s : Type u_1)),
  Function.Injective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
    (⇑((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (Algebra.linearMap R (Rᵣ r))
                (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S (Sᵣ r))) :
              (a : R →ₗ[R] S) → Rᵣ r →ₗ[R] Sᵣ r)
            (Algebra.linearMap R S) :
          LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (Rᵣ r) (Sᵣ r)) :
      (a : Rᵣ r) → Sᵣ r)
Tactic: apply injective_of_isLocalized_span s hs Rᵣ (fun r : s ↦ Algebra.linearMap _ _) _
    (fun r : s ↦ ((IsScalarTower.toAlgHom R S (Sᵣ r)).toLinearMap)) (Algebra.linearMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have this₁ : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
Tactic: have (r : s) : IsScalarTower R S (Sᵣ r) := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this_1 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
this : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have this₁ : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S) (Sᵣ r)
Tactic: have : ∀ r, IsLocalization.Away (algebraMap R S r.val) (Sᵣ r) := ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this_1 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
this_2 : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
this_3 :
  ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S) (Sᵣ r)
this : (r : (↑s : Type u_1)) → Algebra.{u_3, u_4} (Rᵣ r) (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ localizationAlgebra (Submonoid.powers (↑r : R)) S
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have this₁ : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_3, u_4} R (Rᵣ r) (Sᵣ r)
Tactic: have (r : s) : IsScalarTower R (Rᵣ r) (Sᵣ r) :=
    .of_algebraMap_eq <| by simp [RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Rᵣ : (↑s : Type u_1) → Type u_3
inst_2 : (r : (↑s : Type u_1)) → CommSemiring (Rᵣ r)
inst_3 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_3} R (Rᵣ r)
Sᵣ : (↑s : Type u_1) → Type u_4
inst_4 : (r : (↑s : Type u_1)) → CommSemiring (Sᵣ r)
inst_5 : (r : (↑s : Type u_1)) → Algebra.{u_2, u_4} S (Sᵣ r)
f : R →+* S
inst_6 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_3} (↑r : R) (Rᵣ r)
inst_7 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((f : (a : R) → S) (↑r : R) : S) (Sᵣ r)
h :
  ∀ (r : (↑s : Type u_1)),
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
      (⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f (↑r : R)) : (a : Rᵣ r) → Sᵣ r)
algInst : Algebra R S := f.toAlgebra
this_1 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ RingHom.toAlgebra (RingHom.comp (algebraMap S (Sᵣ r)) f)
this_2 : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_2, u_4} R S (Sᵣ r)
this_3 :
  ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_2, u_4} (R := S) ((algebraMap R S : (a : R) → S) (↑r : R) : S) (Sᵣ r)
this_4 : (r : (↑s : Type u_1)) → Algebra.{u_3, u_4} (Rᵣ r) (Sᵣ r) :=
  fun (r : (↑s : Type u_1)) ↦ localizationAlgebra (Submonoid.powers (↑r : R)) S
this : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_3, u_4} R (Rᵣ r) (Sᵣ r)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have apply : ∀ (r : (↑s : Type u_1)),
  Function.Surjective.{u_3 + 1, u_4 + 1} (α := Rᵣ r) (β := Sᵣ r)
    (⇑((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (Algebra.linearMap R (Rᵣ r))
                (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S (Sᵣ r))) :
              (a : R →ₗ[R] S) → Rᵣ r →ₗ[R] Sᵣ r)
            (Algebra.linearMap R S) :
          LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (Rᵣ r) (Sᵣ r)) :
      (a : Rᵣ r) → Sᵣ r)
Tactic: apply surjective_of_isLocalized_span s hs Rᵣ (fun r : s ↦ Algebra.linearMap _ _) _
    (fun r : s ↦ ((IsScalarTower.toAlgHom R S (Sᵣ r)).toLinearMap)) (Algebra.linearMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.FinitePresentation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_3
inst_3 : (g : (↑s : Type u_1)) → AddCommGroup (Mₚ g)
inst_4 : (g : (↑s : Type u_1)) → Module.{u_1, u_3} R (Mₚ g)
Rₚ : (↑s : Type u_1) → Type u_4
inst_5 : (g : (↑s : Type u_1)) → CommRing (Rₚ g)
inst_6 : (g : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Rₚ g)
inst_7 : ∀ (g : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_4} (↑g : R) (Rₚ g)
inst_8 : (g : (↑s : Type u_1)) → Module.{u_4, u_3} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : (↑s : Type u_1)), IsScalarTower.{u_1, u_4, u_3} R (Rₚ g) (Mₚ g)
ϕ : (g : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : (↑s : Type u_1)), IsLocalizedModule (Submonoid.powers (↑g : R)) (ϕ g)
h : ∀ (g : (↑s : Type u_1)), FinitePresentation.{u_4, u_3} (Rₚ g) (Mₚ g)
⊢ FinitePresentation R M
have this : Module.Finite R M
Tactic: have : Module.Finite R M :=
    Module.Finite.of_localizationSpan' (Rₚ := Rₚ) s hs ϕ (fun _ ↦ inferInstance)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.FinitePresentation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_3
inst_3 : (g : (↑s : Type u_1)) → AddCommGroup (Mₚ g)
inst_4 : (g : (↑s : Type u_1)) → Module.{u_1, u_3} R (Mₚ g)
Rₚ : (↑s : Type u_1) → Type u_4
inst_5 : (g : (↑s : Type u_1)) → CommRing (Rₚ g)
inst_6 : (g : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Rₚ g)
inst_7 : ∀ (g : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_4} (↑g : R) (Rₚ g)
inst_8 : (g : (↑s : Type u_1)) → Module.{u_4, u_3} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : (↑s : Type u_1)), IsScalarTower.{u_1, u_4, u_3} R (Rₚ g) (Mₚ g)
ϕ : (g : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : (↑s : Type u_1)), IsLocalizedModule (Submonoid.powers (↑g : R)) (ϕ g)
h : ∀ (g : (↑s : Type u_1)), FinitePresentation.{u_4, u_3} (Rₚ g) (Mₚ g)
this : Module.Finite R M
⊢ FinitePresentation R M
have obtain : ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
  (fsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)),
  FinitePresentation R M
Tactic: obtain ⟨n, f, fsurj⟩ := Module.Finite.exists_fin' R M
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.FinitePresentation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_3
inst_3 : (g : (↑s : Type u_1)) → AddCommGroup (Mₚ g)
inst_4 : (g : (↑s : Type u_1)) → Module.{u_1, u_3} R (Mₚ g)
Rₚ : (↑s : Type u_1) → Type u_4
inst_5 : (g : (↑s : Type u_1)) → CommRing (Rₚ g)
inst_6 : (g : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Rₚ g)
inst_7 : ∀ (g : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_4} (↑g : R) (Rₚ g)
inst_8 : (g : (↑s : Type u_1)) → Module.{u_4, u_3} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : (↑s : Type u_1)), IsScalarTower.{u_1, u_4, u_3} R (Rₚ g) (Mₚ g)
ϕ : (g : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : (↑s : Type u_1)), IsLocalizedModule (Submonoid.powers (↑g : R)) (ϕ g)
h : ∀ (g : (↑s : Type u_1)), FinitePresentation.{u_4, u_3} (Rₚ g) (Mₚ g)
this : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
fsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
⊢ FinitePresentation R M
have rw : f.ker.FG
Tactic: rw [← Module.FinitePresentation.fg_ker_iff f fsurj]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.FinitePresentation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_3
inst_3 : (g : (↑s : Type u_1)) → AddCommGroup (Mₚ g)
inst_4 : (g : (↑s : Type u_1)) → Module.{u_1, u_3} R (Mₚ g)
Rₚ : (↑s : Type u_1) → Type u_4
inst_5 : (g : (↑s : Type u_1)) → CommRing (Rₚ g)
inst_6 : (g : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Rₚ g)
inst_7 : ∀ (g : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_4} (↑g : R) (Rₚ g)
inst_8 : (g : (↑s : Type u_1)) → Module.{u_4, u_3} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : (↑s : Type u_1)), IsScalarTower.{u_1, u_4, u_3} R (Rₚ g) (Mₚ g)
ϕ : (g : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : (↑s : Type u_1)), IsLocalizedModule (Submonoid.powers (↑g : R)) (ϕ g)
h : ∀ (g : (↑s : Type u_1)), FinitePresentation.{u_4, u_3} (Rₚ g) (Mₚ g)
this : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
fsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
⊢ f.ker.FG
have refine : ∀ (g : (↑s : Type u_1)),
  Submodule.FG (R := Rₚ g) (M := TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R))
    (Submodule.localized' (Rₚ g) (Submonoid.powers (↑g : R))
      ((fun (g : (↑s : Type u_1)) ↦
          ((TensorProduct.mk R (Rₚ g) (Fin n → R) : (a : Rₚ g) → (Fin n → R) →ₗ[R] TensorProduct R (Rₚ g) (Fin n → R))
              1 :
            (Fin n → R) →ₗ[R] TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R)))
        g)
      f.ker)
Tactic: refine f.ker.of_localizationSpan' s hs (Rₚ := Rₚ)
    (fun g ↦ TensorProduct.mk R (Rₚ g) (Fin n → R) 1) (fun g ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.FinitePresentation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_3
inst_3 : (g : (↑s : Type u_1)) → AddCommGroup (Mₚ g)
inst_4 : (g : (↑s : Type u_1)) → Module.{u_1, u_3} R (Mₚ g)
Rₚ : (↑s : Type u_1) → Type u_4
inst_5 : (g : (↑s : Type u_1)) → CommRing (Rₚ g)
inst_6 : (g : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Rₚ g)
inst_7 : ∀ (g : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_4} (↑g : R) (Rₚ g)
inst_8 : (g : (↑s : Type u_1)) → Module.{u_4, u_3} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : (↑s : Type u_1)), IsScalarTower.{u_1, u_4, u_3} R (Rₚ g) (Mₚ g)
ϕ : (g : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : (↑s : Type u_1)), IsLocalizedModule (Submonoid.powers (↑g : R)) (ϕ g)
h : ∀ (g : (↑s : Type u_1)), FinitePresentation.{u_4, u_3} (Rₚ g) (Mₚ g)
this : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
fsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
g : (↑s : Type u_1)
⊢ Submodule.FG (R := Rₚ g) (M := TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R))
    (Submodule.localized' (Rₚ g) (Submonoid.powers (↑g : R))
      ((fun (g : (↑s : Type u_1)) ↦
          ((TensorProduct.mk R (Rₚ g) (Fin n → R) : (a : Rₚ g) → (Fin n → R) →ₗ[R] TensorProduct R (Rₚ g) (Fin n → R))
              1 :
            (Fin n → R) →ₗ[R] TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R)))
        g)
      f.ker)
have rw : Submodule.FG (R := Rₚ g) (M := TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R))
  (LinearMap.ker (M₂ := Mₚ g)
    (LinearMap.extendScalarsOfIsLocalization (Submonoid.powers (↑g : R)) (Rₚ g)
      ((IsLocalizedModule.map (Submonoid.powers (↑g : R))
            ((fun (g : (↑s : Type u_1)) ↦
                ((TensorProduct.mk R (Rₚ g) (Fin n → R) :
                      (a : Rₚ g) → (Fin n → R) →ₗ[R] TensorProduct R (Rₚ g) (Fin n → R))
                    1 :
                  (Fin n → R) →ₗ[R] TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R)))
              g)
            (ϕ g) :
          (a : (Fin n → R) →ₗ[R] M) → TensorProduct R (Rₚ g) (Fin n → R) →ₗ[R] Mₚ g)
        f)))
Tactic: rw [LinearMap.localized'_ker_eq_ker_localizedMap (Rₚ g) (Submonoid.powers g.1) _ (ϕ g) f]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.FinitePresentation (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_3
inst_3 : (g : (↑s : Type u_1)) → AddCommGroup (Mₚ g)
inst_4 : (g : (↑s : Type u_1)) → Module.{u_1, u_3} R (Mₚ g)
Rₚ : (↑s : Type u_1) → Type u_4
inst_5 : (g : (↑s : Type u_1)) → CommRing (Rₚ g)
inst_6 : (g : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Rₚ g)
inst_7 : ∀ (g : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_4} (↑g : R) (Rₚ g)
inst_8 : (g : (↑s : Type u_1)) → Module.{u_4, u_3} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : (↑s : Type u_1)), IsScalarTower.{u_1, u_4, u_3} R (Rₚ g) (Mₚ g)
ϕ : (g : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : (↑s : Type u_1)), IsLocalizedModule (Submonoid.powers (↑g : R)) (ϕ g)
h : ∀ (g : (↑s : Type u_1)), FinitePresentation.{u_4, u_3} (Rₚ g) (Mₚ g)
this : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
fsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
g : (↑s : Type u_1)
⊢ Submodule.FG (R := Rₚ g) (M := TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R))
    (LinearMap.ker (M₂ := Mₚ g)
      (LinearMap.extendScalarsOfIsLocalization (Submonoid.powers (↑g : R)) (Rₚ g)
        ((IsLocalizedModule.map (Submonoid.powers (↑g : R))
              ((fun (g : (↑s : Type u_1)) ↦
                  ((TensorProduct.mk R (Rₚ g) (Fin n → R) :
                        (a : Rₚ g) → (Fin n → R) →ₗ[R] TensorProduct R (Rₚ g) (Fin n → R))
                      1 :
                    (Fin n → R) →ₗ[R] TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R)))
                g)
              (ϕ g) :
            (a : (Fin n → R) →ₗ[R] M) → TensorProduct R (Rₚ g) (Fin n → R) →ₗ[R] Mₚ g)
          f)))
have hl : Function.Surjective (α := TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R)) (β := Mₚ g)
  (⇑(LinearMap.extendScalarsOfIsLocalization (Submonoid.powers (↑g : R)) (Rₚ g)
          ((IsLocalizedModule.map (Submonoid.powers (↑g : R))
                ((fun (g : (↑s : Type u_1)) ↦
                    ((TensorProduct.mk R (Rₚ g) (Fin n → R) :
                          (a : Rₚ g) → (Fin n → R) →ₗ[R] TensorProduct R (Rₚ g) (Fin n → R))
                        1 :
                      (Fin n → R) →ₗ[R] TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R)))
                  g)
                (ϕ g) :
              (a : (Fin n → R) →ₗ[R] M) → TensorProduct R (Rₚ g) (Fin n → R) →ₗ[R] Mₚ g)
            f) :
        LinearMap (R := Rₚ g) (RingHom.id (Rₚ g)) (TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R)) (Mₚ g)) :
    (a : TensorProduct R (Rₚ g) (Fin n → R)) → Mₚ g)
Tactic: apply Module.FinitePresentation.fg_ker