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
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
⊢ Membership.mem (α := T) (Subalgebra.map h (Algebra.adjoin R (↑s : Set S))) ((h : (a : S) → T) x : T)

Tactic:
⟨x, hx, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, 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
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
⊢ Membership.mem (α := T) (Subalgebra.map h (Algebra.adjoin R (↑s : Set S))) ((h : (a : S) → T) x : T)

Tactic:
exact ⟨x, hx, 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
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
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
hf :
  ∀ (p : Fin s.card),
    Eq.{w + 1} (α := T) ((AlgHom.comp (φ R s') (rename j) : (a : MvPolynomial (Fin s.card) R) → T) (X p) : T)
      ((h.comp (φ R s) : (a : MvPolynomial (Fin s.card) R) → T) (X p) : T)
⊢ AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)

Tactic:
ext p
-- 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_1 : 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_1) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
p : Fin s.card
hf :
  Eq.{w + 1} (α := T)
    ((aeval ((fun (n : Fin s'.card) ↦ (↑((s'.equivFin.symm : (a : Fin s'.card) → ↥s') n) : T)) ∘ j) :
          (a : MvPolynomial (Fin s.card) R) → T)
        (X p) :
      T)
    ((aeval fun (i : Fin s.card) ↦ (h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) i) : S) :
          (a : MvPolynomial (Fin s.card) R) → T)
        (X p) :
      T)
⊢ Eq.{w + 1} (α := T) ((AlgHom.comp (φ R s') (rename j) : (a : MvPolynomial (Fin s.card) R) → T) (X p) : T)
    ((h.comp (φ R s) : (a : MvPolynomial (Fin s.card) R) → T) (X p) : T)

Tactic:
simp only [φ, AlgHom.comp_apply, aeval_rename, comp_aeval]

Premises used: AlgHom.comp_apply, MvPolynomial.comp_aeval, PolynomialLaw.φ, MvPolynomial.aeval_rename
-- 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_1 : 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_1) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
p : Fin s.card
hf :
  Eq.{w + 1} (α := Fin s.card → T)
    ((fun (n : Fin s'.card) ↦ (↑((s'.equivFin.symm : (a : Fin s'.card) → ↥s') n) : T)) ∘ j) fun (i : Fin s.card) ↦
    (h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) i) : S)
⊢ Eq.{w + 1} (α := T)
    ((aeval ((fun (n : Fin s'.card) ↦ (↑((s'.equivFin.symm : (a : Fin s'.card) → ↥s') n) : T)) ∘ j) :
          (a : MvPolynomial (Fin s.card) R) → T)
        (X p) :
      T)
    ((aeval fun (i : Fin s.card) ↦ (h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) i) : S) :
          (a : MvPolynomial (Fin s.card) R) → T)
        (X p) :
      T)

Tactic:
congr
-- 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_1 : 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_1) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
p : Fin s.card
hf :
  ∀ (n : Fin s.card),
    Eq.{w + 1} (α := T) (((fun (n : Fin s'.card) ↦ (↑((s'.equivFin.symm : (a : Fin s'.card) → ↥s') n) : T)) ∘ j) n : T)
      ((h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S) : T)
⊢ Eq.{w + 1} (α := Fin s.card → T)
    ((fun (n : Fin s'.card) ↦ (↑((s'.equivFin.symm : (a : Fin s'.card) → ↥s') n) : T)) ∘ j) fun (i : Fin s.card) ↦
    (h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) i) : S)

Tactic:
ext n
-- 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_1 : 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_1) = t
s' : Finset T := Finset.image (⇑h : (a : S) → T) s
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
p n : Fin s.card
⊢ Eq.{w + 1} (α := T) (((fun (n : Fin s'.card) ↦ (↑((s'.equivFin.symm : (a : Fin s'.card) → ↥s') n) : T)) ∘ j) n : T)
    ((h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S) : T)

Tactic:
simp only [Function.comp_apply, Equiv.symm_apply_apply, j]

Premises used: Equiv.symm_apply_apply, Function.comp_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
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
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
⊢ AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)

Tactic:
have eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s) := by
    ext p
    simp only [φ, AlgHom.comp_apply, aeval_rename, comp_aeval]
    congr
    ext n
    simp only [Function.comp_apply, Equiv.symm_apply_apply, j]
-- 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
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
⊢ Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)

Tactic:
simp only [← ha, π, p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap, eq_h_comp]

Premises used: AlgHom.comp_toLinearMap, LinearMap.comp_apply, PolynomialLaw.π, 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
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
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
⊢ Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)

