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_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
h₂ h₃ : x + y = 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

Tactic:
rw [map_add, ha, hb]

Premises used: map_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 ι
x : T ⊗[R] S
zero :
  ∃ (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)
tmul :
  ∀ (a : T) (b : 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)
add :
  ∀ (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
⊢ ∃ (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

Tactic:
induction x using TensorProduct.induction_on with
  | zero => exact ⟨0, map_zero _⟩
  | tmul a b =>
    let X := P.σ b
    use a • MvPolynomial.map (algebraMap R T) X
    simp only [LinearMapClass.map_smul, X, aeval_map_algebraMap]
    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]
    rw [this, P.aeval_val_σ, smul_tmul', smul_eq_mul, mul_one]
  | add x y ex ey =>
    obtain ⟨a, ha⟩ := ex
    obtain ⟨b, hb⟩ := ey
    use (a + b)
    rw [map_add, ha, hb]

Premises used: MvPolynomial.X, map_add, Algebra.Generators.aeval_val_σ, MvPolynomial.aeval_map_algebraMap, TensorProduct.smul_tmul', LinearMapClass.map_smul, TensorProduct.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 : Generators R S ι
ι' : Type u_1
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
h :
  ∀ (i : ι),
    Eq (α := T ⊗[R] S)
      ((AlgHom.comp (B := T ⊗[R] P.Ring)
              (AlgHom.restrictScalars R
                (AlgHom.comp (B := Generators.Ring (S := T ⊗[R] S) (baseChange T P))
                  (IsScalarTower.toAlgHom T (Generators.Ring (S := T ⊗[R] S) (baseChange T P)) (T ⊗[R] S))
                  (↑(algebraTensorAlgEquiv R T) : T ⊗[R] MvPolynomial ι R →ₐ[T] MvPolynomial ι T)))
              TensorProduct.includeRight :
            (a : MvPolynomial ι R) → T ⊗[R] S)
          (X i) :
        T ⊗[R] S)
      ((AlgHom.comp (B := T ⊗[R] P.Ring)
              (AlgHom.restrictScalars R
                (AlgHom.comp (B := T ⊗[R] S) (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S))
                  (IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S))))
              TensorProduct.includeRight :
            (a : MvPolynomial ι R) → T ⊗[R] S)
          (X i) :
        T ⊗[R] S)
⊢ Eq (α := T ⊗[R] P.Ring →ₐ[T] T ⊗[R] S)
    (AlgHom.comp (B := Generators.Ring (S := T ⊗[R] S) (baseChange T P))
        (IsScalarTower.toAlgHom T (Generators.Ring (S := T ⊗[R] S) (baseChange T P)) (T ⊗[R] S))
        (↑(algebraTensorAlgEquiv R T) : T ⊗[R] MvPolynomial ι R →ₐ[T] MvPolynomial ι T) :
      T ⊗[R] P.Ring →ₐ[T] T ⊗[R] S)
    (AlgHom.comp (B := T ⊗[R] S) (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S))
        (IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S)) :
      T ⊗[R] P.Ring →ₐ[T] T ⊗[R] S)

Tactic:
ext
-- 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 : Generators R S ι
ι' : Type u_1
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
i : ι
⊢ Eq (α := T ⊗[R] S)
    ((AlgHom.comp (B := T ⊗[R] P.Ring)
            (AlgHom.restrictScalars R
              (AlgHom.comp (B := Generators.Ring (S := T ⊗[R] S) (baseChange T P))
                (IsScalarTower.toAlgHom T (Generators.Ring (S := T ⊗[R] S) (baseChange T P)) (T ⊗[R] S))
                (↑(algebraTensorAlgEquiv R T) : T ⊗[R] MvPolynomial ι R →ₐ[T] MvPolynomial ι T)))
            TensorProduct.includeRight :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (X i) :
      T ⊗[R] S)
    ((AlgHom.comp (B := T ⊗[R] P.Ring)
            (AlgHom.restrictScalars R
              (AlgHom.comp (B := T ⊗[R] S) (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S))
                (IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S))))
            TensorProduct.includeRight :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (X i) :
      T ⊗[R] S)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- 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 : Generators R S ι
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
x : Extension.Ring (R := T) (S := T ⊗[R] S) P.toExtension.baseChange
⊢ Eq (α := Generators.Ring (S := T ⊗[R] S) (baseChange T P))
    ((Extension.Hom.toRingHom (P.baseChangeFromBaseChange T) :
          (a : P.toExtension.baseChange.Ring) → (baseChange T P).Ring)
        x :
      Generators.Ring (S := T ⊗[R] S) (baseChange T P))
    ((algebraTensorAlgEquiv R T : (a : T ⊗[R] MvPolynomial ι R) → MvPolynomial ι T) x : MvPolynomial ι T)

