awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
s : T
x : P.Ring
rw :
  Eq.{u_2 + 1} (α := T) ((aeval ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) : (a : MvPolynomial ι R) → T) x : T)
    ((eval₂Hom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S)) fun (i : ι) ↦
            (algebraMap S T : (a : S) → T) (P.val i) :
          (a : MvPolynomial ι R) → T)
        x :
      T)
rw₁ :
  eval₂ (algebraMap R T) ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) x =
    (eval₂Hom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S)) fun (i : ι) ↦
          (algebraMap S T : (a : S) → T) (P.val i) :
        (a : MvPolynomial ι R) → T)
      x
rw₂ :
  eval₂ (algebraMap R T) ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) x =
    eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap R S))
      (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) x
rw₃ :
  eval₂ (algebraMap R T) ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) x =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) x
rw₄ rw₅ :
  eval₂ (algebraMap R T) (fun (x : ι) ↦ (algebraMap S T : (a : S) → T) (P.val x)) x =
    eval₂ (algebraMap R T) (fun (i : ι) ↦ (algebraMap S T : (a : S) → T) (P.val i)) x
⊢ Eq.{u_2 + 1} (α := T) ((aeval ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) : (a : MvPolynomial ι R) → T) x : T)
    ((algebraMap S T : (a : S) → T) ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : T)

Tactic:
rw [map_aeval, aeval_def, coe_eval₂Hom, ← IsScalarTower.algebraMap_eq, Function.comp_def]

Premises used: MvPolynomial.map_aeval, MvPolynomial.aeval_def, MvPolynomial.coe_eval₂Hom, Function.comp_def, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
s : T
⊢ ∀ (x : P.Ring),
    Eq.{u_2 + 1} (α := T) ((aeval ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) : (a : MvPolynomial ι R) → T) x : T)
      ((algebraMap S T : (a : S) → T) ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : T)

Tactic:
have (x : P.Ring) : aeval (algebraMap S T ∘ P.val) x = algebraMap S T (aeval P.val x) := by
      rw [map_aeval, aeval_def, coe_eval₂Hom, ← IsScalarTower.algebraMap_eq, Function.comp_def]
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
s : T
this :
  ∀ (x : P.Ring),
    Eq.{u_2 + 1} (α := T) ((aeval ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) : (a : MvPolynomial ι R) → T) x : T)
      ((algebraMap S T : (a : S) → T) ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : T)
