awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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)
⊢ ∀ (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
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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)
⊢ ∀ (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) := ‹_›
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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
r : (↑s : Type u_1)
⊢ ∀ (x : R),
    Eq.{u_4 + 1} (α := Sᵣ r) ((algebraMap R (Sᵣ r) : (a : R) → Sᵣ r) x : Sᵣ r)
      ((algebraMap (Rᵣ r) (Sᵣ r) : (a : Rᵣ r) → Sᵣ r) ((algebraMap R (Rᵣ r) : (a : R) → Rᵣ r) x) : Sᵣ r)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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
⊢ ∀ (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]
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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)
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)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)

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)

Premises used: AlgHom.toLinearMap, IsScalarTower.toAlgHom, Algebra.linearMap, surjective_of_isLocalized_span
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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)
⊢ ∀ (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:
simpa [IsLocalization.map_linearMap_eq_toLinearMap_mapₐ] using h

Premises used: IsLocalization.map_linearMap_eq_toLinearMap_mapₐ
-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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.Bijective.{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)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
⟨injective_of_isLocalization_of_span_eq_top hs _ _ _ (fun r ↦ (h r).1),
    surjective_of_isLocalization_of_span_eq_top hs _ _ _ (fun r ↦ (h r).2)⟩

Premises used: injective_of_isLocalization_of_span_eq_top, And.right, And.left, And.intro, surjective_of_isLocalization_of_span_eq_top, Function.Bijective
-- Module: Mathlib.RingTheory.LocalProperties.FinitePresentation
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)
⊢ Module.Finite R M

Tactic:
have : Module.Finite R M :=
    Module.Finite.of_localizationSpan' (Rₚ := Rₚ) s hs ϕ (fun _ ↦ inferInstance)
-- Module: Mathlib.RingTheory.LocalProperties.FinitePresentation
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
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
⊢ FinitePresentation R M

Tactic:
obtain ⟨n, f, fsurj⟩ := Module.Finite.exists_fin' R M

Premises used: Module.Finite.exists_fin'
-- Module: Mathlib.RingTheory.LocalProperties.FinitePresentation
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)
rw : f.ker.FG
⊢ FinitePresentation R M

Tactic:
rw [← Module.FinitePresentation.fg_ker_iff f fsurj]

Premises used: Module.FinitePresentation.fg_ker_iff
-- Module: Mathlib.RingTheory.LocalProperties.FinitePresentation
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

Tactic:
f.ker.of_localizationSpan' s hs (Rₚ := Rₚ)
    (fun g ↦ TensorProduct.mk R (Rₚ g) (Fin n → R) 1) (fun g ↦ ?_)

Premises used: Submodule.of_localizationSpan', OfNat.ofNat, DFunLike.coe, TensorProduct.mk
-- Module: Mathlib.RingTheory.LocalProperties.FinitePresentation
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)
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)
⊢ f.ker.FG

Tactic:
refine f.ker.of_localizationSpan' s hs (Rₚ := Rₚ)
    (fun g ↦ TensorProduct.mk R (Rₚ g) (Fin n → R) 1) (fun g ↦ ?_)

Premises used: Submodule.of_localizationSpan', OfNat.ofNat, DFunLike.coe, TensorProduct.mk
-- Module: Mathlib.RingTheory.LocalProperties.FinitePresentation
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)
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)))
⊢ 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:
rw [LinearMap.localized'_ker_eq_ker_localizedMap (Rₚ g) (Submonoid.powers g.1) _ (ϕ g) f]

Premises used: LinearMap.localized'_ker_eq_ker_localizedMap, Submonoid.powers, Subtype.val
-- Module: Mathlib.RingTheory.LocalProperties.FinitePresentation
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)
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)
⊢ 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:
apply Module.FinitePresentation.fg_ker

Premises used: Module.FinitePresentation.fg_ker