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
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
A : Type u
inst_7 : CommSemiring A
inst_8 : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst_9 : CommSemiring T
inst_10 : Algebra R T
B : Type u
inst_11 : CommSemiring B
inst_12 : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : AlgHom.{u, v, w} R ↥φ.range ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  Eq (α := TensorProduct.{u, w, u_1} R (↥ψ.range) M)
    ((rTensor M (h'.comp φ.rangeRestrict).toLinearMap : (a : A ⊗[R] M) → ↥ψ.range ⊗[R] M) p :
      TensorProduct.{u, w, u_1} R (↥ψ.range) M)
    ((rTensor M ψ.rangeRestrict.toLinearMap : (a : B ⊗[R] M) → ↥ψ.range ⊗[R] M) q :
      TensorProduct.{u, w, u_1} R (↥ψ.range) M)
θ : RingCon.Quotient (RingCon.ker (↑φ : A →+* S)) →ₐ[R] RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)) :=
  (↑(quotientKerEquivRangeₐ ψ).symm : ↥ψ.range →ₐ[R] (RingCon.ker (↑ψ : B →+* T)).Quotient).comp
    (h'.comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range))
ht :
  (h.comp φ.range.val).comp (↑(quotientKerEquivRangeₐ φ) : (RingCon.ker (↑φ : A →+* S)).Quotient →ₐ[R] ↥φ.range) =
    ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range).comp θ)
⊢ Eq (α := RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)) ⊗[R] N)
    (f.toFun' (RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)))
      ((rTensor M
            (((↑(quotientKerEquivRangeₐ ψ).symm : ↥ψ.range →ₐ[R] (RingCon.ker (↑ψ : B →+* T)).Quotient).comp
                    (↑(quotientKerEquivRangeₐ ψ) : (RingCon.ker (↑ψ : B →+* T)).Quotient →ₐ[R] ↥ψ.range)).comp
                (mkₐ R (RingCon.ker (↑ψ : B →+* T)))).toLinearMap :
          (a : B ⊗[R] M) → (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] M)
        q))
    (f.toFun' (RingCon.Quotient (RingCon.ker (↑ψ : B →+* T)))
      ((rTensor M (toLinearMap (mkₐ R (RingCon.ker (↑ψ : B →+* T)))) :
          (a : B ⊗[R] M) → (RingCon.ker (↑ψ : B →+* T)).Quotient ⊗[R] M)
        q))

Tactic:
simp
-- 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
A : Type u
inst_7 : CommSemiring A
inst_8 : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
B : Type u
inst_9 : CommSemiring B
inst_10 : Algebra R B
q : B ⊗[R] M
ψ : B →ₐ[R] S
h : φ.range ≤ ψ.range
hpq :
  Eq (α := TensorProduct.{u, v, u_1} R (↥ψ.range) M)
    ((rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap : (a : A ⊗[R] M) → ↥ψ.range ⊗[R] M) p :
      TensorProduct.{u, v, u_1} R (↥ψ.range) M)
    ((rTensor M ψ.rangeRestrict.toLinearMap : (a : B ⊗[R] M) → ↥ψ.range ⊗[R] M) q :
      TensorProduct.{u, v, u_1} R (↥ψ.range) M)
H :
  ∀ (x : ↥φ.range),
    Eq (α := S) ((ψ.range.val.comp (Subalgebra.inclusion h) : (a : ↥φ.range) → S) x : S)
      ((AlgHom.comp (AlgHom.id R S) φ.range.val : (a : ↥φ.range) → S) x : S)
⊢ ψ.range.val.comp (Subalgebra.inclusion h) = AlgHom.comp (AlgHom.id R S) φ.range.val

Tactic:
ext x
-- 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
A : Type u
inst_7 : CommSemiring A
inst_8 : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
B : Type u
inst_9 : CommSemiring B
inst_10 : Algebra R B
q : B ⊗[R] M
ψ : B →ₐ[R] S
h : φ.range ≤ ψ.range
hpq :
  Eq (α := TensorProduct.{u, v, u_1} R (↥ψ.range) M)
    ((rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap : (a : A ⊗[R] M) → ↥ψ.range ⊗[R] M) p :
      TensorProduct.{u, v, u_1} R (↥ψ.range) M)
    ((rTensor M ψ.rangeRestrict.toLinearMap : (a : B ⊗[R] M) → ↥ψ.range ⊗[R] M) q :
      TensorProduct.{u, v, u_1} R (↥ψ.range) M)
x : ↥φ.range
⊢ Eq (α := S) ((ψ.range.val.comp (Subalgebra.inclusion h) : (a : ↥φ.range) → S) x : S)
    ((AlgHom.comp (AlgHom.id R S) φ.range.val : (a : ↥φ.range) → S) x : S)

Tactic:
simp
-- 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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
⊢ let u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p;
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p

Tactic:
set u := rTensor M (φ R s).rangeRestrict.toLinearMap p with hu

Premises used: AlgHom.toLinearMap, AlgHom.rangeRestrict, PolynomialLaw.φ, DFunLike.coe, LinearMap.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
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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
rw : Subalgebra.FG (Subalgebra.map (φ R s) ⊤)
⊢ Subalgebra.FG (AlgHom.range (φ R s))