Tactic:
rfl

Premises used: rfl
-- 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 : Generators R S ι
ι' : Type u_1
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
hf :
  ∀ (i : ι),
    Eq (α := T ⊗[R] S)
      ((AlgHom.comp (B := T ⊗[R] P.Ring) (IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S))
              (↑(AlgEquiv.symm (algebraTensorAlgEquiv R T)) : MvPolynomial ι T →ₐ[T] T ⊗[R] MvPolynomial ι R) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          (X i) :
        T ⊗[R] S)
      ((AlgHom.comp (B := T ⊗[R] S) (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S))
              (IsScalarTower.toAlgHom T (Generators.Ring (S := T ⊗[R] S) (baseChange T P)) (T ⊗[R] S)) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          (X i) :
        T ⊗[R] S)
⊢ Eq (α := Generators.Ring (S := T ⊗[R] S) (baseChange T P) →ₐ[T] T ⊗[R] S)
    (AlgHom.comp (B := T ⊗[R] P.Ring) (IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S))
      (↑(AlgEquiv.symm (algebraTensorAlgEquiv R T)) : MvPolynomial ι T →ₐ[T] T ⊗[R] MvPolynomial ι R))
    (AlgHom.comp (B := T ⊗[R] S) (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S))
      (IsScalarTower.toAlgHom T (Generators.Ring (S := T ⊗[R] S) (baseChange T P)) (T ⊗[R] S)))

Tactic:
ext
-- 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 : Generators R S ι
ι' : Type u_1
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
i : ι
⊢ Eq (α := T ⊗[R] S)
    ((AlgHom.comp (B := T ⊗[R] P.Ring) (IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S))
            (↑(AlgEquiv.symm (algebraTensorAlgEquiv R T)) : MvPolynomial ι T →ₐ[T] T ⊗[R] MvPolynomial ι R) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        (X i) :
      T ⊗[R] S)
    ((AlgHom.comp (B := T ⊗[R] S) (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S))
            (IsScalarTower.toAlgHom T (Generators.Ring (S := T ⊗[R] S) (baseChange T P)) (T ⊗[R] S)) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        (X i) :
      T ⊗[R] S)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- 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 : Generators R S ι
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
x : Extension.Ring (S := T ⊗[R] S) (toExtension (baseChange T P))
⊢ Eq (α := Extension.Ring (R := T) (S := T ⊗[R] S) P.toExtension.baseChange)
    ((Extension.Hom.toRingHom (P.baseChangeToBaseChange T) :
          (a : (baseChange T P).Ring) → P.toExtension.baseChange.Ring)
        x :
      Extension.Ring (R := T) (S := T ⊗[R] S) P.toExtension.baseChange)
    ((AlgEquiv.symm (algebraTensorAlgEquiv R T) : (a : MvPolynomial ι T) → T ⊗[R] MvPolynomial ι R) x :
      T ⊗[R] MvPolynomial ι R)

Tactic:
rfl

