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 ι
this_1 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : Generators.Ring (Q.comp P)),
    (Function.support (M := S) fun (a : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)) ↦
        if a.1 = i then
          (aeval P.val : (a : MvPolynomial ι R) → S)
            ((monomial a.2 : (a : R) → MvPolynomial ι R)
                (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) a) x) :
              MvPolynomial ι R)
        else 0) ⊆
      (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x)) : Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))
p q : MvPolynomial (ι' ⊕ ι) R
hp :
  Eq.{v + 1} (α := S)
    (∑ᶠ (i_1 : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)),
      if i_1.1 = i then
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((monomial i_1.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i_1) p) :
            MvPolynomial ι R)
      else 0)
    (coeff i ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p))
hq :
  Eq.{v + 1} (α := S)
    (∑ᶠ (i_1 : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)),
      if i_1.1 = i then
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((monomial i_1.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i_1) q) :
            MvPolynomial ι R)
      else 0)
    (coeff i ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) q))
a :
  (Function.support (M := S) fun (i_1 : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)) ↦
      if i_1.1 = i then
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((monomial i_1.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i_1) q) :
            MvPolynomial ι R)
      else 0) ⊆
    (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding q.support) : Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))
⊢ Function.HasFiniteSupport (M := S) fun (i_1 : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)) ↦
    if i_1.1 = i then
      (aeval P.val : (a : MvPolynomial ι R) → S)
        ((monomial i_1.2 : (a : R) → MvPolynomial ι R)
            (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i_1) q) :
          MvPolynomial ι R)
    else 0

Tactic:
refine (((support q).map e).finite_toSet.subset ?_)

Premises used: Finset.map, Set.Finite.subset, MvPolynomial.support, Finset.finite_toSet
-- 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 ι
this_1 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : Generators.Ring (Q.comp P)),
    (Function.support (M := S) fun (a : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)) ↦
        if a.1 = i then
          (aeval P.val : (a : MvPolynomial ι R) → S)
            ((monomial a.2 : (a : R) → MvPolynomial ι R)
                (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) a) x) :
              MvPolynomial ι R)
        else 0) ⊆
      (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x)) : Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))
p q : MvPolynomial (ι' ⊕ ι) R
hp :
  Eq.{v + 1} (α := S)
    (∑ᶠ (i_1 : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)),
      if i_1.1 = i then
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((monomial i_1.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i_1) p) :
            MvPolynomial ι R)
      else 0)
    (coeff i ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p))
hq :
  Eq.{v + 1} (α := S)
    (∑ᶠ (i_1 : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)),
      if i_1.1 = i then
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((monomial i_1.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i_1) q) :
            MvPolynomial ι R)
      else 0)
    (coeff i ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) q))
⊢ (Function.support (M := S) fun (a : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)) ↦
      if a.1 = i then
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((monomial a.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) a) q) :
            MvPolynomial ι R)
      else 0) ⊆
    (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding q.support) : Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))

Tactic:
this 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 ι
this_1 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : Generators.Ring (Q.comp P)),
    (Function.support (M := S) fun (a : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)) ↦
        if a.1 = i then
          (aeval P.val : (a : MvPolynomial ι R) → S)
            ((monomial a.2 : (a : R) → MvPolynomial ι R)
                (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) a) x) :
              MvPolynomial ι R)
        else 0) ⊆
      (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x)) : Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))
p q : MvPolynomial (ι' ⊕ ι) R
hp :
  Eq.{v + 1} (α := S)
    (∑ᶠ (i_1 : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)),
      if i_1.1 = i then
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((monomial i_1.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i_1) p) :
            MvPolynomial ι R)
      else 0)
    (coeff i ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p))
hq :
  Eq.{v + 1} (α := S)
    (∑ᶠ (i_1 : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)),
      if i_1.1 = i then
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((monomial i_1.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i_1) q) :
            MvPolynomial ι R)
      else 0)
    (coeff i ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) q))
