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 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : IsScalarTower R' R'' S''
inst_16 : IsScalarTower R' S' S''
inst_17 : IsScalarTower S S' S''
f : P'.Hom P''
g : P.Hom P'
x : ι
induction :
  ∀ (x : P'.Ring),
    Eq.{u_5 + 1} (α := S'')
      ((aeval P''.val : (a : MvPolynomial ι'' R'') → S'')
          ((aeval f.val : (a : MvPolynomial ι' R') → P''.Ring) x : P''.Ring) :
        S'')
      ((algebraMap S' S'' : (a : S') → S'') ((aeval P'.val : (a : MvPolynomial ι' R') → S') x : S') : S'')
⊢ Eq.{u_5 + 1} (α := S'')
    ((aeval P''.val : (a : MvPolynomial ι'' R'') → S'')
        ((aeval f.val : (a : MvPolynomial ι' R') → P''.Ring) (g.val x) : P''.Ring) :
      S'')
    ((algebraMap S' S'' : (a : S') → S'') ((aeval P'.val : (a : MvPolynomial ι' R') → S') (g.val x) : S') : S'')

Tactic:
induction g.val x using MvPolynomial.induction_on with
    | C r => simp [← IsScalarTower.algebraMap_apply]
    | add x y hx hy => simp only [map_add, hx, hy]
    | mul_X p i hp => simp only [map_mul, hp, aeval_X, aeval_val]

Premises used: MvPolynomial.aeval_X, Algebra.Generators.Hom.val, Algebra.Generators.Hom.aeval_val, map_add, MvPolynomial.induction_on, map_mul, MvPolynomial.C, 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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f : P.Hom P'
val : ∀ (x : ι) (m : ι' →₀ ℕ), coeff m (Hom.val (f.comp (Hom.id P)) x) = coeff m (f.val x)
⊢ f.comp (Hom.id P) = f

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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f : P.Hom P'
x : ι
m : ι' →₀ ℕ
⊢ coeff m (val (f.comp (Hom.id P)) x) = coeff m (f.val x)

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
P : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
inst_6 : Algebra S S'
f : P.Hom P'
val : ∀ (x : ι) (m : ι' →₀ ℕ), coeff m (Hom.val ((Hom.id P').comp f) x) = coeff m (f.val x)
⊢ (Hom.id P').comp f = f

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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
inst_6 : Algebra S S'
f : P.Hom P'
x : ι
m : ι' →₀ ℕ
⊢ coeff m (val ((Hom.id P').comp f) x) = coeff m (f.val x)

Tactic:
simp [Hom.id, aeval_X_left]

Premises used: MvPolynomial.aeval_X_left, Algebra.Generators.Hom.id
-- 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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R R''
inst_16 : IsScalarTower R R' R''
inst_17 : IsScalarTower R' R'' S''
inst_18 : IsScalarTower R' S' S''
inst_19 : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
r : R
⊢ Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) ((C : (a : R) → MvPolynomial ι R) r) : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring)
        ((f.toAlgHom : (a : P.Ring) → P'.Ring) ((C : (a : R) → MvPolynomial ι R) r)) :
      P''.Ring)

Tactic:
simp only [← MvPolynomial.algebraMap_eq, AlgHom.map_algebraMap]

Premises used: MvPolynomial.algebraMap_eq, AlgHom.map_algebraMap
-- 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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R R''
inst_16 : IsScalarTower R R' R''
inst_17 : IsScalarTower R' R'' S''
inst_18 : IsScalarTower R' S' S''
inst_19 : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x y : MvPolynomial ι R
hx :
  Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) x : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) x) : P''.Ring)
hy :
  Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) y : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) y) : P''.Ring)
⊢ Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) (x + y) : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) (x + y)) : P''.Ring)

Tactic:
simp only [map_add, hx, hy]

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 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R R''
inst_16 : IsScalarTower R R' R''
inst_17 : IsScalarTower R' R'' S''
inst_18 : IsScalarTower R' S' S''
inst_19 : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
p : MvPolynomial ι R
i : ι
hp :
  Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) p : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) p) : P''.Ring)
mul_X :
  HMul.hMul (α := P''.Ring) (β := P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) p) : P''.Ring)
      ((aeval g.val : (a : MvPolynomial ι' R') → P''.Ring) (f.val i) : P''.Ring) =
    HMul.hMul (α := P''.Ring) (β := P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) p) : P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring) (f.val i) : P''.Ring)
