-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type v
inst_3 : CommSemiring S
inst_4 : Algebra R S
t : S ⊗[R] M
s : S
obtain :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
obtain₁ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
obtain₂ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG) (gen : Finset S)
    (hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
obtain₃ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG) (gen : Finset S)
    (hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S))
    (hAB : A ≤ A ⊔ Algebra.adjoin R (↑{s} : Set S)),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
obtain₄ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG) (gen : Finset S)
    (hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)) (hAB : A ≤ AlgHom.range (φ R gen)),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
obtain₅ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG) (gen : Finset S)
    (hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)) (hAB : A ≤ AlgHom.range (φ R gen))
    (p : MvPolynomial (Fin gen.card) R ⊗[R] M)
    (hp : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
obtain₆ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (hB : (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG) (gen : Finset S)
    (hgen : AlgHom.range (φ R gen) = A ⊔ Algebra.adjoin R (↑{s} : Set S)) (hAB : A ≤ AlgHom.range (φ R gen))
    (p : MvPolynomial (Fin gen.card) R ⊗[R] M)
    (hp : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t)
    (hs : Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R gen)) s),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
        (ψ : (a : MvPolynomial (Fin n) R) → S) q = s
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M) (q : MvPolynomial (Fin n) R),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t ∧
      (ψ : (a : MvPolynomial (Fin n) R) → S) q = s

Tactic:
classical
  obtain ⟨A, hA, ht⟩ := TensorProduct.Algebra.exists_of_fg t
  have hB : Subalgebra.FG (A ⊔ Algebra.adjoin R ({s} : Finset S)) :=
    Subalgebra.FG.sup hA (Subalgebra.fg_adjoin_finset _)
  obtain ⟨gen, hgen⟩ := exists_range_φ_eq_of_fg hB
  have hAB : A ≤ A ⊔ Algebra.adjoin R ({s} : Finset S) := le_sup_left
  rw [← hgen] at hAB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor _ hAB ht
  have hs : s ∈ (φ R gen).range := by
    rw [hgen]
    apply Algebra.subset_adjoin
    simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]
    exact Or.inr (Algebra.subset_adjoin rfl)
  use gen.card, φ R gen, p, hs.choose, hp, hs.choose_spec

Premises used: TensorProduct.Algebra.exists_of_fg