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
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 : h'.comp (AlgHom.rangeRestrict (φ R s)) = AlgHom.comp (AlgHom.rangeRestrict (φ R s')) (rename j)
⊢ 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)

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 : 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 :
  ∀ (n : Fin s.card),
    Eq.{w + 1} (α := T)
      (↑((h'.comp (AlgHom.rangeRestrict (φ R s)) : (a : MvPolynomial (Fin s.card) R) → ↥(φ R s').range) (X n)) : T)
      (↑(((AlgHom.comp (AlgHom.rangeRestrict (φ R s')) (rename j) :
                AlgHom.{u, u, w} R (MvPolynomial (Fin s.card) R) ↥(AlgHom.range (φ R s'))) :
              (a : MvPolynomial (Fin s.card) R) → ↥(φ R s').range)
            (X n)) :
        T)
⊢ h'.comp (AlgHom.rangeRestrict (φ R s)) = AlgHom.comp (AlgHom.rangeRestrict (φ R s')) (rename j)

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 : 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)
n : Fin s.card
hpq :
  Eq.{w + 1} (α := T) ((h : (a : S) → T) ((φ R s : (a : MvPolynomial (Fin s.card) R) → S) (X n) : S) : T)
    ((φ R s' : (a : MvPolynomial (Fin s'.card) R) → T)
        (X
            ((s'.equivFin : (a : ↥s') → Fin s'.card)
              (Subtype.mk (p := fun (x : T) ↦ x ∈ s')
                ((h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S)) ⋯)) :
          MvPolynomial (Fin s'.card) R) :
      T)
⊢ Eq.{w + 1} (α := T)
    (↑((h'.comp (AlgHom.rangeRestrict (φ R s)) : (a : MvPolynomial (Fin s.card) R) → ↥(φ R s').range) (X n)) : T)
    (↑(((AlgHom.comp (AlgHom.rangeRestrict (φ R s')) (rename j) :
              AlgHom.{u, u, w} R (MvPolynomial (Fin s.card) R) ↥(AlgHom.range (φ R s'))) :
            (a : MvPolynomial (Fin s.card) R) → ↥(φ R s').range)
          (X n)) :
      T)

Tactic:
simp only [AlgHom.coe_comp, Function.comp_apply, coe_codRestrict,
      Subalgebra.coe_val, rename_X, h', j]

Premises used: Subalgebra.coe_val, AlgHom.coe_comp, MvPolynomial.rename_X, Function.comp_apply, AlgHom.coe_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)
n : Fin s.card
⊢ Eq.{w + 1} (α := T) ((h : (a : S) → T) ((φ R s : (a : MvPolynomial (Fin s.card) R) → S) (X n) : S) : T)
    ((φ R s' : (a : MvPolynomial (Fin s'.card) R) → T)
        (X
            ((s'.equivFin : (a : ↥s') → Fin s'.card)
              (Subtype.mk (p := fun (x : T) ↦ x ∈ s')
                ((h : (a : S) → T) (↑((s.equivFin.symm : (a : Fin s.card) → ↥s) n) : S)) ⋯)) :
          MvPolynomial (Fin s'.card) R) :
      T)

Tactic:
simp only [φ, aeval_X, Equiv.symm_apply_apply]

Premises used: MvPolynomial.aeval_X, Equiv.symm_apply_apply, PolynomialLaw.φ
-- 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
h₁ :
  ∀ (t : S ⊗[R] M),
    Eq (α := T ⊗[R] N) (((⇑(rTensor N h.toLinearMap) : (a : S ⊗[R] N) → T ⊗[R] N) ∘ toFun S f) t)
      ((toFun T f ∘ (⇑(rTensor M h.toLinearMap) : (a : S ⊗[R] M) → T ⊗[R] M)) t)
⊢ Eq (α := S ⊗[R] M → T ⊗[R] N) ((⇑(rTensor N h.toLinearMap) : (a : S ⊗[R] N) → T ⊗[R] N) ∘ toFun S f)
    (toFun T f ∘ (⇑(rTensor M h.toLinearMap) : (a : S ⊗[R] M) → T ⊗[R] M))

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
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
⊢ Eq (α := T ⊗[R] N) (((⇑(rTensor N h.toLinearMap) : (a : S ⊗[R] N) → T ⊗[R] N) ∘ toFun S f) t)
    ((toFun T f ∘ (⇑(rTensor M h.toLinearMap) : (a : S ⊗[R] M) → T ⊗[R] M)) t)

Tactic:
simp only [Function.comp_apply, PolynomialLaw.isCompat_apply]

Premises used: Function.comp_apply, PolynomialLaw.isCompat_apply
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
h : ∀ (t : S ⊗[R] M), Eq (α := S ⊗[R] N) (toFun S 0 t) (0 t)
⊢ Eq (α := S ⊗[R] M → S ⊗[R] N) (toFun S 0) 0

Tactic:
ext t
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type u_5
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),
    Eq (α := S ⊗[R] N) (toFun S 0 t) (0 t)
⊢ Eq (α := S ⊗[R] N) (toFun S 0 t) (0 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_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type u_5
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
⊢ Eq (α := S ⊗[R] N) (toFun S 0 t) (0 t)

Tactic:
simp only [toFun_eq_rTensor_φ_toFun' _ ha, zero_def, Pi.zero_apply, _root_.map_zero]

Premises used: PolynomialLaw.toFun_eq_rTensor_φ_toFun', Pi.zero_apply, map_zero, PolynomialLaw.zero_def
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f g : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : 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),
    toFun S (f + g) t = toFun S f t + toFun S g t
⊢ toFun S (f + g) t = toFun S f t + toFun S g 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_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f g : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
h :
  ∀ (t : S ⊗[R] M),
    toFun S (f + g) t = HAdd.hAdd (α := S ⊗[R] M → S ⊗[R] N) (β := S ⊗[R] M → S ⊗[R] N) (toFun S f) (toFun S g) t
⊢ toFun S (f + g) = HAdd.hAdd (α := S ⊗[R] M → S ⊗[R] N) (toFun S f) (toFun S g)

Tactic:
ext t
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f g : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
t : S ⊗[R] M
⊢ toFun S (f + g) t = HAdd.hAdd (α := S ⊗[R] M → S ⊗[R] N) (β := S ⊗[R] M → S ⊗[R] N) (toFun S f) (toFun S g) t

Tactic:
simp only [Pi.add_apply, toFun_add_apply]

Premises used: PolynomialLaw.toFun_add_apply, Pi.add_apply
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_6
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_8
inst_5 : CommSemiring S
inst_6 : Algebra R S
h : ∀ (t : S ⊗[R] M), toFun S (-f) t = HSMul.hSMul (α := R) (β := S ⊗[R] M → S ⊗[R] N) (-1) (toFun S f) t
⊢ toFun S (-f) = HSMul.hSMul (α := R) (β := S ⊗[R] M → S ⊗[R] N) (-1) (toFun S f)

Tactic:
ext t
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_6
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_8
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),
    toFun S (-f) t = HSMul.hSMul (α := R) (β := S ⊗[R] M → S ⊗[R] N) (-1) (toFun S f) t
⊢ toFun S (-f) t = HSMul.hSMul (α := R) (β := S ⊗[R] M → S ⊗[R] N) (-1) (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 : CommRing R
M : Type u_6
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_8
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
⊢ toFun S (-f) t = HSMul.hSMul (α := R) (β := S ⊗[R] M → S ⊗[R] N) (-1) (toFun S f) t

Tactic:
simp only [toFun_eq_rTensor_φ_toFun' _ ha, neg_def, Pi.smul_apply, map_smul]

Premises used: PolynomialLaw.toFun_eq_rTensor_φ_toFun', PolynomialLaw.neg_def, map_smul, Pi.smul_apply
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
r : R
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
h : ∀ (t : S ⊗[R] M), toFun S (r • f) t = HSMul.hSMul (β := S ⊗[R] M → S ⊗[R] N) r (toFun S f) t
⊢ toFun S (r • f) = HSMul.hSMul (β := S ⊗[R] M → S ⊗[R] N) r (toFun S f)

Tactic:
ext t
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
r : R
f : M →ₚₗ[R] N
S : Type u_5
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),
    toFun S (r • f) t = HSMul.hSMul (β := S ⊗[R] M → S ⊗[R] N) r (toFun S f) t
⊢ toFun S (r • f) t = HSMul.hSMul (β := S ⊗[R] M → S ⊗[R] N) r (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_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
r : R
f : M →ₚₗ[R] N
S : Type u_5
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
⊢ toFun S (r • f) t = HSMul.hSMul (β := S ⊗[R] M → S ⊗[R] N) r (toFun S f) t

Tactic:
simp only [toFun_eq_rTensor_φ_toFun' _ ha, smul_def, Pi.smul_apply, map_smul]

Premises used: PolynomialLaw.toFun_eq_rTensor_φ_toFun', PolynomialLaw.smul_def, map_smul, Pi.smul_apply
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
simp :
  Eq (α := S ⊗[R] N)
    (1 ⊗ₜ[R]
      Function.comp (β := R ⊗[R] N) (⇑(TensorProduct.lid R N) : (a : R ⊗[R] N) → N)
        (toFun R f ∘ (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M)) x)
    (toFun S f (1 ⊗ₜ[R] x))
⊢ Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] f.ground x) (toFun S f (1 ⊗ₜ[R] x))

Tactic:
simp only [ground, toFun'_eq_toFun]

Premises used: PolynomialLaw.ground, PolynomialLaw.toFun'_eq_toFun
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
⊢ Eq (α := S ⊗[R] N)
    ((rTensor N (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (toFun R f (1 ⊗ₜ[R] x)) : S ⊗[R] N)
    (toFun S f ((rTensor M (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x)) : S ⊗[R] N)

Tactic:
f.isCompat_apply (Algebra.ofId R S) (1 ⊗ₜ[R] x)

Premises used: Algebra.ofId, TensorProduct.tmul, PolynomialLaw.isCompat_apply, OfNat.ofNat
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
h :
  Eq (α := S ⊗[R] N)
    (1 ⊗ₜ[R]
      Function.comp (β := R ⊗[R] N) (⇑(TensorProduct.lid R N) : (a : R ⊗[R] N) → N)
        (toFun R f ∘ (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M)) x)
    ((rTensor N (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (toFun R f (1 ⊗ₜ[R] x)))
h₁ :
  Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x) ((rTensor M (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x))
⊢ Eq (α := S ⊗[R] N)
    (1 ⊗ₜ[R]
      Function.comp (β := R ⊗[R] N) (⇑(TensorProduct.lid R N) : (a : R ⊗[R] N) → N)
        (toFun R f ∘ (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M)) x)
    (toFun S f (1 ⊗ₜ[R] x))

Tactic:
convert! f.isCompat_apply (Algebra.ofId R S) (1 ⊗ₜ[R] x)

Premises used: Algebra.ofId, TensorProduct.tmul, PolynomialLaw.isCompat_apply, OfNat.ofNat
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
h :
  Eq (α := S ⊗[R] N)
    ((rTensor N (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (toFun R f (1 ⊗ₜ[R] x)) : S ⊗[R] N)
    ((rTensor N (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (toFun R f (1 ⊗ₜ[R] x)) : S ⊗[R] N)
⊢ Eq (α := S ⊗[R] N)
    (1 ⊗ₜ[R]
      Function.comp (β := R ⊗[R] N) (⇑(TensorProduct.lid R N) : (a : R ⊗[R] N) → N)
        (toFun R f ∘ (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M)) x)
    ((rTensor N (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (toFun R f (1 ⊗ₜ[R] x)))

Tactic:
simp only [Function.comp_apply, TensorProduct.lid_symm_apply, TensorProduct.includeRight_lid]

Premises used: TensorProduct.lid_symm_apply, Function.comp_apply, TensorProduct.includeRight_lid
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
⊢ Eq (α := S ⊗[R] N)
    ((rTensor N (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (toFun R f (1 ⊗ₜ[R] x)) : S ⊗[R] N)
    ((rTensor N (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (toFun R f (1 ⊗ₜ[R] x)) : S ⊗[R] N)

Tactic:
congr
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
h : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((toLinearMap (Algebra.ofId R S) : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
h₁ : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((Algebra.ofId R S : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
h₂ h₃ : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x) (1 ⊗ₜ[R] x)
⊢ Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x) ((rTensor M (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x))

Tactic:
rw [rTensor_tmul, toLinearMap_apply, _root_.map_one]

Premises used: LinearMap.rTensor_tmul, AlgHom.toLinearMap_apply, map_one
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst_7 : CommSemiring S
inst_8 : Algebra R S
h : ∀ (t : S ⊗[R] M), toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t
⊢ Eq (α := S ⊗[R] M → S ⊗[R] P) (toFun S (g.comp f)) (toFun S g ∘ toFun S f)

Tactic:
ext t
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst_7 : CommSemiring S
inst_8 : 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),
    toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t
⊢ toFun S (g.comp f) t = (toFun S g ∘ 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_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst_7 : CommSemiring S
inst_8 : 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
⊢ π R N S
      (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] N) s
        (f.toFun' (MvPolynomial (Fin s.card) R) p)) =
    toFun S f t

Tactic:
simp only [toFun_eq_rTensor_φ_toFun' _ ha, π]

Premises used: PolynomialLaw.toFun_eq_rTensor_φ_toFun', PolynomialLaw.π