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
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
s : S
x : ↥I
⊢ (f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) = HSMul.hSMul (β := S) s ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S)

Tactic:
have : f (s ⊗ₜ[R] x) = s • f (1 ⊗ₜ x) := by simp [f]
-- 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
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
s : S
x : ↥I
this : (f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) = HSMul.hSMul (β := S) s ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S)
refine_2 :
  Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    (HSMul.hSMul (β := S) s ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S))
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) : S)

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
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
s : S
x : ↥I
this : (f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) = HSMul.hSMul (β := S) s ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S)
refine_2 :
  Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S)
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    (HSMul.hSMul (β := S) s ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S))

Tactic:
apply Ideal.mul_mem_left

Premises used: Ideal.mul_mem_left
-- 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
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
s : S
x : ↥I
this : (f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) = HSMul.hSMul (β := S) s ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S)
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) (1 ⊗ₜ[R] x) : S)

Tactic:
simpa [f, Algebra.smul_def] using Ideal.mem_map_of_mem _ x.2

Premises used: Ideal.mem_map_of_mem, Algebra.smul_def, Subtype.property
-- 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
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
x : S ⊗[R] ↥I
refine_2 :
  Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) 0 : S)
refine_2₁ :
  ∀ (x y : S ⊗[R] ↥I),
    Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
        ((f : (a : S ⊗[R] ↥I) → S) x : S) →
      Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
          ((f : (a : S ⊗[R] ↥I) → S) y : S) →
        Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
          ((f : (a : S ⊗[R] ↥I) → S) (x + y) : S)
refine_2₂ :
  ∀ (s : S) (x : ↥I),
    Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
      ((f : (a : S ⊗[R] ↥I) → S) (s ⊗ₜ[R] x) : S)
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((f : (a : S ⊗[R] ↥I) → S) x : S)

Tactic:
induction x with
      | zero => simp
      | add _ _ _ _ => simp_all [Ideal.add_mem]
      | tmul s x =>
        have : f (s ⊗ₜ[R] x) = s • f (1 ⊗ₜ x) := by simp [f]
        rw [this]
        apply Ideal.mul_mem_left
        simpa [f, Algebra.smul_def] using Ideal.mem_map_of_mem _ x.2

Premises used: Ideal.add_mem, Algebra.smul_def, TensorProduct.tmul, Ideal.mul_mem_left
-- 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
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
⊢ Ideal.map (F := R →+* S) (algebraMap R S) I = f.range

Tactic:
have : I.map (algebraMap R S) = LinearMap.range f := by
    refine le_antisymm ?_ ?_
    · rw [Ideal.map_le_iff_le_comap]
      intro x hx
      use 1 ⊗ₜ ⟨x, hx⟩
      simp [f, Algebra.smul_def]
    · rintro - ⟨x, rfl⟩
      induction x with
      | zero => simp
      | add _ _ _ _ => simp_all [Ideal.add_mem]
      | tmul s x =>
        have : f (s ⊗ₜ[R] x) = s • f (1 ⊗ₜ x) := by simp [f]
        rw [this]
        apply Ideal.mul_mem_left
        simpa [f, Algebra.smul_def] using Ideal.mem_map_of_mem _ x.2
