awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
have 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)
Tactic: rw [map_aeval, aeval_def, coe_eval₂Hom, ← IsScalarTower.algebraMap_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
⊢ 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)
have 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
Tactic: rw [map_aeval, aeval_def, coe_eval₂Hom, ← IsScalarTower.algebraMap_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ 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)
have 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
Tactic: rw [map_aeval, aeval_def, coe_eval₂Hom, ← IsScalarTower.algebraMap_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ 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)
have 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
Tactic: rw [map_aeval, aeval_def, coe_eval₂Hom, ← IsScalarTower.algebraMap_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ 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)
have 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
Tactic: rw [map_aeval, aeval_def, coe_eval₂Hom, ← IsScalarTower.algebraMap_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (hypothesis)
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
⊢ (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
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
| s
have rw : ((aeval Q.val : (a : MvPolynomial ι' S) → T) (Finsupp.sum (Q.σ s) AddMonoidAlgebra.single) : T)
Tactic: rw [← Q.aeval_val_σ s, ← (Q.σ s).sum_single]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
⊢ (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
have 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)
Tactic: conv_rhs => rw [← Q.aeval_val_σ s, ← (Q.σ s).sum_single]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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 ι
⊢ Generators T (T ⊗[R] S) ι
have 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)
Tactic: apply Generators.ofSurjective (fun x ↦ 1 ⊗ₜ[R] P.val x)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use a • MvPolynomial.map (algebraMap R T) X
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ 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)
have 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
Tactic: simp only [LinearMapClass.map_smul, X, aeval_map_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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
⊢ 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)
        ((C : (a : R) → MvPolynomial ι R) a) :
      T ⊗[R] S)
    (1 ⊗ₜ[R]
        (aeval fun (x : ι) ↦ P.val x : (a : MvPolynomial ι R) → S)
          ((C : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R) :
      T ⊗[R] S)
have 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)
        ((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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
⊢ 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)
have 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)
Tactic: rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
⊢ 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)
have 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)
Tactic: rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
⊢ 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)
have 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)
Tactic: rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
⊢ 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)
have C₄ : Eq (α := T ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul (β := S) a 1) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a)
Tactic: rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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)
⊢ 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)
have C₅ : Eq (α := T ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul (β := S) a 1) (1 ⊗ₜ[R] HSMul.hSMul (β := S) a 1)
Tactic: rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]