awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
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 : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : Eq (α := Subalgebra T (T ⊗[R] S)) (adjoin T (↑s : Set (T ⊗[R] S))) ⊤
k : (x : ↥s) → ℕ
t : (x : ↥s) → Fin (k x) → T
m : (x : ↥s) → Fin (k x) → S
h : ∀ (x : ↥s), (↑x : T ⊗[R] S) = ∑ j : Fin (k x), t x j ⊗ₜ[R] m x j
f : MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[R] S :=
  MvPolynomial.aeval fun (x : (x : ↥s) × Fin (k x)) ↦
    match (motive := (x : ↥s) × Fin (k x) → S) x with
    | ⟨x, i⟩ => m x i
⊢ Function.Surjective (α := T ⊗[R] MvPolynomial ((x : ↥s) × Fin (k x)) R) (β := T ⊗[R] S)
    (⇑(TensorProduct.map (AlgHom.id T T) f : T ⊗[R] MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[T] T ⊗[R] S) :
      (a : T ⊗[R] MvPolynomial ((x : ↥s) × Fin (k x)) R) → T ⊗[R] S)
have rw : (↑s : Set (T ⊗[R] S)) ⊆
  (↑(AlgHom.range (A := T ⊗[R] MvPolynomial ((x : ↥s) × Fin (k x)) R)
          (TensorProduct.map (AlgHom.id T T) f : T ⊗[R] MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[T] T ⊗[R] S) :
        Subalgebra T (T ⊗[R] S)) :
    Set (T ⊗[R] S))
Tactic: rw [← AlgHom.range_eq_top, _root_.eq_top_iff, ← hs, adjoin_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
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 : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : Eq (α := Subalgebra T (T ⊗[R] S)) (adjoin T (↑s : Set (T ⊗[R] S))) ⊤
k : (x : ↥s) → ℕ
t : (x : ↥s) → Fin (k x) → T
m : (x : ↥s) → Fin (k x) → S
h : ∀ (x : ↥s), (↑x : T ⊗[R] S) = ∑ j : Fin (k x), t x j ⊗ₜ[R] m x j
f : MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[R] S :=
  MvPolynomial.aeval fun (x : (x : ↥s) × Fin (k x)) ↦
    match (motive := (x : ↥s) × Fin (k x) → S) x with
    | ⟨x, i⟩ => m x i
x : T ⊗[R] S
hx : x ∈ (↑s : Set (T ⊗[R] S))
i : ↥s := Subtype.mk (p := fun (x : T ⊗[R] S) ↦ x ∈ s) x hx
⊢ x ∈
    (↑(AlgHom.range (A := T ⊗[R] MvPolynomial ((x : ↥s) × Fin (k x)) R)
            (TensorProduct.map (AlgHom.id T T) f : T ⊗[R] MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[T] T ⊗[R] S) :
          Subalgebra T (T ⊗[R] S)) :
      Set (T ⊗[R] S))
have h₁ : (AlgHom.toRingHom (TensorProduct.map (AlgHom.id T T) f : T ⊗[R] MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[T] T ⊗[R] S) :
      (a : T ⊗[R] MvPolynomial ((x : ↥s) × Fin (k x)) R) → T ⊗[R] S)
    (∑ j : Fin (k i), t i j ⊗ₜ[R] MvPolynomial.X (Sigma.mk (β := fun (x : ↥s) ↦ Fin (k x)) i j)) =
  x
Tactic: use ∑ (j : Fin (k i)), t i j ⊗ₜ MvPolynomial.X ⟨i, j⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
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 : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : Eq (α := Subalgebra T (T ⊗[R] S)) (adjoin T (↑s : Set (T ⊗[R] S))) ⊤
k : (x : ↥s) → ℕ
t : (x : ↥s) → Fin (k x) → T
m : (x : ↥s) → Fin (k x) → S
h : ∀ (x : ↥s), (↑x : T ⊗[R] S) = ∑ j : Fin (k x), t x j ⊗ₜ[R] m x j
f : MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[R] S :=
  MvPolynomial.aeval fun (x : (x : ↥s) × Fin (k x)) ↦
    match (motive := (x : ↥s) × Fin (k x) → S) x with
    | ⟨x, i⟩ => m x i
⊢ Function.Surjective (α := MvPolynomial ((x : ↥s) × Fin (k x)) R) (β := S)
    (⇑f : (a : MvPolynomial ((x : ↥s) × Fin (k x)) R) → S)
have hf : Function.Surjective (α := T ⊗[R] MvPolynomial ((x : ↥s) × Fin (k x)) R) (β := T ⊗[R] S)
  (⇑(TensorProduct.map (AlgHom.id T T) f : T ⊗[R] MvPolynomial ((x : ↥s) × Fin (k x)) R →ₐ[T] T ⊗[R] S) :
    (a : T ⊗[R] MvPolynomial ((x : ↥s) × Fin (k x)) R) → T ⊗[R] S)
Tactic: have hf : Function.Surjective (Algebra.TensorProduct.map (.id T T) f) := by
    rw [← AlgHom.range_eq_top, _root_.eq_top_iff, ← hs, adjoin_le_iff]
    intro x hx
    let i : s := ⟨x, hx⟩
    use ∑ (j : Fin (k i)), t i j ⊗ₜ MvPolynomial.X ⟨i, j⟩
    simp [f, ← h, i]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
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)
⊢ FinitePresentation R S
have this : FiniteType R S
Tactic: have : Algebra.FiniteType R S := .of_finiteType_tensorProduct_of_faithfullyFlat T
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
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)
this : FiniteType R S
⊢ FinitePresentation R S
have this₁ : ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
Tactic: rw [Algebra.FiniteType.iff_quotient_mvPolynomial''] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
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)
this :
  ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S)
      (⇑f : (a : MvPolynomial (Fin n) R) → S)
