awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : FinitePresentation T (T ⊗[R] S)
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
this : Module.FaithfullyFlat (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)
fT : T ⊗[R] MvPolynomial (Fin n) R →ₐ[T] T ⊗[R] S := TensorProduct.map (AlgHom.id T T) f
refine :
  Ideal.FG (R := T ⊗[R] MvPolynomial (Fin n) R)
    (Ideal.map (F := MvPolynomial (Fin n) R →+* T ⊗[R] MvPolynomial (Fin n) R)
      (algebraMap (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker f.toRingHom))
⊢ FinitePresentation R S

Tactic:
refine .of_surjective hf (.of_FG_map_of_faithfullyFlat (S := T ⊗[R] MvPolynomial (Fin n) R) ?_)
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : FinitePresentation T (T ⊗[R] S)
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
this : Module.FaithfullyFlat (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)
fT : T ⊗[R] MvPolynomial (Fin n) R →ₐ[T] T ⊗[R] S := TensorProduct.map (AlgHom.id T T) f
⊢ Eq (α := Ideal (T ⊗[R] MvPolynomial (Fin n) R))
    (Ideal.map (F := MvPolynomial (Fin n) R →+* T ⊗[R] MvPolynomial (Fin n) R)
      (algebraMap (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker f.toRingHom))
    (RingHom.ker fT)

Tactic:
have : (RingHom.ker f.toRingHom).map
      (algebraMap (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)) = RingHom.ker fT :=
    (Algebra.TensorProduct.lTensor_ker f hf).symm
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : FinitePresentation T (T ⊗[R] S)
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
this_1 : Module.FaithfullyFlat (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)
fT : T ⊗[R] MvPolynomial (Fin n) R →ₐ[T] T ⊗[R] S := TensorProduct.map (AlgHom.id T T) f
this :
  Eq (α := Ideal (T ⊗[R] MvPolynomial (Fin n) R))
    (Ideal.map (F := MvPolynomial (Fin n) R →+* T ⊗[R] MvPolynomial (Fin n) R)
      (algebraMap (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker f.toRingHom))
    (RingHom.ker fT)
rw : Ideal.FG (RingHom.ker fT)
⊢ Ideal.FG (R := T ⊗[R] MvPolynomial (Fin n) R)
    (Ideal.map (F := MvPolynomial (Fin n) R →+* T ⊗[R] MvPolynomial (Fin n) R)
      (algebraMap (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker f.toRingHom))

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : FinitePresentation T (T ⊗[R] S)
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
this_1 : Module.FaithfullyFlat (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)
fT : T ⊗[R] MvPolynomial (Fin n) R →ₐ[T] T ⊗[R] S := TensorProduct.map (AlgHom.id T T) f
this :
  Eq (α := Ideal (T ⊗[R] MvPolynomial (Fin n) R))
    (Ideal.map (F := MvPolynomial (Fin n) R →+* T ⊗[R] MvPolynomial (Fin n) R)
      (algebraMap (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker f.toRingHom))
    (RingHom.ker fT)
hf₁ :
  Function.Surjective (α := T ⊗[R] MvPolynomial (Fin n) R) (β := T ⊗[R] S)
    (⇑fT : (a : T ⊗[R] MvPolynomial (Fin n) R) → T ⊗[R] S)
⊢ Ideal.FG (RingHom.ker fT)

Tactic:
apply ker_fG_of_surjective

Premises used: Algebra.FinitePresentation.ker_fG_of_surjective
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : FinitePresentation T (T ⊗[R] S)
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
this_1 : Module.FaithfullyFlat (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)
fT : T ⊗[R] MvPolynomial (Fin n) R →ₐ[T] T ⊗[R] S := TensorProduct.map (AlgHom.id T T) f
this :
  Eq (α := Ideal (T ⊗[R] MvPolynomial (Fin n) R))
    (Ideal.map (F := MvPolynomial (Fin n) R →+* T ⊗[R] MvPolynomial (Fin n) R)
      (algebraMap (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker f.toRingHom))
    (RingHom.ker fT)
⊢ Function.Surjective (α := T ⊗[R] MvPolynomial (Fin n) R) (β := T ⊗[R] S)
    (⇑fT : (a : T ⊗[R] MvPolynomial (Fin n) R) → T ⊗[R] S)

Tactic:
FiniteType.baseChangeAux_surj T hf

Premises used: Algebra.FiniteType.baseChangeAux_surj
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.FaithfullyFlat R T
inst_6 : FinitePresentation T (T ⊗[R] S)
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
this_1 : Module.FaithfullyFlat (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)
fT : T ⊗[R] MvPolynomial (Fin n) R →ₐ[T] T ⊗[R] S := TensorProduct.map (AlgHom.id T T) f
this :
  Eq (α := Ideal (T ⊗[R] MvPolynomial (Fin n) R))
    (Ideal.map (F := MvPolynomial (Fin n) R →+* T ⊗[R] MvPolynomial (Fin n) R)
      (algebraMap (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker f.toRingHom))
    (RingHom.ker fT)
⊢ Function.Surjective (α := T ⊗[R] MvPolynomial (Fin n) R) (β := T ⊗[R] S)
    (⇑fT : (a : T ⊗[R] MvPolynomial (Fin n) R) → T ⊗[R] S)

Tactic:
exact FiniteType.baseChangeAux_surj T hf

Premises used: Algebra.FiniteType.baseChangeAux_surj
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
⊢ CodescendsAlong.{u_4} (fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ FiniteType)
    fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
.mk _ finiteType_respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_

Premises used: RingHom.CodescendsAlong.mk, RingHom.finiteType_respectsIso
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
refine :
  ∀ (R S T : Type u_4) (x : CommRing R) (x_1 : CommRing S) (x_2 : CommRing T) (x_3 : Algebra R S) (x_4 : Algebra R T)
    (h : FaithfullyFlat (algebraMap R S)) (h' : FiniteType (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))),
    FiniteType (algebraMap R T)
⊢ CodescendsAlong.{u_4} (fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ FiniteType)
    fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
refine .mk _ finiteType_respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : FiniteType (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
rw : ∀ (h' : Algebra.FiniteType S (S ⊗[R] T)), Algebra.FiniteType R T
⊢ FiniteType (algebraMap R T)

Tactic:
rw [finiteType_algebraMap] at h' ⊢

Premises used: RingHom.finiteType_algebraMap
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Algebra.FiniteType S (S ⊗[R] T)
⊢ Module.FaithfullyFlat R S

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Algebra.FiniteType S (S ⊗[R] T)
h₁ : Module.FaithfullyFlat R S
⊢ Algebra.FiniteType S (S ⊗[R] T)

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : Module.FaithfullyFlat R S
h' : Algebra.FiniteType S (S ⊗[R] T)
⊢ Algebra.FiniteType R T

Tactic:
.of_finiteType_tensorProduct_of_faithfullyFlat S

Premises used: Algebra.FiniteType.of_finiteType_tensorProduct_of_faithfullyFlat
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : Module.FaithfullyFlat R S
h' : Algebra.FiniteType S (S ⊗[R] T)
⊢ Algebra.FiniteType R T

Tactic:
exact .of_finiteType_tensorProduct_of_faithfullyFlat S
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
⊢ CodescendsAlong.{u_4} (fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ FinitePresentation)
    fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
.mk _ finitePresentation_respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_

Premises used: RingHom.CodescendsAlong.mk, RingHom.finitePresentation_respectsIso
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
refine :
  ∀ (R S T : Type u_4) (x : CommRing R) (x_1 : CommRing S) (x_2 : CommRing T) (x_3 : Algebra R S) (x_4 : Algebra R T)
    (h : FaithfullyFlat (algebraMap R S)) (h' : FinitePresentation (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))),
    FinitePresentation (algebraMap R T)
⊢ CodescendsAlong.{u_4} (fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ FinitePresentation)
    fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
refine .mk _ finitePresentation_respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : FinitePresentation (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
rw : ∀ (h' : Algebra.FinitePresentation S (S ⊗[R] T)), Algebra.FinitePresentation R T
⊢ FinitePresentation (algebraMap R T)

Tactic:
rw [finitePresentation_algebraMap] at h' ⊢

Premises used: RingHom.finitePresentation_algebraMap
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Algebra.FinitePresentation S (S ⊗[R] T)
⊢ Module.FaithfullyFlat R S

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Algebra.FinitePresentation S (S ⊗[R] T)
h₁ : Module.FaithfullyFlat R S
⊢ Algebra.FinitePresentation S (S ⊗[R] T)

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : Module.FaithfullyFlat R S
h' : Algebra.FinitePresentation S (S ⊗[R] T)
⊢ Algebra.FinitePresentation R T

Tactic:
.of_finitePresentation_tensorProduct_of_faithfullyFlat S

Premises used: Algebra.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : Module.FaithfullyFlat R S
h' : Algebra.FinitePresentation S (S ⊗[R] T)
⊢ Algebra.FinitePresentation R T

Tactic:
exact .of_finitePresentation_tensorProduct_of_faithfullyFlat S
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
⊢ CodescendsAlong.{u_4} (fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ Finite)
    fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
.mk _ finite_respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_

Premises used: RingHom.CodescendsAlong.mk, RingHom.finite_respectsIso
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
refine :
  ∀ (R S T : Type u_4) (x : CommRing R) (x_1 : CommRing S) (x_2 : CommRing T) (x_3 : Algebra R S) (x_4 : Algebra R T)
    (h : FaithfullyFlat (algebraMap R S)) (h' : Finite (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))),
    Finite (algebraMap R T)
⊢ CodescendsAlong.{u_4} (fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ Finite)
    fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
refine .mk _ finite_respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Finite (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
rw : ∀ (h' : Module.Finite S (S ⊗[R] T)), Module.Finite R T
⊢ Finite (algebraMap R T)

Tactic:
rw [finite_algebraMap] at h' ⊢

Premises used: RingHom.finite_algebraMap
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Module.Finite S (S ⊗[R] T)
⊢ Module.FaithfullyFlat R S

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Module.Finite S (S ⊗[R] T)
h₁ : Module.FaithfullyFlat R S
⊢ Module.Finite S (S ⊗[R] T)

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : Module.FaithfullyFlat R S
h' : Module.Finite S (S ⊗[R] T)
⊢ Module.Finite R T

Tactic:
.of_finite_tensorProduct_of_faithfullyFlat S

Premises used: Module.Finite.of_finite_tensorProduct_of_faithfullyFlat
-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R S T : Type u_4
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : Module.FaithfullyFlat R S
h' : Module.Finite S (S ⊗[R] T)
⊢ Module.Finite R T

Tactic:
exact .of_finite_tensorProduct_of_faithfullyFlat S
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑f : (a : A) → S)
t : Finset A
ht : Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
H : ∀ (g : ↥t), FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S))
hker : Ideal.FG (RingHom.ker f.toRingHom)
⊢ FinitePresentation R S

Tactic:
apply Algebra.FinitePresentation.of_surjective hf

Premises used: Algebra.FinitePresentation.of_surjective
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑f : (a : A) → S)
t : Finset A
ht : Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
H : ∀ (g : ↥t), FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S))
hker :
  ∀ (g : (↑(↑t : Set A) : Type u_3)),
    Ideal.FG
      (RingHom.ker (F :=
        RingHom.{u_3, u_2} (Localization.Away (↑g : A))
          (Localization.Away (M := S) ((f.toRingHom : (a : A) → S) (↑g : A) : S)))
        (Localization.awayMap f.toRingHom (↑g : A)))
⊢ Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
apply RingHom.ker_fg_of_localizationSpan t ht

Premises used: RingHom.ker_fg_of_localizationSpan
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑f : (a : A) → S)
t : Finset A
ht : Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
H : ∀ (g : ↥t), FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S))
g : (↑(↑t : Set A) : Type u_3)
f' : AlgHom.{u_1, u_3, u_2} R (Localization.Away (↑g : A))
  (Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S)) :=
  Localization.awayMapₐ f (↑g : A)
⊢ ∀ (g : ↥t), FinitePresentation.{u_1, u_3} R (Localization.Away (↑g : A))

Tactic:
have (g : t) : Algebra.FinitePresentation R (Localization.Away g.val) :=
    haveI : Algebra.FinitePresentation A (Localization.Away g.val) :=
      IsLocalization.Away.finitePresentation g.val
    Algebra.FinitePresentation.trans R A (Localization.Away g.val)
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑f : (a : A) → S)
t : Finset A
ht : Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
H : ∀ (g : ↥t), FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S))
g : (↑(↑t : Set A) : Type u_3)
f' : AlgHom.{u_1, u_3, u_2} R (Localization.Away (↑g : A))
  (Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S)) :=
  Localization.awayMapₐ f (↑g : A)
this : ∀ (g : ↥t), FinitePresentation.{u_1, u_3} R (Localization.Away (↑g : A))
hker :
  Function.Surjective.{u_3 + 1, u_2 + 1} (α := Localization.Away (↑g : A)) (β :=
    Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S))
    (⇑f' : (a : Localization.Away (↑g : A)) → Localization.Away ((f : (a : A) → S) (↑g : A)))
⊢ Ideal.FG
    (RingHom.ker (F :=
      RingHom.{u_3, u_2} (Localization.Away (↑g : A))
        (Localization.Away (M := S) ((f.toRingHom : (a : A) → S) (↑g : A) : S)))
      (Localization.awayMap f.toRingHom (↑g : A)))

Tactic:
apply Algebra.FinitePresentation.ker_fG_of_surjective f'

Premises used: Algebra.FinitePresentation.ker_fG_of_surjective
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑f : (a : A) → S)
t : Finset A
ht : Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
H : ∀ (g : ↥t), FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S))
g : (↑(↑t : Set A) : Type u_3)
f' : AlgHom.{u_1, u_3, u_2} R (Localization.Away (↑g : A))
  (Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S)) :=
  Localization.awayMapₐ f (↑g : A)