⊢ Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) (p * X i) : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) (p * X i)) : P''.Ring)

Tactic:
simp only [map_mul, hp, toAlgHom_X, comp_val]

Premises used: Algebra.Generators.Hom.toAlgHom_X, map_mul, Algebra.Generators.Hom.comp_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 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R R''
inst_16 : IsScalarTower R R' R''
inst_17 : IsScalarTower R' R'' S''
inst_18 : IsScalarTower R' S' S''
inst_19 : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
p : MvPolynomial ι R
i : ι
hp :
  Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) p : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) p) : P''.Ring)
⊢ HMul.hMul (α := P''.Ring) (β := P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) p) : P''.Ring)
      ((aeval g.val : (a : MvPolynomial ι' R') → P''.Ring) (f.val i) : P''.Ring) =
    HMul.hMul (α := P''.Ring) (β := P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) p) : P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring) (f.val i) : P''.Ring)

Tactic:
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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R R''
inst_16 : IsScalarTower R R' R''
inst_17 : IsScalarTower R' R'' S''
inst_18 : IsScalarTower R' S' S''
inst_19 : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x : P.Ring
C :
  ∀ (r : R),
    Eq (α := P''.Ring)
      ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) ((MvPolynomial.C : (a : R) → MvPolynomial ι R) r) : P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring)
          ((f.toAlgHom : (a : P.Ring) → P'.Ring) ((MvPolynomial.C : (a : R) → MvPolynomial ι R) r)) :
        P''.Ring)
add :
  ∀ (x y : MvPolynomial ι R)
    (hx :
      Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) x : P''.Ring)
        ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) x) : P''.Ring))
    (hy :
      Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) y : P''.Ring)
        ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) y) : P''.Ring)),
    Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) (x + y) : P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) (x + y)) : P''.Ring)
mul_X :
  ∀ (p : MvPolynomial ι R) (i : ι)
    (hp :
      Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) p : P''.Ring)
        ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) p) : P''.Ring)),
    Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) (p * X i) : P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) (p * X i)) : P''.Ring)
⊢ Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) x : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) x) : P''.Ring)

Tactic:
induction x using MvPolynomial.induction_on with
  | C r => simp only [← MvPolynomial.algebraMap_eq, AlgHom.map_algebraMap]
  | add x y hx hy => simp only [map_add, hx, hy]
  | mul_X p i hp => simp only [map_mul, hp, toAlgHom_X, comp_val]; rfl

Premises used: map_add, Algebra.Generators.Hom.toAlgHom_X, MvPolynomial.induction_on, map_mul, MvPolynomial.algebraMap_eq, Algebra.Generators.Hom.comp_val, AlgHom.map_algebraMap, MvPolynomial.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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
i : ι
⊢ Eq.{u_7 + 1} (α := T) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) (X (Sum.inr i)) : T)
    ((algebraMap S T : (a : S) → T) (P.val i) : T)

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_3
T : Type u_7
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 ι
⊢ Eq (α := P.Ring →ₐ[R] Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.toComp P)) (rename Sum.inr)

Tactic:
rfl

Premises used: MvPolynomial.X, MvPolynomial.rename, 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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
i : ι' ⊕ ι
inl :
  ∀ (val : ι'),
    Eq.{u_7 + 1} (α := T)
      ((aeval Q.val : (a : MvPolynomial ι' S) → T)
          (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) (Sum.inl val)) :
        T)
      ((algebraMap T T : (a : T) → T) (Generators.val (Q.comp P) (Sum.inl val)) : T)
inr :
  ∀ (val : ι),
    Eq.{u_7 + 1} (α := T)
      ((aeval Q.val : (a : MvPolynomial ι' S) → T)
          (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) (Sum.inr val)) :
        T)
      ((algebraMap T T : (a : T) → T) (Generators.val (Q.comp P) (Sum.inr val)) : T)
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) : T)
    ((algebraMap T T : (a : T) → T) (val (Q.comp P) i) : T)

Tactic:
cases i
-- 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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
val : ι'
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T)
        (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) (Sum.inl val)) :
      T)
    ((algebraMap T T : (a : T) → T) (Generators.val (Q.comp P) (Sum.inl val)) : T)

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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
val : ι
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T)
        (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) (Sum.inr val)) :
      T)
    ((algebraMap T T : (a : T) → T) (Generators.val (Q.comp P) (Sum.inr val)) : T)

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_3
T : Type u_7
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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
rw :
  HSMul.hSMul (β := Q.Ring) a
      ((v₁.sumElim v₂).prod fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦ Hom.val (P := Q.comp P) (Q.ofComp P) x1 ^ x2) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
            ((monomial v₂ : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)) :
        MvPolynomial ι' S)
      (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)