⊢ (Function.support (M := S) fun (i_1 : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)) ↦
      if i_1.1 = i then
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((monomial i_1.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i_1) q) :
            MvPolynomial ι R)
      else 0) ⊆
    (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding q.support) : Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))

Tactic:
convert! this 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
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 ι
x : ↥Q.ker
refine_1 : (n : ι' →₀ ℕ) → (r : S) → Generators.Ring (Q.comp P)
refine_2 :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P))
    (Finsupp.sum (↑x : Q.Ring) fun (n : ι' →₀ ℕ) (r : S) ↦
      HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R))
⊢ ↥(ker (Q.comp P))

Tactic:
refine ⟨x.1.sum fun n r ↦ ?_, ?_⟩
-- 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 ι
x : ↥Q.ker
n : ι' →₀ ℕ
r : S
refine_1 : ι → ι' ⊕ ι
refine_1₁ : ι' ⊕ ι →₀ ℕ
⊢ Generators.Ring (Q.comp P)

Tactic:
refine rename ?_ (P.σ r) * monomial ?_ 1

Premises used: MvPolynomial.monomial, MvPolynomial.rename, OfNat.ofNat, 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 ι
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 ι
x : ↥Q.ker
n : ι' →₀ ℕ
r : S
⊢ ι → ι' ⊕ ι

Tactic:
exacts [Sum.inr, n.mapDomain Sum.inl]

Premises used: Finsupp.mapDomain, Sum.inl, Sum.inr
-- 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 ι
x : ↥Q.ker
refine_2 :
  Eq.{u_7 + 1} (α := T)
    ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T)
        (Finsupp.sum (↑x : Q.Ring) fun (n : ι' →₀ ℕ) (r : S) ↦
          HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
            ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
            ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
              MvPolynomial (ι' ⊕ ι) R)) :
      T)
    (0 : T)
⊢ Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P))
    (Finsupp.sum (↑x : Q.Ring) fun (n : ι' →₀ ℕ) (r : S) ↦
      HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R))

Tactic:
simp only [ker_eq_ker_aeval_val, RingHom.mem_ker]

Premises used: RingHom.mem_ker, Algebra.Generators.ker_eq_ker_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 ι
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 ι
x : ↥Q.ker
rw :
  ((aeval Q.val : (a : MvPolynomial ι' S) → T)
      (∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring))) :
    T)
| (0 : T)

Tactic:
rw [← aeval_val_eq_zero x.2, ← x.1.support_sum_monomial_coeff]