rw : ((aeval Q.val : (a : MvPolynomial ι' S) → T) (Finsupp.sum (Q.σ s) AddMonoidAlgebra.single) : T)
| s

Tactic:
rw [← Q.aeval_val_σ s, ← (Q.σ s).sum_single]

Premises used: Algebra.Generators.aeval_val_σ, AddMonoidAlgebra.sum_single, Algebra.Generators.σ
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
s : T
this :
  ∀ (x : P.Ring),
    Eq.{u_2 + 1} (α := T) ((aeval ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) : (a : MvPolynomial ι R) → T) x : T)
      ((algebraMap S T : (a : S) → T) ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : T)
conv_rhs :
  Eq.{u_2 + 1} (α := T)
    ((aeval (Sum.elim Q.val ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val)) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
        (Finsupp.sum (Q.σ s) fun (n : ι' →₀ ℕ) (r : S) ↦
          HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
            ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
            ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
              MvPolynomial (ι' ⊕ ι) R)) :
      T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T) (Finsupp.sum (Q.σ s) AddMonoidAlgebra.single) : T)
⊢ (aeval (Sum.elim Q.val ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val)) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
      (Finsupp.sum (Q.σ s) fun (n : ι' →₀ ℕ) (r : S) ↦
        HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
          ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R)) =
    s

Tactic:
conv_rhs => rw [← Q.aeval_val_σ s, ← (Q.σ s).sum_single]

Premises used: Algebra.Generators.aeval_val_σ, AddMonoidAlgebra.sum_single, Algebra.Generators.σ
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
s : T
this :
  ∀ (x : P.Ring),
    Eq.{u_2 + 1} (α := T) ((aeval ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) : (a : MvPolynomial ι R) → T) x : T)
      ((algebraMap S T : (a : S) → T) ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : T)
⊢ Eq.{u_2 + 1} (α := T)
    ((aeval (Sum.elim Q.val ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val)) : (a : MvPolynomial (ι' ⊕ ι) R) → T)
        (Finsupp.sum (Q.σ s) fun (n : ι' →₀ ℕ) (r : S) ↦
          HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
            ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
            ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
              MvPolynomial (ι' ⊕ ι) R)) :
      T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T) (Finsupp.sum (Q.σ s) AddMonoidAlgebra.single) : T)

Tactic:
simp only [map_finsuppSum, map_mul, aeval_rename, Sum.elim_comp_inr, this, aeval_val_σ,
      aeval_monomial, map_one, Finsupp.prod_mapDomain_index_inj Sum.inl_injective, Sum.elim_inl,
      one_mul, single_eq_monomial]

Premises used: Sum.elim_comp_inr, Sum.inl_injective, MvPolynomial.single_eq_monomial, Finsupp.prod_mapDomain_index_inj, Algebra.Generators.aeval_val_σ, map_mul, map_one, map_finsuppSum, Sum.elim_inl, MvPolynomial.aeval_rename, MvPolynomial.aeval_monomial, one_mul
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
P : Generators R T ι
s : T
⊢ (aeval P.val : (a : MvPolynomial ι S) → T)
      ((MvPolynomial.map (algebraMap R S) : (a : MvPolynomial ι R) → MvPolynomial ι S) (P.σ s) : MvPolynomial ι S) =
    s

Tactic:
simp [@aeval_def S, ← IsScalarTower.algebraMap_eq, ← @aeval_def R]

Premises used: MvPolynomial.aeval_def, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
apply :
  Function.Surjective (α := MvPolynomial ι T) (β := T ⊗[R] S)
    (⇑(aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
      (a : MvPolynomial ι T) → T ⊗[R] S)
⊢ Generators T (T ⊗[R] S) ι

Tactic:
apply Generators.ofSurjective (fun x ↦ 1 ⊗ₜ[R] P.val x)

Premises used: Algebra.Generators.ofSurjective, Algebra.Generators.val, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
⊢ ∃ (a : MvPolynomial ι T),
    Eq (α := T ⊗[R] S)
      (((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          a :
        T ⊗[R] S)
      (0 : T ⊗[R] S)

Tactic:
⟨0, map_zero _⟩

Premises used: map_zero, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
⊢ ∃ (a : MvPolynomial ι T),
    Eq (α := T ⊗[R] S)
      (((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          a :
        T ⊗[R] S)
      (0 : T ⊗[R] S)

Tactic:
exact ⟨0, map_zero _⟩
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
h :
  Eq (α := T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        (HSMul.hSMul (β := MvPolynomial ι T) a
          ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) X : MvPolynomial ι T)) :
      T ⊗[R] S)
    (a ⊗ₜ[R] b : T ⊗[R] S)
⊢ ∃ (a_1 : MvPolynomial ι T),
    Eq (α := T ⊗[R] S)
      (((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          a_1 :
        T ⊗[R] S)
      (a ⊗ₜ[R] b : T ⊗[R] S)

Tactic:
use a • MvPolynomial.map (algebraMap R T) X

Premises used: Algebra.algebraMap, MvPolynomial.map, DFunLike.coe
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
h :
  HSMul.hSMul (β := T ⊗[R] S) a
      (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
            (a : MvPolynomial ι R) → T ⊗[R] S)
          (P.σ b) :
        T ⊗[R] S) =
    a ⊗ₜ[R] b
⊢ Eq (α := T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        (HSMul.hSMul (β := MvPolynomial ι T) a
          ((MvPolynomial.map (algebraMap R T) : (a : MvPolynomial ι R) → MvPolynomial ι T) X : MvPolynomial ι T)) :
      T ⊗[R] S)
    (a ⊗ₜ[R] b : T ⊗[R] S)

Tactic:
simp only [LinearMapClass.map_smul, X, aeval_map_algebraMap]

Premises used: MvPolynomial.aeval_map_algebraMap, LinearMapClass.map_smul
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
a_1 : T
b : S
X : P.Ring := P.σ b
a : R
C :
  Eq (α := T ⊗[R] S) ((algebraMap R (T ⊗[R] S) : (a : R) → T ⊗[R] S) a : T ⊗[R] S)
    (1 ⊗ₜ[R]
        (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S)
          ((MvPolynomial.C : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R) :
      T ⊗[R] S)
C₁ :
  Eq (α := T ⊗[R] S) ((algebraMap R (T ⊗[R] S) : (a : R) → T ⊗[R] S) a : T ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : T ⊗[R] S)
C₂ :
  Eq (α := T ⊗[R] S) ((algebraMap R T : (a : R) → T) a ⊗ₜ[R] 1 : T ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : T ⊗[R] S)
C₃ :
  Eq (α := T ⊗[R] S) (HSMul.hSMul (β := T) a 1 ⊗ₜ[R] 1 : T ⊗[R] S) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : T ⊗[R] S)
C₄ : Eq (α := T ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul (β := S) a 1) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a)
C₅ C₆ : Eq (α := T ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul (β := S) a 1) (1 ⊗ₜ[R] HSMul.hSMul (β := S) a 1)
⊢ Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        ((MvPolynomial.C : (a : R) → MvPolynomial ι R) a) :
      T ⊗[R] S)
    (1 ⊗ₜ[R]
        (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S)
          ((MvPolynomial.C : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R) :
      T ⊗[R] S)

Tactic:
rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]

Premises used: TensorProduct.smul_tmul, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_eq_smul_one, MvPolynomial.aeval_C
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
p q : MvPolynomial ι R
hp :
  Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        p :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) p : T ⊗[R] S)
hq :
  Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        q :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) q : T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (p + q) :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) (p + q) : T ⊗[R] S)

Tactic:
simp [map_add, tmul_add, hp, hq]

Premises used: map_add, TensorProduct.tmul_add
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
p : MvPolynomial ι R
i : ι
hp :
  Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        p :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) p : T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S)
    (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (p * MvPolynomial.X i) :
      T ⊗[R] S)
    (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) (p * MvPolynomial.X i) : T ⊗[R] S)

Tactic:
simp [hp]
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
⊢ ∀ (y : P.Ring),
    Eq (α := T ⊗[R] S)
      (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
            (a : MvPolynomial ι R) → T ⊗[R] S)
          y :
        T ⊗[R] S)
      (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) y : T ⊗[R] S)

