awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
B : Subalgebra R S
hB : B.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t
obtain : ∀ (s : Finset S) (hs : AlgHom.range (φ R s) = B), ∃ (a : lifts R M S), π R M S a = t
⊢ ∃ (a : lifts R M S), π R M S a = t

Tactic:
obtain ⟨s : Finset S, hs : (PolynomialLaw.φ R s).range = B⟩ := exists_range_φ_eq_of_fg hB

Premises used: Finset, PolynomialLaw.exists_range_φ_eq_of_fg
-- 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
B : Subalgebra R S
hB : B.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t
s : Finset S
hs : AlgHom.range (φ R s) = B
obtain :
  ∀ (p : MvPolynomial (Fin s.card) R ⊗[R] M)
    (hp : (rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p = t),
    ∃ (a : lifts R M S), π R M S a = t
⊢ ∃ (a : lifts R M S), π R M S a = t

Tactic:
obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor B (le_of_eq hs.symm) ht

Premises used: le_of_eq, Eq.symm, PolynomialLaw.exists_lift_of_mem_range_rTensor
-- 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
B : Subalgebra R S
hB : B.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t
s : Finset S
hs : AlgHom.range (φ R s) = B
p : MvPolynomial (Fin s.card) R ⊗[R] M
hp : (rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p = t
⊢ ∃ (a : lifts R M S), π R M S a = t

Tactic:
⟨⟨s, p⟩, hp⟩

Premises used: Exists.intro, Sigma.mk
-- 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
B : Subalgebra R S
hB : B.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t
s : Finset S
hs : AlgHom.range (φ R s) = B
p : MvPolynomial (Fin s.card) R ⊗[R] M
hp : (rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p = t
⊢ ∃ (a : lifts R M S), π R M S a = t

Tactic:
exact ⟨⟨s, p⟩, hp⟩
-- 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
intro : ∀ (t : S ⊗[R] M), ∃ (a : lifts R M S), π R M S a = t
intro₁ :
  ∀ (t : S ⊗[R] M) (B : Subalgebra R S) (hB : B.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t),
    ∃ (a : lifts R M S), π R M S a = t
intro₂ :
  ∀ (t : S ⊗[R] M) (B : Subalgebra R S) (hB : B.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t) (s : Finset S)
    (hs : AlgHom.range (φ R s) = B), ∃ (a : lifts R M S), π R M S a = t
intro₃ :
  ∀ (t : S ⊗[R] M) (B : Subalgebra R S) (hB : B.FG)
    (ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M B.val.toLinearMap)) t) (s : Finset S)
    (hs : AlgHom.range (φ R s) = B) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
    (hp : (rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p = t),
    ∃ (a : lifts R M S), π R M S a = t
⊢ Function.Surjective (α := lifts R M S) (β := S ⊗[R] M) (π R M S)

Tactic:
classical
  intro t
  obtain ⟨B : Subalgebra R S, hB : B.FG, ht : t ∈ range _⟩ := TensorProduct.Algebra.exists_of_fg t
  obtain ⟨s : Finset S, hs : (PolynomialLaw.φ R s).range = B⟩ := exists_range_φ_eq_of_fg hB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor B (le_of_eq hs.symm) ht
  exact ⟨⟨s, p⟩, hp⟩

Premises used: Finset, LinearMap.range, Subalgebra
-- 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
obtain :
  ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
    (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
    ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M),
      (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t

Tactic:
obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t

Premises used: PolynomialLaw.π_surjective
-- 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 : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
w : ℕ
w₁ : MvPolynomial (Fin s.card) R →ₐ[R] S
w₂ : MvPolynomial (Fin s.card) R ⊗[R] M
h : (rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p = t
⊢ ∃ (n : ℕ) (ψ : MvPolynomial (Fin n) R →ₐ[R] S) (p : MvPolynomial (Fin n) R ⊗[R] M),
    (rTensor M ψ.toLinearMap : (a : MvPolynomial (Fin n) R ⊗[R] M) → S ⊗[R] M) p = t

Tactic:
use s.card, φ R s, p, ha

Premises used: PolynomialLaw.φ, Finset.card
-- 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
⊢ ∃ (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:
obtain ⟨A, hA, ht⟩ := TensorProduct.Algebra.exists_of_fg t

Premises used: TensorProduct.Algebra.exists_of_fg
-- 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
A : Subalgebra R S
hA : A.FG
ht : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t
⊢ (A ⊔ Algebra.adjoin R (↑{s} : Set S)).FG

Tactic:
have hB : Subalgebra.FG (A ⊔ Algebra.adjoin R ({s} : Finset S)) :=
    Subalgebra.FG.sup hA (Subalgebra.fg_adjoin_finset _)
-- 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
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
obtain :
  ∀ (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
⊢ ∃ (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:
obtain ⟨gen, hgen⟩ := exists_range_φ_eq_of_fg hB

Premises used: PolynomialLaw.exists_range_φ_eq_of_fg
-- 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
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)
⊢ A ≤ A ⊔ Algebra.adjoin R (↑{s} : Set S)

Tactic:
have hAB : A ≤ A ⊔ Algebra.adjoin R ({s} : Finset S) := le_sup_left
-- 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
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)
⊢ A ≤ AlgHom.range (φ R gen)

Tactic:
rw [← hgen] at hAB
-- 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
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)
obtain :
  ∀ (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
⊢ ∃ (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:
obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor _ hAB ht

Premises used: PolynomialLaw.exists_lift_of_mem_range_rTensor
-- 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
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
rw : s ∈ A ⊔ Algebra.adjoin R (↑{s} : Set S)
⊢ Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R gen)) s

Tactic:
rw [hgen]
-- 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
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
a : s ∈ (↑A : Set S) ⊔ (↑(Algebra.adjoin R (↑{s} : Set S)) : Set S)
⊢ s ∈ A ⊔ Algebra.adjoin R (↑{s} : Set S)

Tactic:
apply Algebra.subset_adjoin

Premises used: Algebra.subset_adjoin
-- 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
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
a : s ∈ A ∨ Membership.mem (γ := Subalgebra R S) R[s] s
⊢ s ∈ (↑A : Set S) ⊔ (↑(Algebra.adjoin R (↑{s} : Set S)) : Set S)

Tactic:
simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]

Premises used: Set.mem_union, Finset.coe_singleton, Set.sup_eq_union, SetLike.mem_coe
-- 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
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
⊢ s ∈ A ∨ Membership.mem (γ := Subalgebra R S) R[s] s

Tactic:
Or.inr (Algebra.subset_adjoin rfl)

Premises used: Algebra.subset_adjoin, Or.inr, rfl
-- 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
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
⊢ s ∈ A ∨ Membership.mem (γ := Subalgebra R S) R[s] s

Tactic:
exact Or.inr (Algebra.subset_adjoin rfl)

Premises used: Algebra.subset_adjoin, Or.inr, rfl
-- 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
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
⊢ Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R gen)) s

Tactic:
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)
-- 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
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
w : ℕ
w₁ : MvPolynomial (Fin gen.card) R →ₐ[R] S
w₂ : MvPolynomial (Fin gen.card) R ⊗[R] M
w₃ : MvPolynomial (Fin gen.card) R
left : (rTensor M (toLinearMap (φ R gen)) : (a : MvPolynomial (Fin gen.card) R ⊗[R] M) → S ⊗[R] M) p = t
right :
  (φ R gen : (a : MvPolynomial (Fin gen.card) R) → S)
      (Exists.choose (p := fun (y : MvPolynomial (Fin gen.card) R) ↦
        (toRingHom (φ R gen) : (a : MvPolynomial (Fin gen.card) R) → S) y = s) hs) =
    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:
use gen.card, φ R gen, p, hs.choose, hp, hs.choose_spec

Premises used: Exists.choose_spec, PolynomialLaw.φ, Finset.card, Exists.choose
-- 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
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
h : ∀ (t : S ⊗[R] M), f.toFun' S t = toFun S f t
⊢ Eq (α := S ⊗[R] M → S ⊗[R] N) (f.toFun' S) (toFun S f)

Tactic:
ext t
-- 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
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
t : S ⊗[R] M
h :
  ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
    (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
    f.toFun' S t = toFun S f t
⊢ f.toFun' S t = toFun S f t

Tactic:
obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t

Premises used: PolynomialLaw.π_surjective
-- 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
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
h :
  f.toFun' S t = f.toFun' S ((rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p)
⊢ f.toFun' S t = toFun S f t

Tactic:
simp only [f.toFun_eq_rTensor_φ_toFun' ha, f.isCompat_apply']

Premises used: PolynomialLaw.toFun_eq_rTensor_φ_toFun', PolynomialLaw.isCompat_apply'
-- 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
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
⊢ f.toFun' S t = f.toFun' S ((rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p)

Tactic:
congr_arg _ ha.symm

Premises used: congr_arg, Eq.symm
-- 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
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
⊢ f.toFun' S t = f.toFun' S ((rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p)

Tactic:
exact congr_arg _ ha.symm

Premises used: congr_arg, Eq.symm
-- 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
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
obtain :
  ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
    (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
    Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
      (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)
⊢ Eq (α := T ⊗[R] N) ((rTensor N h.toLinearMap : (a : S ⊗[R] N) → T ⊗[R] N) (toFun S f t) : T ⊗[R] N)
    (toFun T f ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t) : T ⊗[R] N)

Tactic:
obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t

Premises used: PolynomialLaw.π_surjective
-- 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
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
x : S
hx : Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R s)) x
simp :
  ∀ (hx_1 : Membership.mem (γ := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) x),
    Membership.mem (α := T) (γ := Subalgebra R T) (Algebra.adjoin R (↑s' : Set T))
      ((h.comp (Subalgebra.val (AlgHom.range (φ R s))) : (a : ↥(φ R s).range) → T)
          (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R s)) x) x hx) :
        T)
⊢ Membership.mem (α := T) (γ := Subalgebra R T) (AlgHom.range (φ R s'))
    ((h.comp (Subalgebra.val (AlgHom.range (φ R s))) : (a : ↥(φ R s).range) → T)
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R s)) x) x hx) :
      T)

Tactic:
simp only [range_φ] at hx ⊢

Premises used: PolynomialLaw.range_φ
-- 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
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type v
inst_5 : CommSemiring S
inst_6 : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst_7 : CommSemiring T
inst_8 : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
x : S
hx_1 : Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R s)) x
hx : Membership.mem (γ := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) x
simp : Membership.mem (α := T) (Subalgebra.map h (Algebra.adjoin R (↑s : Set S))) ((h : (a : S) → T) x : T)
⊢ Membership.mem (α := T) (γ := Subalgebra R T) (Algebra.adjoin R (↑s' : Set T))
    ((h.comp (Subalgebra.val (AlgHom.range (φ R s))) : (a : ↥(φ R s).range) → T)
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (AlgHom.range (φ R s)) x) x hx_1) :
      T)

Tactic:
simp only [AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply, Finset.coe_image,
      Algebra.adjoin_image, s']

Premises used: Finset.coe_image, Subalgebra.coe_val, Algebra.adjoin_image, AlgHom.coe_comp, Function.comp_apply