Premises used: MvPolynomial.support_sum_monomial_coeff, Algebra.Generators.aeval_val_eq_zero, Subtype.val, Subtype.property
-- 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 ι
x : ↥Q.ker
refine_2 :
  Eq.{u_7 + 1} (α := T)
    ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T)
        (Finsupp.sum (↑x : Q.Ring) fun (n : ι' →₀ ℕ) (r : S) ↦
          HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
            ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
            ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
              MvPolynomial (ι' ⊕ ι) R)) :
      T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T)
        (∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring))) :
      T)
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T)
        (Finsupp.sum (↑x : Q.Ring) fun (n : ι' →₀ ℕ) (r : S) ↦
          HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
            ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
            ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
              MvPolynomial (ι' ⊕ ι) R)) :
      T)
    (0 : T)

Tactic:
conv_rhs => rw [← aeval_val_eq_zero x.2, ← x.1.support_sum_monomial_coeff]

Premises used: MvPolynomial.support_sum_monomial_coeff, Algebra.Generators.aeval_val_eq_zero, Subtype.val, Subtype.property
-- 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 ι
x : ↥Q.ker
refine_2 :
  Eq.{u_7 + 1} (α := T)
    (∑ x_1 ∈ (↑x : Q.Ring).support,
      HMul.hMul (α := T) (β := T)
        ((aeval fun (x : ι) ↦ (algebraMap S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
            (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) x_1)) :
          T)
        (x_1.prod fun (a : ι') (b : ℕ) ↦ Q.val a ^ b : T))
    (∑ x_1 ∈ support (↑x : Q.Ring),
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) (coeff x_1 (↑x : Q.Ring)) : T)
        (x_1.prod fun (a : ι') (b : ℕ) ↦ Q.val a ^ b : T))
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T)
        (Finsupp.sum (↑x : Q.Ring) fun (n : ι' →₀ ℕ) (r : S) ↦
          HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
            ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
            ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
              MvPolynomial (ι' ⊕ ι) R)) :
      T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T)
        (∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring))) :
      T)

Tactic:
simp only [Finsupp.sum, map_sum, map_mul, aeval_rename, Function.comp_def, comp_val,
      Sum.elim_inr, aeval_monomial, map_one, Finsupp.prod_mapDomain_index_inj Sum.inl_injective,
      Sum.elim_inl, one_mul]

Premises used: Sum.inl_injective, Finsupp.sum, Algebra.Generators.comp_val, Finsupp.prod_mapDomain_index_inj, map_sum, Sum.elim_inr, map_mul, Function.comp_def, map_one, Sum.elim_inl, MvPolynomial.aeval_rename, MvPolynomial.aeval_monomial, one_mul
-- 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 ι
x : ↥Q.ker
refine_2 :
  ∀ (v : ι' →₀ ℕ) (i : v ∈ support (↑x : Q.Ring)),
    Eq.{u_7 + 1} (α := T)
      ((aeval fun (x : ι) ↦ (algebraMap S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
          (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
        T)
      ((algebraMap S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
⊢ Eq.{u_7 + 1} (α := T)
    (∑ x_1 ∈ (↑x : Q.Ring).support,
      HMul.hMul (α := T) (β := T)
        ((aeval fun (x : ι) ↦ (algebraMap S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
            (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) x_1)) :
          T)
        (x_1.prod fun (a : ι') (b : ℕ) ↦ Q.val a ^ b : T))
    (∑ x_1 ∈ support (↑x : Q.Ring),
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) (coeff x_1 (↑x : Q.Ring)) : T)
        (x_1.prod fun (a : ι') (b : ℕ) ↦ Q.val a ^ b : T))

Tactic:
congr! with v 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 ι
x : ↥Q.ker
v : ι' →₀ ℕ
i : v ∈ support (↑x : Q.Ring)
refine_2 :
  Eq.{u_7 + 1} (α := T)
    ((aeval fun (x : ι) ↦ (IsScalarTower.toAlgHom R S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
refine_2₁ :
  Eq.{u_7 + 1} (α := T)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S T) (aeval P.val) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
refine_2₂ :
  Eq.{u_7 + 1} (α := T)
    ((IsScalarTower.toAlgHom R S T : (a : S) → T)
        ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) : S) :
      T)
    ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
refine_2₃ :
  Eq.{u_7 + 1} (α := T) ((IsScalarTower.toAlgHom R S T : (a : S) → T) (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v : S) : T)
    ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval fun (x : ι) ↦ (algebraMap S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((algebraMap S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)

Tactic:
simp_rw [← IsScalarTower.toAlgHom_apply R, ← comp_aeval, AlgHom.comp_apply, P.aeval_val_σ,
      coeff]

Premises used: AlgHom.comp_apply, MvPolynomial.coeff, Algebra.Generators.aeval_val_σ, MvPolynomial.comp_aeval, 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 ι
x : ↥Q.ker
rw : ∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring))
| (↑x : Q.Ring)

Tactic:
rw [← x.1.support_sum_monomial_coeff]

Premises used: MvPolynomial.support_sum_monomial_coeff, Subtype.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
ι' : 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 ι
x : ↥Q.ker
conv_rhs :
  Eq (α := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (↑(Q.kerCompPreimage P x) : (Q.comp P).Ring) : Q.Ring)
    (∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring)) :
      MvPolynomial ι' S)
⊢ (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (↑(Q.kerCompPreimage P x) : (Q.comp P).Ring) =
    (↑x : Q.Ring)

Tactic:
conv_rhs => rw [← x.1.support_sum_monomial_coeff]

Premises used: MvPolynomial.support_sum_monomial_coeff, Subtype.val