Tactic:
rw [← Algebra.map_top]

Premises used: Algebra.map_top
-- 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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
⊢ Subalgebra.FG (Subalgebra.map (φ R s) ⊤)

Tactic:
Subalgebra.FG.map _ Algebra.FiniteType.out

Premises used: Subalgebra.FG.map, Algebra.FiniteType.out
-- 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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
⊢ Subalgebra.FG (Subalgebra.map (φ R s) ⊤)

Tactic:
exact Subalgebra.FG.map _ Algebra.FiniteType.out

Premises used: Subalgebra.FG.map, Algebra.FiniteType.out
-- 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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
⊢ Subalgebra.FG (AlgHom.range (φ R s))

Tactic:
have uFG : Subalgebra.FG (R := R) (φ R s).range := by
    rw [← Algebra.map_top]
    exact Subalgebra.FG.map _ Algebra.FiniteType.out
-- 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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
uFG : Subalgebra.FG (AlgHom.range (φ R s))
⊢ let u' : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s'))) M :=
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
        (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p';
  u' =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
        (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p'

Tactic:
set u' := rTensor M (φ R s').rangeRestrict.toLinearMap p' with hu'

Premises used: AlgHom.toLinearMap, AlgHom.rangeRestrict, PolynomialLaw.φ, DFunLike.coe, LinearMap.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
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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
uFG : Subalgebra.FG (AlgHom.range (φ R s))
u' : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s'))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
      (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
    p'
hu' :
  u' =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
        (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p'
rw : Subalgebra.FG (Subalgebra.map (φ R s') ⊤)
⊢ Subalgebra.FG (AlgHom.range (φ R s'))

Tactic:
rw [← Algebra.map_top]

Premises used: Algebra.map_top
-- 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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
uFG : Subalgebra.FG (AlgHom.range (φ R s))
u' : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s'))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
      (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
    p'
hu' :
  u' =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
        (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p'
⊢ Subalgebra.FG (Subalgebra.map (φ R s') ⊤)

Tactic:
Subalgebra.FG.map _ Algebra.FiniteType.out

Premises used: Subalgebra.FG.map, Algebra.FiniteType.out
-- 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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
uFG : Subalgebra.FG (AlgHom.range (φ R s))
u' : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s'))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
      (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
    p'
hu' :
  u' =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
        (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p'
⊢ Subalgebra.FG (Subalgebra.map (φ R s') ⊤)

Tactic:
exact Subalgebra.FG.map _ Algebra.FiniteType.out

Premises used: Subalgebra.FG.map, Algebra.FiniteType.out
-- 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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
uFG : Subalgebra.FG (AlgHom.range (φ R s))
u' : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s'))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
      (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
    p'
hu' :
  u' =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
        (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p'
⊢ Subalgebra.FG (AlgHom.range (φ R s'))

Tactic:
have u'FG : Subalgebra.FG (R := R) (φ R s').range := by
    rw [← Algebra.map_top]
    exact Subalgebra.FG.map _ Algebra.FiniteType.out
-- 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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M)
    ((rTensor M (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → S ⊗[R] M) p : S ⊗[R] M)
    ((rTensor M (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → S ⊗[R] M) p' : S ⊗[R] M)
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
uFG : Subalgebra.FG (AlgHom.range (φ R s))
u' : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s'))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
      (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
    p'
hu' :
  u' =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
        (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p'
u'FG : Subalgebra.FG (AlgHom.range (φ R s'))
⊢ Eq (α := S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s)))) : (a : ↥(φ R s).range ⊗[R] M) → S ⊗[R] M) u :
      S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s')))) : (a : ↥(φ R s').range ⊗[R] M) → S ⊗[R] M) u' :
      S ⊗[R] M)

Tactic:
simp only [hu, hu', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap,
      val_comp_rangeRestrict, h]

Premises used: AlgHom.comp_toLinearMap, AlgHom.val_comp_rangeRestrict, LinearMap.comp_apply, LinearMap.rTensor_comp
-- 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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  Eq (α := S ⊗[R] M) (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p))
    (π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
u : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
      (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
    p
hu :
  u =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s))) :
        (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s).range ⊗[R] M)
      p
uFG : Subalgebra.FG (AlgHom.range (φ R s))
u' : TensorProduct.{u, v, u_1} R (↥(AlgHom.range (φ R s'))) M :=
  (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
      (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
    p'
hu' :
  u' =
    (rTensor M (toLinearMap (AlgHom.rangeRestrict (φ R s'))) :
        (a : MvPolynomial (Fin s'.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
      p'
u'FG : Subalgebra.FG (AlgHom.range (φ R s'))
⊢ Eq (α := S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s)))) : (a : ↥(φ R s).range ⊗[R] M) → S ⊗[R] M) u :
      S ⊗[R] M)
    ((rTensor M (toLinearMap (Subalgebra.val (AlgHom.range (φ R s')))) : (a : ↥(φ R s').range ⊗[R] M) → S ⊗[R] M) u' :
      S ⊗[R] M)

Tactic:
have huu' : rTensor M (Subalgebra.val _).toLinearMap u =
    rTensor M (Subalgebra.val _).toLinearMap u' := by
    simp only [π] at h
    simp only [hu, hu', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap,
      val_comp_rangeRestrict, h]