this : ∀ (g : ↥t), FinitePresentation.{u_1, u_3} R (Localization.Away (↑g : A))
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := Localization.Away (↑g : A)) (β :=
    Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S))
    (⇑f' : (a : Localization.Away (↑g : A)) → Localization.Away ((f : (a : A) → S) (↑g : A)))

Tactic:
IsLocalization.Away.mapₐ_surjective_of_surjective _ hf

Premises used: IsLocalization.Away.mapₐ_surjective_of_surjective
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑f : (a : A) → S)
t : Finset A
ht : Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
H : ∀ (g : ↥t), FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S))
g : (↑(↑t : Set A) : Type u_3)
f' : AlgHom.{u_1, u_3, u_2} R (Localization.Away (↑g : A))
  (Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S)) :=
  Localization.awayMapₐ f (↑g : A)
this : ∀ (g : ↥t), FinitePresentation.{u_1, u_3} R (Localization.Away (↑g : A))
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := Localization.Away (↑g : A)) (β :=
    Localization.Away (M := S) ((f : (a : A) → S) (↑g : A) : S))
    (⇑f' : (a : Localization.Away (↑g : A)) → Localization.Away ((f : (a : A) → S) (↑g : A)))

Tactic:
exact IsLocalization.Away.mapₐ_surjective_of_surjective _ hf

Premises used: IsLocalization.Away.mapₐ_surjective_of_surjective
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ i ∈ s, FinitePresentation.{u_1, u_2} R (Localization.Away i)
obtain :
  ∀ (s_1 : Finset S) (h₁ : (↑s_1 : Set S) ⊆ s) (hs : Eq (α := Ideal S) (Ideal.span (↑s_1 : Set S)) ⊤),
    FinitePresentation R S
⊢ FinitePresentation R S

Tactic:
obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs

Premises used: Ideal.span_eq_top_iff_finite, Iff.mp
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
h : ∀ i ∈ s_1, FinitePresentation.{u_1, u_2} R (Localization.Away i)
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
⊢ ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))

Tactic:
replace h (i : s) : Algebra.FinitePresentation R (Localization.Away i.val) := h i (h₁ i.property)
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
apply : ∀ x ∈ (↑s : Set S), FiniteType.{u_1, u_2} R (Localization.Away x)
⊢ FiniteType R S

Tactic:
apply Algebra.FiniteType.of_span_eq_top_target s hs

Premises used: Algebra.FiniteType.of_span_eq_top_target
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
x : S
hx : x ∈ (↑s : Set S)
⊢ FinitePresentation.{u_1, u_2} R (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) x hx) : S))

Tactic:
have := h ⟨x, hx⟩
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
x : S
hx : x ∈ (↑s : Set S)
this : FinitePresentation.{u_1, u_2} R (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) x hx) : S))
⊢ FiniteType.{u_1, u_2} R (Localization.Away x)

Tactic:
infer_instance