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
ι' : 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
nth_rw nth_rw₁ :
  HMul.hMul (α := Q.Ring) ((C : (a : S) → MvPolynomial ι' S) ((algebraMap R S : (a : R) → S) a) : MvPolynomial ι' S)
      (HMul.hMul (α := Q.Ring) ((C : (a : S) → Q.Ring) (v₂.prod fun (a : ι) ↦ HPow.hPow (P.val a)))
        (v₁.prod fun (x : ι') (x2 : ℕ) ↦ HPow.hPow (α := Q.Ring) (X x) x2)) =
    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))
⊢ 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))

Tactic:
nth_rw 2 [mul_comm]

Premises used: mul_comm
-- 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 ι
j : ι →₀ ℕ
a : R
⊢ Eq (α := MvPolynomial (ι' ⊕ ι) R)
    ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) ((monomial j : (a : R) → MvPolynomial ι R) a) :
      MvPolynomial (ι' ⊕ ι) R)
    ((monomial (Finsupp.mapDomain Sum.inr j) : (a : R) → MvPolynomial (ι' ⊕ ι) R) a : MvPolynomial (ι' ⊕ ι) R)

Tactic:
rename_monomial _ _ _

Premises used: MvPolynomial.rename_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 ι
j : ι →₀ ℕ
a : R
h : Eq (α := (g : ι →₀ ℕ) → ι' ⊕ ι →₀ ℕ) (Finsupp.sumElim 0) (Finsupp.mapDomain Sum.inr)
⊢ Eq (α := Generators.Ring (Q.comp P))
    ((Hom.toAlgHom (Q.toComp P) : (a : P.Ring) → (Q.comp P).Ring) ((monomial j : (a : R) → MvPolynomial ι R) a) :
      Generators.Ring (Q.comp P))
    ((monomial (Finsupp.sumElim 0 j) : (a : R) → MvPolynomial (ι' ⊕ ι) R) a : MvPolynomial (ι' ⊕ ι) R)

Tactic:
convert! rename_monomial _ _ _

Premises used: MvPolynomial.rename_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 ι
j : ι →₀ ℕ
a : R
h :
  ∀ (f : ι →₀ ℕ) (i₁ : ι'),
    Eq (α := ℕ) ((Finsupp.sumElim 0 f : (a : ι' ⊕ ι) → ℕ) (Sum.inl i₁) : ℕ)
      ((Finsupp.mapDomain Sum.inr f : (a : ι' ⊕ ι) → ℕ) (Sum.inl i₁) : ℕ)
h₁ :
  ∀ (f : ι →₀ ℕ) (i₂ : ι),
    Eq (α := ℕ) ((Finsupp.sumElim 0 f : (a : ι' ⊕ ι) → ℕ) (Sum.inr i₂) : ℕ)
      ((Finsupp.mapDomain Sum.inr f : (a : ι' ⊕ ι) → ℕ) (Sum.inr i₂) : ℕ)
⊢ Eq (α := (g : ι →₀ ℕ) → ι' ⊕ ι →₀ ℕ) (Finsupp.sumElim 0) (Finsupp.mapDomain Sum.inr)

Tactic:
ext f (i₁ | 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
ι' : 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 ι
j : ι →₀ ℕ
a : R
f : ι →₀ ℕ
i₁ : ι'
⊢ Eq (α := ℕ) ((Finsupp.sumElim 0 f : (a : ι' ⊕ ι) → ℕ) (Sum.inl i₁) : ℕ)
    ((Finsupp.mapDomain Sum.inr f : (a : ι' ⊕ ι) → ℕ) (Sum.inl i₁) : ℕ)

Tactic:
simp [Finsupp.mapDomain_notin_range, Finsupp.mapDomain_apply Sum.inr_injective]

Premises used: Sum.inr_injective, Finsupp.mapDomain_apply, Finsupp.mapDomain_notin_range
-- 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 ι
j : ι →₀ ℕ
a : R
f : ι →₀ ℕ
i₂ : ι
⊢ Eq (α := ℕ) ((Finsupp.sumElim 0 f : (a : ι' ⊕ ι) → ℕ) (Sum.inr i₂) : ℕ)
    ((Finsupp.mapDomain Sum.inr f : (a : ι' ⊕ ι) → ℕ) (Sum.inr i₂) : ℕ)

Tactic:
simp [Finsupp.mapDomain_notin_range, Finsupp.mapDomain_apply Sum.inr_injective]

Premises used: Sum.inr_injective, Finsupp.mapDomain_apply, Finsupp.mapDomain_notin_range
-- 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 ι
p : P.Ring
hf :
  ∀ (i : ι) (m : ι' →₀ ℕ),
    Eq.{v + 1} (α := S)
      (coeff m
        ((AlgHom.comp (B := Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.ofComp P)) (rename Sum.inr) :
            (a : MvPolynomial ι R) → Q.Ring)
          (X i)))
      (coeff m
        ((AlgHom.comp (IsScalarTower.toAlgHom R S Q.Ring) (IsScalarTower.toAlgHom R P.Ring S) :
            (a : MvPolynomial ι R) → Q.Ring)
          (X i)))
⊢ Eq (α := MvPolynomial ι R →ₐ[R] Q.Ring)
    (AlgHom.comp (B := Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.ofComp P)) (rename Sum.inr))
    (AlgHom.comp (IsScalarTower.toAlgHom R S Q.Ring) (IsScalarTower.toAlgHom R P.Ring 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
ι' : 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 ι
p : P.Ring
i : ι
m : ι' →₀ ℕ
⊢ Eq.{v + 1} (α := S)
    (coeff m
      ((AlgHom.comp (B := Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.ofComp P)) (rename Sum.inr) :
          (a : MvPolynomial ι R) → Q.Ring)
        (X i)))
    (coeff m
      ((AlgHom.comp (IsScalarTower.toAlgHom R S Q.Ring) (IsScalarTower.toAlgHom R P.Ring S) :
          (a : MvPolynomial ι R) → Q.Ring)
        (X i)))

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 ι
a : S
h :
  Eq (α := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ a)) :
      Q.Ring)
    ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
⊢ ∃ (a_1 : Generators.Ring (Q.comp P)),
    Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a_1 : Q.Ring)
      ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)

Tactic:
use MvPolynomial.rename Sum.inr (P.σ a)

Premises used: MvPolynomial.rename, Sum.inr, 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
ι' : 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 ι
a : S
h :
  Eq (α := Q.Ring)
    ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → Q.Ring) (P.σ a) : Q.Ring)
    ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
⊢ Eq (α := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ a)) :
      Q.Ring)
    ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)

Tactic:
simp only [Hom.toAlgHom, ofComp, Generators.comp, MvPolynomial.aeval_rename,
        Sum.elim_comp_inr]

Premises used: Sum.elim_comp_inr, Algebra.Generators.comp, Algebra.Generators.Hom.toAlgHom, Algebra.Generators.ofComp, 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_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 ι
a : S
h :
  Eq (α := Q.Ring)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S (MvPolynomial ι' S)) (aeval P.val) : (a : MvPolynomial ι R) → Q.Ring)
        (P.σ a) :
      Q.Ring)
    ((IsScalarTower.toAlgHom R S (MvPolynomial ι' S) : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
⊢ Eq (α := Q.Ring)
    ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → Q.Ring) (P.σ a) : Q.Ring)
    ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)

Tactic:
simp_rw [Function.comp_def, ← MvPolynomial.algebraMap_eq, ← IsScalarTower.toAlgHom_apply R,
        ← MvPolynomial.comp_aeval]

Premises used: MvPolynomial.comp_aeval, Function.comp_def, MvPolynomial.algebraMap_eq, IsScalarTower.toAlgHom_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
ι' : 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 ι
a : S
⊢ Eq (α := Q.Ring)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S (MvPolynomial ι' S)) (aeval P.val) : (a : MvPolynomial ι R) → Q.Ring)
        (P.σ a) :
      Q.Ring)
    ((IsScalarTower.toAlgHom R S (MvPolynomial ι' S) : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' 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_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 ι
p q : MvPolynomial ι' S
hp : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p
hq : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = q
add :
  ∀ (p : Generators.Ring (Q.comp P)),
    ∃ (a : Generators.Ring (Q.comp P)),
      (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a =
        HAdd.hAdd (α := MvPolynomial ι' S) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring) q
⊢ ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p + q

Tactic:
obtain ⟨p, rfl⟩ := hp

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
ι' : 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 ι
q : MvPolynomial ι' S
hq : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = q
p : Generators.Ring (Q.comp P)
add :
  ∀ (q : Generators.Ring (Q.comp P)),
    ∃ (a : Generators.Ring (Q.comp P)),
      (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a =
        HAdd.hAdd (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
          ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring)
          ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) q : Q.Ring)
⊢ ∃ (a : Generators.Ring (Q.comp P)),
    (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a =
      HAdd.hAdd (α := MvPolynomial ι' S) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring) q

Tactic:
obtain ⟨q, rfl⟩ := hq

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
ι' : 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 ι
p q : Generators.Ring (Q.comp P)
h :
  (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (p + q) =
    HAdd.hAdd (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring)
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) q : Q.Ring)
⊢ ∃ (a : Generators.Ring (Q.comp P)),
    (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a =
      HAdd.hAdd (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring)
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) q : Q.Ring)

Tactic:
use p + q
-- 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 ι
p q : Generators.Ring (Q.comp P)
⊢ (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (p + q) =
    HAdd.hAdd (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring)
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) q : Q.Ring)

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 ι
p : MvPolynomial ι' S
i : ι'
hp : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p
mul_X :
  ∀ (p : MvPolynomial (ι' ⊕ ι) R),
    ∃ (a : Generators.Ring (Q.comp P)),
      (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a =
        HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
          ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring) (X i)
⊢ ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p * X i

Tactic:
obtain ⟨(p : MvPolynomial (ι' ⊕ ι) R), rfl⟩ := hp

Premises used: Sum, MvPolynomial, 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
ι' : 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 ι
i : ι'
p : MvPolynomial (ι' ⊕ ι) R
h :
  (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (p * X (Sum.inl i)) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring) (X i)
⊢ ∃ (a : Generators.Ring (Q.comp P)),
    (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a =
      HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring) (X i)

Tactic:
use p * MvPolynomial.X (R := R) (Sum.inl i)

Premises used: MvPolynomial.X, Sum.inl
-- 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 ι
i : ι'
p : MvPolynomial (ι' ⊕ ι) R
⊢ (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (p * X (Sum.inl i)) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring) (X i)

Tactic:
simp [Algebra.Generators.ofComp, Algebra.Generators.Hom.toAlgHom]

Premises used: Algebra.Generators.Hom.toAlgHom, Algebra.Generators.ofComp
-- 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 ι
p : Q.Ring
C :
  ∀ (a : S),
    ∃ (a_1 : Generators.Ring (Q.comp P)),
      Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a_1 : Q.Ring)
        ((MvPolynomial.C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
add :
  ∀ (p q : MvPolynomial ι' S)
    (hp : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p)
    (hq : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = q),
    ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p + q
mul_X :
  ∀ (p : MvPolynomial ι' S) (i : ι')
    (hp : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p),
    ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p * X i
⊢ ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p

Tactic:
induction p using MvPolynomial.induction_on with
  | C a =>
      use MvPolynomial.rename Sum.inr (P.σ a)
      simp only [Hom.toAlgHom, ofComp, Generators.comp, MvPolynomial.aeval_rename,
        Sum.elim_comp_inr]
      simp_rw [Function.comp_def, ← MvPolynomial.algebraMap_eq, ← IsScalarTower.toAlgHom_apply R,
        ← MvPolynomial.comp_aeval]
      simp
  | add p q hp hq =>
      obtain ⟨p, rfl⟩ := hp
      obtain ⟨q, rfl⟩ := hq
      use p + q
      simp
  | mul_X p i hp =>
      obtain ⟨(p : MvPolynomial (ι' ⊕ ι) R), rfl⟩ := hp
      use p * MvPolynomial.X (R := R) (Sum.inl i)
      simp [Algebra.Generators.ofComp, Algebra.Generators.Hom.toAlgHom]

Premises used: Sum.elim_comp_inr, Algebra.Generators.comp, Algebra.Generators.Hom.toAlgHom, Sum, MvPolynomial.induction_on, MvPolynomial.comp_aeval, Algebra.Generators.ofComp, Function.comp_def, MvPolynomial.algebraMap_eq, MvPolynomial, MvPolynomial.aeval_rename, MvPolynomial.C, rfl, IsScalarTower.toAlgHom_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_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
P : Generators R T ι
i : ι
⊢ Eq.{u_7 + 1} (α := T) ((aeval (val (extendScalars S P)) : (a : MvPolynomial ι S) → T) (X i) : T)
    ((algebraMap T T : (a : T) → 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
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''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : Algebra R S'
inst_20 : IsScalarTower R R' S'
inst_21 : IsScalarTower R S S'
f : P.Hom P'
x : R
⊢ Eq (α := P'.toExtension.Ring)
    ((AlgHom.toRingHom f.toAlgHom : (a : P.toExtension.Ring) → P'.toExtension.Ring)
        ((algebraMap R P.toExtension.Ring : (a : R) → P.toExtension.Ring) x) :
      P'.toExtension.Ring)
    ((algebraMap R' P'.toExtension.Ring : (a : R') → P'.toExtension.Ring) ((algebraMap R R' : (a : R) → R') x) :
      P'.toExtension.Ring)

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' ι'
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
inst_19 : Algebra R S'
inst_20 : IsScalarTower R R' S'
inst_21 : IsScalarTower R S S'
f : P.Hom P'
x : P.toExtension.Ring
⊢ Eq.{u_2 + 1} (α := S')
    ((algebraMap P'.toExtension.Ring S' : (a : P'.toExtension.Ring) → S')
        ((AlgHom.toRingHom f.toAlgHom : (a : P.toExtension.Ring) → P'.toExtension.Ring) x : P'.toExtension.Ring) :
      S')
    ((algebraMap S S' : (a : S) → S') ((algebraMap P.toExtension.Ring S : (a : P.toExtension.Ring) → S) x : 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
P : Generators R S ι
toRingHom :
  ∀ (x : P.toExtension.Ring),
    Eq (α := P.toExtension.Ring)
      ((Extension.Hom.toRingHom (Hom.id P).toExtensionHom : (a : P.toExtension.Ring) → P.toExtension.Ring) x :
        P.toExtension.Ring)
      (((Extension.Hom.id P.toExtension).toRingHom : (a : P.toExtension.Ring) → P.toExtension.Ring) x :
        P.toExtension.Ring)
⊢ (Hom.id P).toExtensionHom = Extension.Hom.id P.toExtension

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 ι
x : P.toExtension.Ring
⊢ Eq (α := P.toExtension.Ring)
    ((Extension.Hom.toRingHom (Hom.id P).toExtensionHom : (a : P.toExtension.Ring) → P.toExtension.Ring) x :
      P.toExtension.Ring)
    (((Extension.Hom.id P.toExtension).toRingHom : (a : P.toExtension.Ring) → P.toExtension.Ring) x :
      P.toExtension.Ring)

Tactic:
simp