⊢ Eq (α := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((monomial (v₁.sumElim v₂) : (a : R) → MvPolynomial (ι' ⊕ ι) R) a) :
      Q.Ring)
    ((monomial v₁ : (a : S) → MvPolynomial ι' S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((monomial v₂ : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)) :
      MvPolynomial ι' S)

Tactic:
rw [Hom.toAlgHom_monomial, monomial_eq]

Premises used: MvPolynomial.monomial_eq, Algebra.Generators.Hom.toAlgHom_monomial
-- 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_3
T : Type u_7
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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
simp :
  HSMul.hSMul (β := Q.Ring) a
      ((v₁.sumElim v₂).prod fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
        HPow.hPow (α := Q.Ring) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) x1) x2) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
            (v₂.prod fun (i : ι) (k : ℕ) ↦ P.val i ^ k : S)) :
        MvPolynomial ι' S)
      (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)
⊢ HSMul.hSMul (β := Q.Ring) a
      ((v₁.sumElim v₂).prod fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦ Hom.val (P := Q.comp P) (Q.ofComp P) x1 ^ x2) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
            ((monomial v₂ : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)) :
        MvPolynomial ι' S)
      (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)

Tactic:
simp only [ofComp_val, aeval_monomial]

Premises used: Algebra.Generators.ofComp_val, MvPolynomial.aeval_monomial
-- 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_3
T : Type u_7
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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
rw :
  a •
      HMul.hMul (α := Q.Ring)
        (v₁.prod
          ((fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
              HPow.hPow (α := Q.Ring) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) x1) x2) ∘
            Sum.inl))
        (v₂.prod
          ((fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
              HPow.hPow (α := Q.Ring) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) x1) x2) ∘
            Sum.inr)) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
            (v₂.prod fun (i : ι) (k : ℕ) ↦ P.val i ^ k : S)) :
        MvPolynomial ι' S)
      (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)
⊢ HSMul.hSMul (β := Q.Ring) a
      ((v₁.sumElim v₂).prod fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
        HPow.hPow (α := Q.Ring) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) x1) x2) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
            (v₂.prod fun (i : ι) (k : ℕ) ↦ P.val i ^ k : S)) :
        MvPolynomial ι' S)
      (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)

Tactic:
rw [Finsupp.prod_sumElim]

Premises used: Finsupp.prod_sumElim
-- 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_3
T : Type u_7
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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
simp :
  HMul.hMul (α := Q.Ring) ((C : (a : S) → MvPolynomial ι' S) ((algebraMap R S : (a : R) → S) a) : MvPolynomial ι' S)
      (HMul.hMul (α := Q.Ring) (v₁.prod fun (x : ι') (x2 : ℕ) ↦ HPow.hPow (α := Q.Ring) (X x) x2)
        ((C : (a : S) → Q.Ring) (v₂.prod fun (a : ι) ↦ HPow.hPow (P.val a)))) =
    HMul.hMul (α := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S) ((algebraMap R S : (a : R) → S) a) : MvPolynomial ι' S)
      (HMul.hMul (α := MvPolynomial ι' S)
        ((C : (a : S) → MvPolynomial ι' S) (v₂.prod fun (i : ι) (k : ℕ) ↦ P.val i ^ k))
        (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e))
⊢ a •
      HMul.hMul (α := Q.Ring)
        (v₁.prod
          ((fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
              HPow.hPow (α := Q.Ring) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) x1) x2) ∘
            Sum.inl))
        (v₂.prod
          ((fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
              HPow.hPow (α := Q.Ring) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) x1) x2) ∘
            Sum.inr)) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
            (v₂.prod fun (i : ι) (k : ℕ) ↦ P.val i ^ k : S)) :
        MvPolynomial ι' S)
      (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)

Tactic:
simp only [Function.comp_def, Sum.elim_inl, Sum.elim_inr, ← map_pow, ← map_finsuppProd,
    C_mul, Algebra.smul_def, MvPolynomial.algebraMap_apply, mul_assoc]

Premises used: map_finsuppProd, mul_assoc, MvPolynomial.algebraMap_apply, map_pow, Sum.elim_inr, Function.comp_def, Sum.elim_inl, MvPolynomial.C_mul, Algebra.smul_def