-- 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
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
this : Ideal.map (F := R →+* S) (algebraMap R S) I = f.range
e : S ⊗[R] ↥I ≃ₗ[S] ↥(Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  LinearEquiv.ofInjective f hf ≪≫ₗ LinearEquiv.ofEq f.range (Ideal.map (F := R →+* S) (algebraMap R S) I) ⋯
rwa : Module.Finite S ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)
rwa₁ rwa₂ rwa₃ rwa₄ : Submodule.FG.{u_2, u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
⊢ Module.Finite S (S ⊗[R] ↥I)

Tactic:
rwa [Module.Finite.equiv_iff e, Module.Finite.iff_fg]

Premises used: Module.Finite.equiv_iff, Module.Finite.iff_fg
-- 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
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
this : Ideal.map (F := R →+* S) (algebraMap R S) I = f.range
e : S ⊗[R] ↥I ≃ₗ[S] ↥(Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  LinearEquiv.ofInjective f hf ≪≫ₗ LinearEquiv.ofEq f.range (Ideal.map (F := R →+* S) (algebraMap R S) I) ⋯
⊢ Module.Finite S (S ⊗[R] ↥I)

Tactic:
have : Module.Finite S (S ⊗[R] ↥I) := by
    rwa [Module.Finite.equiv_iff e, Module.Finite.iff_fg]
-- 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
inst_3 : Module.FaithfullyFlat R S
I : Ideal R
hI : FG.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
f : S ⊗[R] ↥I →ₗ[S] S :=
  ((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
    (((AlgebraTensorModule.lTensor S S : (↥I →ₗ[R] R) →ₗ[R] S ⊗[R] ↥I →ₗ[S] S ⊗[R] R) :
          (a : ↥I →ₗ[R] R) → S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
        (Submodule.subtype I) :
      S ⊗[R] ↥I →ₗ[S] S ⊗[R] R)
hf : Function.Injective (α := S ⊗[R] ↥I) (β := S) (⇑f : (a : S ⊗[R] ↥I) → S)
this_1 : Ideal.map (F := R →+* S) (algebraMap R S) I = f.range
e : S ⊗[R] ↥I ≃ₗ[S] ↥(Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  LinearEquiv.ofInjective f hf ≪≫ₗ LinearEquiv.ofEq f.range (Ideal.map (F := R →+* S) (algebraMap R S) I) ⋯
this : Module.Finite S (S ⊗[R] ↥I)
⊢ Module.Finite R ↥I

Tactic:
apply Module.Finite.of_finite_tensorProduct_of_faithfullyFlat S

Premises used: Module.Finite.of_finite_tensorProduct_of_faithfullyFlat
-- 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 : FiniteType T (T ⊗[R] S)
obtain :
  ∀ (s : Finset (T ⊗[R] S)) (hs : Eq (α := Subalgebra T (T ⊗[R] S)) (adjoin T (↑s : Set (T ⊗[R] S))) ⊤), FiniteType R S
⊢ FiniteType R S

Tactic:
obtain ⟨s, hs⟩ := Algebra.FiniteType.out (R := T) (A := T ⊗[R] S)

Premises used: Algebra.FiniteType.out
-- 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 : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : Eq (α := Subalgebra T (T ⊗[R] S)) (adjoin T (↑s : Set (T ⊗[R] S))) ⊤
⊢ ∀ (x : ↥s), ∃ (k : ℕ) (m : Fin k → T) (n : Fin k → S), (↑x : T ⊗[R] S) = ∑ j : Fin k, m j ⊗ₜ[R] n j

Tactic:
have (x : s) := TensorProduct.exists_sum_tmul_eq x.1
-- 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 : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : Eq (α := Subalgebra T (T ⊗[R] S)) (adjoin T (↑s : Set (T ⊗[R] S))) ⊤
this : ∀ (x : ↥s), ∃ (k : ℕ) (m : Fin k → T) (n : Fin k → S), (↑x : T ⊗[R] S) = ∑ j : Fin k, m j ⊗ₜ[R] n j
choose :
  ∀ (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), FiniteType R S
⊢ FiniteType R S

Tactic:
choose k t m h using 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 : 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
apply :
  Function.Surjective (α := MvPolynomial ((x : ↥s) × Fin (k x)) R) (β := S)
    (⇑f : (a : MvPolynomial ((x : ↥s) × Fin (k x)) R) → S)
⊢ FiniteType R S

Tactic:
apply Algebra.FiniteType.of_surjective f

Premises used: Algebra.FiniteType.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 : 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
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))
⊢ 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:
rw [← AlgHom.range_eq_top, _root_.eq_top_iff, ← hs, adjoin_le_iff]

Premises used: eq_top_iff, AlgHom.range_eq_top, Algebra.adjoin_le_iff
-- 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 : 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
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
⊢ 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))

Tactic:
use ∑ (j : Fin (k i)), t i j ⊗ₜ MvPolynomial.X ⟨i, j⟩

Premises used: MvPolynomial.X, Fin
-- 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 : 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
⊢ (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:
simp [f, ← h, i]
-- 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 : 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)

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]
-- 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 : 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
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)
⊢ Function.Surjective (α := MvPolynomial ((x : ↥s) × Fin (k x)) R) (β := S)
    (⇑f : (a : MvPolynomial ((x : ↥s) × Fin (k x)) R) → S)

Tactic:
(Module.FaithfullyFlat.lTensor_surjective_iff_surjective _ T _).mp hf

Premises used: Multiset.sum, Multiset.foldr, Module.FaithfullyFlat.lTensor_surjective_iff_surjective, Finsupp.sum, MvPolynomial.eval₂, Iff.mp, Finset.sum
-- 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 : 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
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)
⊢ Function.Surjective (α := MvPolynomial ((x : ↥s) × Fin (k x)) R) (β := S)
    (⇑f : (a : MvPolynomial ((x : ↥s) × Fin (k x)) R) → S)

Tactic:
exact (Module.FaithfullyFlat.lTensor_surjective_iff_surjective _ T _).mp hf

Premises used: Module.FaithfullyFlat.lTensor_surjective_iff_surjective, Iff.mp
-- 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)
⊢ FiniteType R S

Tactic:
have : Algebra.FiniteType R S := .of_finiteType_tensorProduct_of_faithfullyFlat T
-- 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)
this : FiniteType R S
⊢ ∃ (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

Premises used: Algebra.FiniteType.iff_quotient_mvPolynomial''
-- 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)
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)
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
⊢ FinitePresentation R S

Tactic:
obtain ⟨n, f, hf⟩ := 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)
⊢ 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
-- 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
⊢ FinitePresentation R S

Tactic:
.of_surjective hf (.of_FG_map_of_faithfullyFlat (S := T ⊗[R] MvPolynomial (Fin n) R) ?_)

Premises used: Ideal.FG.of_FG_map_of_faithfullyFlat, Algebra.FinitePresentation.of_surjective