Tactic:
have ha' : π R M T (⟨s', p'⟩ : lifts R M T) = rTensor M h.toLinearMap t := by
    simp only [← ha, π, p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap, eq_h_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
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
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
ha' :
  Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)
rw :
  Eq (α := T ⊗[R] N)
    ((rTensor N (h.comp (φ R s)).toLinearMap : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → T ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s.card) R) p) :
      T ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] N) → T ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s'.card) R) p') :
      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:
rw [toFun_eq_rTensor_φ_toFun' f ha, toFun_eq_rTensor_φ_toFun' f ha', ← LinearMap.comp_apply,
    ← rTensor_comp, ← comp_toLinearMap]

Premises used: AlgHom.comp_toLinearMap, PolynomialLaw.toFun_eq_rTensor_φ_toFun', 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
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
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
ha' :
  Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)
hh' : AlgHom.comp (Subalgebra.val (AlgHom.range (φ R s'))) h' = h.comp (Subalgebra.val (AlgHom.range (φ R s)))
hpq :
  Eq (α := TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
    ((rTensor M (h'.comp (AlgHom.rangeRestrict (φ R s))).toLinearMap :
          (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
        p :
      TensorProduct.{u, w, 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' :
      TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
⊢ Eq (α := T ⊗[R] N)
    ((rTensor N (h.comp (φ R s)).toLinearMap : (a : MvPolynomial (Fin s.card) R ⊗[R] N) → T ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s.card) R) p) :
      T ⊗[R] N)
    ((rTensor N (toLinearMap (φ R s')) : (a : MvPolynomial (Fin s'.card) R ⊗[R] N) → T ⊗[R] N)
        (f.toFun' (MvPolynomial (Fin s'.card) R) p') :
      T ⊗[R] N)

Tactic:
apply toFun'_eq_of_diagram f p p' h h'

Premises used: PolynomialLaw.toFun'_eq_of_diagram
-- 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
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
ha' :
  Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)
⊢ AlgHom.comp (Subalgebra.val (AlgHom.range (φ R s'))) h' = h.comp (Subalgebra.val (AlgHom.range (φ R s)))

Tactic:
simp only [val_comp_codRestrict, h']

Premises used: AlgHom.val_comp_codRestrict
-- 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
h' : AlgHom.{u, v, w} R ↥(AlgHom.range (φ R s)) ↥(AlgHom.range (φ R s')) :=
  AlgHom.codRestrict (h.comp (Subalgebra.val (AlgHom.range (φ R s)))) (AlgHom.range (φ R s')) ⋯
j : Fin s.card → Fin s'.card :=
  Function.comp (β := ↥s') (⇑s'.equivFin : (a : ↥s') → Fin s'.card)
    ((fun (x : ↥s) ↦
        match (motive := ↥s → ↥s') x with
        | ⟨x, hx⟩ => Subtype.mk (p := fun (x : T) ↦ x ∈ s') ((h : (a : S) → T) x) ⋯) ∘
      (⇑s.equivFin.symm : (a : Fin s.card) → ↥s))
eq_h_comp : AlgHom.comp (φ R s') (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M :=
  (rTensor M (toLinearMap (rename j)) : (a : MvPolynomial (Fin s.card) R ⊗[R] M) → MvPolynomial (Fin s'.card) R ⊗[R] M)
    p
ha' :
  Eq (α := T ⊗[R] M) (π R M T (Sigma.mk (β := fun (s : Finset T) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s' p'))
    ((rTensor M h.toLinearMap : (a : S ⊗[R] M) → T ⊗[R] M) t)
hpq :
  Eq (α := TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
    ((rTensor M (h'.comp (AlgHom.rangeRestrict (φ R s))).toLinearMap :
          (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
        p :
      TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
    ((rTensor M (toLinearMap (AlgHom.comp (AlgHom.rangeRestrict (φ R s')) (rename j))) :
          (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
        p :
      TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
⊢ Eq (α := TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)
    ((rTensor M (h'.comp (AlgHom.rangeRestrict (φ R s))).toLinearMap :
          (a : MvPolynomial (Fin s.card) R ⊗[R] M) → ↥(φ R s').range ⊗[R] M)
        p :
      TensorProduct.{u, w, 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' :
      TensorProduct.{u, w, u_1} R (↥(AlgHom.range (φ R s'))) M)

Tactic:
simp only [p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]

Premises used: AlgHom.comp_toLinearMap, LinearMap.comp_apply, LinearMap.rTensor_comp