Premises used: rfl
-- 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.128304
inst_3 : CommRing T
inst_4 : Algebra R T
P : Generators R S ι
b : ι' → S
s : S
h :
  (aeval (Sum.elim P.val b) : (a : MvPolynomial (ι ⊕ ι') R) → S)
      ((rename Sum.inl : (a : MvPolynomial ι R) → MvPolynomial (ι ⊕ ι') R) (P.σ s) : MvPolynomial (ι ⊕ ι') R) =
    s
⊢ ∃ (a : MvPolynomial (ι ⊕ ι') R), (aeval (Sum.elim P.val b) : (a : MvPolynomial (ι ⊕ ι') R) → S) a = s

Tactic:
use rename Sum.inl (P.σ s)

Premises used: Sum.inl, MvPolynomial.rename, DFunLike.coe, 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.128304
inst_3 : CommRing T
inst_4 : Algebra R T
P : Generators R S ι
b : ι' → S
s : S
⊢ (aeval (Sum.elim P.val b) : (a : MvPolynomial (ι ⊕ ι') R) → S)
      ((rename Sum.inl : (a : MvPolynomial ι R) → MvPolynomial (ι ⊕ ι') R) (P.σ s) : MvPolynomial (ι ⊕ ι') R) =
    s

Tactic:
simp [aeval_rename]

Premises used: MvPolynomial.aeval_rename
-- 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
ι' : Type u_1
P : Generators R S ι
b : ι' → S
i : ι
⊢ (P.extend b).val (Sum.inl i) = P.val i

Tactic:
rfl

Premises used: rfl, Sum.elim
-- 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
ι' : Type u_1
P : Generators R S ι
b : ι' → S
i : ι'
⊢ (P.extend b).val (Sum.inr i) = b i

Tactic:
rfl

Premises used: rfl, Sum.elim
-- 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.130410
inst_3 : CommRing T
inst_4 : Algebra R T
P : Generators R S ι'
e : ι ≃ ι'
s : S
rw : ((aeval P.val : (a : MvPolynomial ι' R) → S) (P.σ s) : S)
| s

Tactic:
rw [← P.aeval_val_σ s]

Premises used: Algebra.Generators.aeval_val_σ
-- 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.130410
inst_3 : CommRing T
inst_4 : Algebra R T
P : Generators R S ι'
e : ι ≃ ι'
s : S
conv_rhs :
  Eq.{v + 1} (α := S)
    ((aeval (P.val ∘ (⇑e : (a : ι) → ι')) : (a : MvPolynomial ι R) → S)
        (((⇑(rename (⇑e.symm : (a : ι') → ι)) : (a : MvPolynomial ι' R) → MvPolynomial ι R) ∘ P.σ) s) :
      S)
    ((aeval P.val : (a : MvPolynomial ι' R) → S) (P.σ s) : S)
⊢ (aeval (P.val ∘ (⇑e : (a : ι) → ι')) : (a : MvPolynomial ι R) → S)
      (((⇑(rename (⇑e.symm : (a : ι') → ι)) : (a : MvPolynomial ι' R) → MvPolynomial ι R) ∘ P.σ) s) =
    s

Tactic:
conv_rhs => rw [← P.aeval_val_σ s]

Premises used: Algebra.Generators.aeval_val_σ
-- 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.130410
inst_3 : CommRing T
inst_4 : Algebra R T
P : Generators R S ι'
e : ι ≃ ι'
s : S
rw :
  Eq.{v + 1} (α := S)
    ((aeval P.val : (a : MvPolynomial ι' R) → S)
        ((rename (⇑e : (a : ι) → ι') : (a : MvPolynomial ι R) → MvPolynomial ι' R)
          (((⇑(rename (⇑e.symm : (a : ι') → ι)) : (a : MvPolynomial ι' R) → MvPolynomial ι R) ∘ P.σ) s)) :
      S)
    ((aeval P.val : (a : MvPolynomial ι' R) → S) (P.σ s) : S)
⊢ Eq.{v + 1} (α := S)
    ((aeval (P.val ∘ (⇑e : (a : ι) → ι')) : (a : MvPolynomial ι R) → S)
        (((⇑(rename (⇑e.symm : (a : ι') → ι)) : (a : MvPolynomial ι' R) → MvPolynomial ι R) ∘ P.σ) s) :
      S)
    ((aeval P.val : (a : MvPolynomial ι' R) → S) (P.σ s) : S)

Tactic:
rw [← MvPolynomial.aeval_rename]

Premises used: MvPolynomial.aeval_rename
-- 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.130410
inst_3 : CommRing T
inst_4 : Algebra R T
P : Generators R S ι'
e : ι ≃ ι'
s : S
⊢ Eq.{v + 1} (α := S)
    ((aeval P.val : (a : MvPolynomial ι' R) → S)
        ((rename (⇑e : (a : ι) → ι') : (a : MvPolynomial ι R) → MvPolynomial ι' R)
          (((⇑(rename (⇑e.symm : (a : ι') → ι)) : (a : MvPolynomial ι' R) → MvPolynomial ι R) ∘ P.σ) s)) :
      S)
    ((aeval P.val : (a : MvPolynomial ι' R) → S) (P.σ s) : S)

Tactic:
simp
-- 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
ι' : Type u_1
P : Generators R S ι'
e : ι ≃ ι'
⊢ (P.reindex e).val = P.val ∘ (⇑e : (a : ι) → ι')

Tactic:
rfl

Premises used: rfl
-- 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 : Generators R S ι
ι' : Type u_1
T : Type ?u.133356
inst_3 : CommRing T
inst_4 : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s_1 : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs_1 : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s_1 x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s x) = x
x : MvPolynomial σ R ⧸ I
rw :
  ((aeval
          (Function.comp (β := MvPolynomial σ R)
            (⇑(Ideal.Quotient.mkₐ R I) : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) X) :
        (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
      (s x) :
    MvPolynomial σ R ⧸ I)
| x

Tactic:
rw [← hs x, ← Ideal.Quotient.mkₐ_eq_mk R, aeval_unique (Ideal.Quotient.mkₐ _ I)]

Premises used: Ideal.Quotient.mkₐ_eq_mk, MvPolynomial.aeval_unique, Ideal.Quotient.mkₐ
-- 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 : Generators R S ι
ι' : Type u_1
T : Type ?u.133356
inst_3 : CommRing T
inst_4 : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s_1 : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs_1 : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s_1 x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s x) = x
x : MvPolynomial σ R ⧸ I
conv_rhs :
  Eq (α := MvPolynomial σ R ⧸ I)
    ((aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
        (s x) :
      MvPolynomial σ R ⧸ I)
    ((aeval
            (Function.comp (β := MvPolynomial σ R)
              (⇑(Ideal.Quotient.mkₐ R I) : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) X) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
        (s x) :
      MvPolynomial σ R ⧸ I)
⊢ (aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i) :
        (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
      (s x) =
    x

Tactic:
conv_rhs => rw [← hs x, ← Ideal.Quotient.mkₐ_eq_mk R, aeval_unique (Ideal.Quotient.mkₐ _ I)]

Premises used: Ideal.Quotient.mkₐ_eq_mk, MvPolynomial.aeval_unique, Ideal.Quotient.mkₐ
-- 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 : Generators R S ι
ι' : Type u_1
T : Type ?u.133356
inst_3 : CommRing T
inst_4 : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s_1 : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs_1 : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s_1 x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s x) = x
x : MvPolynomial σ R ⧸ I
⊢ Eq (α := MvPolynomial σ R ⧸ I)
    ((aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
        (s x) :
      MvPolynomial σ R ⧸ I)
    ((aeval
            (Function.comp (β := MvPolynomial σ R)
              (⇑(Ideal.Quotient.mkₐ R I) : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) X) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
        (s x) :
      MvPolynomial σ R ⧸ I)

Tactic:
simp [Function.comp_def]

Premises used: 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 : Generators R S ι
ι' : Type u_1
T : Type ?u.133356
inst_3 : CommRing T
inst_4 : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s_1 : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs_1 : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s_1 x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s x) = x
hC :
  ∀ (x : R),
    Eq (α := MvPolynomial σ R ⧸ I)
      ((RingHom.comp (β := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I)) C :
            (a : R) → MvPolynomial σ R ⧸ I)
          x :
        MvPolynomial σ R ⧸ I)
      ((RingHom.comp
              (↑(aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i)) :
                MvPolynomial σ R →+* MvPolynomial σ R ⧸ I)
              C :
            (a : R) → MvPolynomial σ R ⧸ I)
          x :
        MvPolynomial σ R ⧸ I)
hX :
  ∀ (x : σ),
    Eq (α := MvPolynomial σ R ⧸ I)
      ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I) : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X x) :
        MvPolynomial σ R ⧸ I)
      (((↑(aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i)) :
              MvPolynomial σ R →+* MvPolynomial σ R ⧸ I) :
            (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
          (X x) :
        MvPolynomial σ R ⧸ I)
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial σ R ⧸ I) (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I))
    (↑(aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i)) :
      MvPolynomial σ R →+* MvPolynomial σ R ⧸ I)

Tactic:
ext x
-- 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 : Generators R S ι
ι' : Type u_1
T : Type ?u.133356
inst_3 : CommRing T
inst_4 : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s_1 : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs_1 : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s_1 x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s x) = x
x : R
⊢ Eq (α := MvPolynomial σ R ⧸ I)
    ((RingHom.comp (β := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I)) C :
          (a : R) → MvPolynomial σ R ⧸ I)
        x :
      MvPolynomial σ R ⧸ I)
    ((RingHom.comp
            (↑(aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i)) :
              MvPolynomial σ R →+* MvPolynomial σ R ⧸ I)
            C :
          (a : R) → MvPolynomial σ R ⧸ I)
        x :
      MvPolynomial σ R ⧸ I)

Tactic:
simp [IsScalarTower.algebraMap_apply R (MvPolynomial σ R)]

Premises used: MvPolynomial, IsScalarTower.algebraMap_apply
-- 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 : Generators R S ι
ι' : Type u_1
T : Type ?u.133356
inst_3 : CommRing T
inst_4 : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s_1 : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs_1 : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s_1 x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s x) = x
x : σ
⊢ Eq (α := MvPolynomial σ R ⧸ I)
    ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I) : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X x) :
      MvPolynomial σ R ⧸ I)
    (((↑(aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i)) :
            MvPolynomial σ R →+* MvPolynomial σ R ⧸ I) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
        (X x) :
      MvPolynomial σ R ⧸ I)

Tactic:
simp [IsScalarTower.algebraMap_apply R (MvPolynomial σ R)]

Premises used: MvPolynomial, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
inst : CommRing R
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s x) = x
⊢ (naive s hs).σ = s

Tactic:
rfl

Premises used: rfl, Algebra.Generators.σ