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_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)
have C : ∀ (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)
Tactic: 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]
Cleared hypotheses: y
-- 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
y : P.Ring
C :
  ∀ (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)
          ((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)
⊢ 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)
have add : ∀ (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: 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]
Cleared hypotheses: y
-- 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
y : P.Ring
C :
  ∀ (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)
          ((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)
add :
  ∀ (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)
⊢ 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)
have mul_X : ∀ (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: 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]
Cleared hypotheses: y
-- 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_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
⊢ 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
have 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)
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]
-- 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
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)
⊢ 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
have 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
Tactic: rw [this, P.aeval_val_σ, smul_tmul', smul_eq_mul, mul_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 : 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
⊢ 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
have h₁ : HSMul.hSMul (β := T ⊗[R] S) a (1 ⊗ₜ[R] b) = a ⊗ₜ[R] b
Tactic: rw [this, P.aeval_val_σ, smul_tmul', smul_eq_mul, mul_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 : 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
⊢ 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
have h₂ : Eq (α := T ⊗[R] S) (HSMul.hSMul (β := T) a 1 ⊗ₜ[R] b) (a ⊗ₜ[R] b)
Tactic: rw [this, P.aeval_val_σ, smul_tmul', smul_eq_mul, mul_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 : 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)
⊢ 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
have h₃ : Eq (α := T ⊗[R] S) ((a * 1) ⊗ₜ[R] b) (a ⊗ₜ[R] b)
Tactic: rw [this, P.aeval_val_σ, smul_tmul', smul_eq_mul, mul_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 : 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)
⊢ 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
have h₄ : Eq (α := T ⊗[R] S) (a ⊗ₜ[R] b) (a ⊗ₜ[R] b)
Tactic: rw [this, P.aeval_val_σ, smul_tmul', smul_eq_mul, mul_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 ι
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨a, ha⟩ := ex
Cleared hypotheses: ex
-- 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 ι
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨b, hb⟩ := ey
Cleared hypotheses: ey
-- 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 ι
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
⊢ ∃ (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
have 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
Tactic: use (a + b)
-- 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 ι
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
⊢ ((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
have h : HAdd.hAdd (α := T ⊗[R] S) (β := 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)
    (((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 :
      T ⊗[R] S) =
  x + y
Tactic: rw [map_add, ha, hb]
-- 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 ι
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 :
  HAdd.hAdd (α := T ⊗[R] S) (β := 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)
      (((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 :
        T ⊗[R] S) =
    x + y
⊢ ((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
have h₁ : HAdd.hAdd (β := T ⊗[R] S) x
    (((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 :
      T ⊗[R] S) =
  x + y
Tactic: rw [map_add, ha, hb]
-- 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 ι
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 :
  HAdd.hAdd (α := T ⊗[R] S) (β := 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)
      (((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 :
        T ⊗[R] S) =
    x + y
h₁ :
  HAdd.hAdd (β := T ⊗[R] S) x
      (((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 :
        T ⊗[R] S) =
    x + y
⊢ ((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
have h₂ : x + y = x + y
Tactic: rw [map_add, ha, hb]