⊢ FinitePresentation R S
have obtain : ∀ (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)),
  FinitePresentation R S
Tactic: obtain ⟨n, f, hf⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
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)
⊢ FinitePresentation R S
have this : Module.FaithfullyFlat (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R)
Tactic: have : Module.FaithfullyFlat (MvPolynomial (Fin n) R) (T ⊗[R] MvPolynomial (Fin n) R) :=
    .of_linearEquiv _ _ (Algebra.TensorProduct.commRight _ _ _).symm.toLinearEquiv
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
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
⊢ FinitePresentation R S
have 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))
Tactic: refine .of_surjective hf (.of_FG_map_of_faithfullyFlat (S := T ⊗[R] MvPolynomial (Fin n) R) ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
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
⊢ 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))
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
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)
⊢ 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))
have rw : Ideal.FG (RingHom.ker fT)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
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)
⊢ Ideal.FG (RingHom.ker fT)
have hf₁ : Function.Surjective (α := T ⊗[R] MvPolynomial (Fin n) R) (β := T ⊗[R] S)
  (⇑fT : (a : T ⊗[R] MvPolynomial (Fin n) R) → T ⊗[R] S)
Tactic: apply ker_fG_of_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
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
have 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)
Tactic: refine .mk _ finiteType_respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
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))
⊢ FiniteType (algebraMap R T)
have rw : ∀ (h' : Algebra.FiniteType S (S ⊗[R] T)), Algebra.FiniteType R T
Tactic: rw [finiteType_algebraMap] at h' ⊢
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
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)
⊢ Algebra.FiniteType R T
have h₁ : Module.FaithfullyFlat R S
Tactic: rw [faithfullyFlat_algebraMap_iff] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
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
have 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)
Tactic: refine .mk _ finitePresentation_respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
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))
⊢ FinitePresentation (algebraMap R T)
have rw : ∀ (h' : Algebra.FinitePresentation S (S ⊗[R] T)), Algebra.FinitePresentation R T
Tactic: rw [finitePresentation_algebraMap] at h' ⊢
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
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)
⊢ Algebra.FinitePresentation R T
have h₁ : Module.FaithfullyFlat R S
Tactic: rw [faithfullyFlat_algebraMap_iff] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
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
have 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)
Tactic: refine .mk _ finite_respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (goal)
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))
⊢ Finite (algebraMap R T)
have rw : ∀ (h' : Module.Finite S (S ⊗[R] T)), Module.Finite R T
Tactic: rw [finite_algebraMap] at h' ⊢
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Descent (hypothesis)
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.Finite R T
have h₁ : Module.FaithfullyFlat R S
Tactic: rw [faithfullyFlat_algebraMap_iff] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
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))
⊢ FinitePresentation R S
have hker : Ideal.FG (RingHom.ker f.toRingHom)
Tactic: apply Algebra.FinitePresentation.of_surjective hf
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
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))
⊢ Ideal.FG (RingHom.ker f.toRingHom)
have 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)))
Tactic: apply RingHom.ker_fg_of_localizationSpan t ht
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (hypothesis)
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)
⊢ 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)))
have this : ∀ (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)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
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))
⊢ 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)))
have 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)))
Tactic: apply Algebra.FinitePresentation.ker_fG_of_surjective f'
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
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)
⊢ FinitePresentation R S
have obtain : ∀ (s_1 : Finset S) (h₁ : (↑s_1 : Set S) ⊆ s) (hs : Eq (α := Ideal S) (Ideal.span (↑s_1 : Set S)) ⊤),
  FinitePresentation R S
Tactic: obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (hypothesis)
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)) ⊤
⊢ FinitePresentation R S
have h₂ : ∀ (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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
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))
⊢ FiniteType R S
have apply : ∀ x ∈ (↑s : Set S), FiniteType.{u_1, u_2} R (Localization.Away x)
Tactic: apply Algebra.FiniteType.of_span_eq_top_target s hs
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (hypothesis)
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)
⊢ FiniteType.{u_1, u_2} R (Localization.Away x)
have this : FinitePresentation.{u_1, u_2} R (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) x hx) : S))
Tactic: have := h ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (hypothesis)
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))
⊢ FinitePresentation R S
have hfintype : FiniteType R S
Tactic: have hfintype : Algebra.FiniteType R S := by
    apply Algebra.FiniteType.of_span_eq_top_target s hs
    intro x hx
    have := h ⟨x, hx⟩
    infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
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))
hfintype : FiniteType R S
⊢ FinitePresentation R S
have obtain : ∀ (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)),
  FinitePresentation R S
Tactic: obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp hfintype
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
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))
hfintype : FiniteType 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)
⊢ Membership.mem (γ := Ideal S) (Ideal.span (↑s : Set S)) 1
have rw : Membership.mem (γ := Ideal S) ⊤ 1
Tactic: rw [hs]