Tactic:
have : ∀ y : P.Ring,
      aeval (fun x ↦ (1 ⊗ₜ[R] P.val x : T ⊗[R] S)) y = 1 ⊗ₜ aeval (fun x ↦ P.val x) y := by
      intro y
      induction y using MvPolynomial.induction_on with
      | C a =>
        rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]
      | add p q hp hq => simp [map_add, tmul_add, hp, hq]
      | mul_X p i hp => simp [hp]
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
a : T
b : S
X : P.Ring := P.σ b
this :
  ∀ (y : P.Ring),
    Eq (α := T ⊗[R] S)
      (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
            (a : MvPolynomial ι R) → T ⊗[R] S)
          y :
        T ⊗[R] S)
      (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) y : T ⊗[R] S)
h :
  HSMul.hSMul (β := T ⊗[R] S) a
      (1 ⊗ₜ[R] (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S) (P.σ b) : T ⊗[R] S) =
    a ⊗ₜ[R] b
h₁ : HSMul.hSMul (β := T ⊗[R] S) a (1 ⊗ₜ[R] b) = a ⊗ₜ[R] b
h₂ : Eq (α := T ⊗[R] S) (HSMul.hSMul (β := T) a 1 ⊗ₜ[R] b) (a ⊗ₜ[R] b)
h₃ : Eq (α := T ⊗[R] S) ((a * 1) ⊗ₜ[R] b) (a ⊗ₜ[R] b)
h₄ h₅ : Eq (α := T ⊗[R] S) (a ⊗ₜ[R] b) (a ⊗ₜ[R] b)
⊢ HSMul.hSMul (β := T ⊗[R] S) a
      (((aeval (R := R) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι R →ₐ[R] T ⊗[R] S) :
            (a : MvPolynomial ι R) → T ⊗[R] S)
          (P.σ b) :
        T ⊗[R] S) =
    a ⊗ₜ[R] b

Tactic:
rw [this, P.aeval_val_σ, smul_tmul', smul_eq_mul, mul_one]

Premises used: Algebra.Generators.aeval_val_σ, TensorProduct.smul_tmul', smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
x y : T ⊗[R] S
ex :
  ∃ (a : MvPolynomial ι T),
    ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        a =
      x
ey :
  ∃ (a : MvPolynomial ι T),
    ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        a =
      y
add :
  ∀ (a : MvPolynomial ι T)
    (ha :
      ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          a =
        x),
    ∃ (a : MvPolynomial ι T),
      ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          a =
        x + y
⊢ ∃ (a : MvPolynomial ι T),
    ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        a =
      x + y

Tactic:
obtain ⟨a, ha⟩ := ex
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
x y : T ⊗[R] S
ey :
  ∃ (a : MvPolynomial ι T),
    ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        a =
      y
a : MvPolynomial ι T
ha :
  ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
        (a : MvPolynomial ι T) → T ⊗[R] S)
      a =
    x
add :
  ∀ (b : MvPolynomial ι T)
    (hb :
      ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          b =
        y),
    ∃ (a : MvPolynomial ι T),
      ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          a =
        x + y
⊢ ∃ (a : MvPolynomial ι T),
    ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        a =
      x + y

Tactic:
obtain ⟨b, hb⟩ := ey
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
x y : T ⊗[R] S
a : MvPolynomial ι T
ha :
  ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
        (a : MvPolynomial ι T) → T ⊗[R] S)
      a =
    x
b : MvPolynomial ι T
hb :
  ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
        (a : MvPolynomial ι T) → T ⊗[R] S)
      b =
    y
h :
  ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
        (a : MvPolynomial ι T) → T ⊗[R] S)
      (a + b) =
    x + y
⊢ ∃ (a : MvPolynomial ι T),
    ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        a =
      x + y

Tactic:
use (a + b)

Premises used: HAdd.hAdd