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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x))
a :
  ∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i,
      (monomial j.2 : (a : R) → MvPolynomial ι R) (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x) ∈
    P.ker
⊢ Membership.mem (γ := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
      (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i,
        (monomial j.2 : (a : R) → MvPolynomial ι R) (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x)))

Tactic:
refine Ideal.mem_map_of_mem _ ?_

Premises used: Ideal.mem_map_of_mem
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x))
a :
  Eq.{v + 1} (α := S)
    (∑ x_1 ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with x_1.1 = i,
      (aeval P.val : (a : P.Ring) → S)
        ((monomial x_1.2 : (a : R) → MvPolynomial ι R)
            (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) x_1) x) :
          MvPolynomial ι R))
    0
⊢ ∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i,
      (monomial j.2 : (a : R) → MvPolynomial ι R) (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x) ∈
    P.ker

Tactic:
simp only [ker_eq_ker_aeval_val, AddEquiv.toEquiv_eq_coe, RingHom.mem_ker, map_sum]

Premises used: RingHom.mem_ker, map_sum, AddEquiv.toEquiv_eq_coe, 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
ι' : 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x))
a :
  Eq.{v + 1} (α := S)
    (∑ x_1 ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with x_1.1 = i,
      (aeval P.val : (a : P.Ring) → S)
        ((monomial x_1.2 : (a : R) → MvPolynomial ι R)
            (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) x_1) x) :
          MvPolynomial ι R))
    (coeff i ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x))
⊢ Eq.{v + 1} (α := S)
    (∑ x_1 ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with x_1.1 = i,
      (aeval P.val : (a : P.Ring) → S)
        ((monomial x_1.2 : (a : R) → MvPolynomial ι R)
            (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) x_1) x) :
          MvPolynomial ι R))
    0

Tactic:
rw [← coeff_zero i, ← h₂]

Premises used: MvPolynomial.coeff_zero
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x_1 : Generators.Ring (Q.comp P)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
x : Generators.Ring (Q.comp P)
rw :
  (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x)) : Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))ᶜ ⊆
    (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)ᶜ
⊢ (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 ((ι' →₀ ℕ) × (ι →₀ ℕ)))

Tactic:
rw [← Set.compl_subset_compl]

Premises used: Set.compl_subset_compl
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x_1 : Generators.Ring (Q.comp P)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
x : Generators.Ring (Q.comp P)
j : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)
obtain :
  ∀ (j : ι' ⊕ ι →₀ ℕ),
    Membership.mem (α := Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ))
        (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x)) :
            Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))ᶜ
        ((e : (a : ι' ⊕ ι →₀ ℕ) → (ι' →₀ ℕ) × (ι →₀ ℕ)) j : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)) →
      Membership.mem (α := Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)) (γ := Set (Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)))
        (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)ᶜ
        ((e : (a : ι' ⊕ ι →₀ ℕ) → (ι' →₀ ℕ) × (ι →₀ ℕ)) j : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ))
⊢ j ∈
      (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x)) :
          Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))ᶜ →
    Membership.mem (γ := Set (Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)))
      (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)ᶜ
      j

Tactic:
obtain ⟨j, rfl⟩ := e.surjective j

Premises used: AddEquiv.surjective, 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 ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x_1 : Generators.Ring (Q.comp P)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
x : Generators.Ring (Q.comp P)
j : ι' ⊕ ι →₀ ℕ
⊢ Membership.mem (α := Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ))
      (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x)) : Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))ᶜ
      ((e : (a : ι' ⊕ ι →₀ ℕ) → (ι' →₀ ℕ) × (ι →₀ ℕ)) j : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)) →
    Membership.mem (α := Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)) (γ := Set (Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)))
      (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)ᶜ
      ((e : (a : ι' ⊕ ι →₀ ℕ) → (ι' →₀ ℕ) × (ι →₀ ℕ)) j : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ))

Tactic:
simp_all
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
⊢ ∀ (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 ((ι' →₀ ℕ) × (ι →₀ ℕ)))

Tactic:
have (x : (Q.comp P).Ring) : (Function.support fun a ↦ if a.1 = i then aeval P.val
          (monomial a.2 (coeff (e.symm a) x)) else 0) ⊆ SetLike.coe ((support x).map e) := by
        rw [← Set.compl_subset_compl]
        intro j
        obtain ⟨j, rfl⟩ := e.surjective j
        simp_all
-- 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 (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
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 ((ι' →₀ ℕ) × (ι →₀ ℕ)))
a :
  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) x) :
            MvPolynomial ι R)
      else 0)
    (coeff i ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x))
⊢ Eq.{v + 1} (α := S)
    (∑ x_1 ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with x_1.1 = i,
      (aeval P.val : (a : P.Ring) → S)
        ((monomial x_1.2 : (a : R) → MvPolynomial ι R)
            (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) x_1) x) :
          MvPolynomial ι R))
    (coeff i ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x))

Tactic:
rw [Finset.sum_filter, ← finsum_eq_sum_of_support_subset _ (this x)]

Premises used: finsum_eq_sum_of_support_subset, Finset.sum_filter
-- 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 ((ι' →₀ ℕ) × (ι →₀ ℕ)))
v : ι' ⊕ ι →₀ ℕ
a : R
a₁ :
  Eq.{v + 1} (α := S)
    (∑
      a_1 ∈
        Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding
          (support (R := R) ((monomial v : (a : R) → MvPolynomial (ι' ⊕ ι) R) a)) with
      a_1.1 = i,
      (aeval P.val : (a : MvPolynomial ι R) → S)
        ((monomial a_1.2 : (a : R) → MvPolynomial ι R)
          (coeff (σ := ι' ⊕ ι) ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) a_1)
            ((monomial v : (a : R) → MvPolynomial (ι' ⊕ ι) R) a))))
    (coeff i
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((monomial v : (a : R) → MvPolynomial (ι' ⊕ ι) R) a)))
⊢ 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)
              ((monomial v : (a : R) → MvPolynomial (ι' ⊕ ι) R) a)))
      else 0)
    (coeff i
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((monomial v : (a : R) → MvPolynomial (ι' ⊕ ι) R) a)))

Tactic:
rw [finsum_eq_sum_of_support_subset _ (this _), ← Finset.sum_filter]

Premises used: finsum_eq_sum_of_support_subset, Finset.sum_filter
-- 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 ((ι' →₀ ℕ) × (ι →₀ ℕ)))
v : ι' ⊕ ι →₀ ℕ
a : R
a₁ :
  ∀ (v : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)),
    Eq.{v + 1} (α := S)
      (∑
        a_1 ∈
          Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding
            (support (R := R)
              ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
                a)) with
        a_1.1 = i,
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((monomial a_1.2 : (a : R) → MvPolynomial ι R)
            (coeff (σ := ι' ⊕ ι) ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) a_1)
              ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
                a))))
      (coeff i
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
          ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R) a)))
⊢ Eq.{v + 1} (α := S)
    (∑
      a_1 ∈
        Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding
          (support (R := R) ((monomial v : (a : R) → MvPolynomial (ι' ⊕ ι) R) a)) with
      a_1.1 = i,
      (aeval P.val : (a : MvPolynomial ι R) → S)
        ((monomial a_1.2 : (a : R) → MvPolynomial ι R)
          (coeff (σ := ι' ⊕ ι) ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) a_1)
            ((monomial v : (a : R) → MvPolynomial (ι' ⊕ ι) R) a))))
    (coeff i
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((monomial v : (a : R) → MvPolynomial (ι' ⊕ ι) R) a)))

Tactic:
obtain ⟨v, rfl⟩ := e.symm.surjective v

Premises used: AddEquiv.surjective, rfl, AddEquiv.symm
-- 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 ((ι' →₀ ℕ) × (ι →₀ ℕ)))
a : R
v : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)
simp :
  coeff i
    ((monomial v.1 : (a : S) → MvPolynomial ι' S)
      ((aeval P.val : (a : MvPolynomial ι R) → S) ((monomial v.2 : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)))
| coeff i
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
      ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R) a))

Tactic:
simp only [e, Finsupp.sumFinsuppAddEquivProdFinsupp,
          Finsupp.sumFinsuppEquivProdFinsupp, AddEquiv.symm_mk, AddEquiv.coe_mk,
          Equiv.coe_fn_symm_mk, ofComp_toAlgHom_monomial_sumElim]

Premises used: Equiv.coe_fn_symm_mk, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, Finsupp.sumFinsuppEquivProdFinsupp, AddEquiv.coe_mk, AddEquiv.symm_mk, Finsupp.sumFinsuppAddEquivProdFinsupp
-- 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 ((ι' →₀ ℕ) × (ι →₀ ℕ)))
a : R
v : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)
a₁ :
  Eq.{v + 1} (α := S)
    (∑
      a_1 ∈
        Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding
          (support (R := R)
            ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
              a)) with
      a_1.1 = i,
      (aeval P.val : (a : MvPolynomial ι R) → S)
        ((monomial a_1.2 : (a : R) → MvPolynomial ι R)
          (coeff (σ := ι' ⊕ ι) ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) a_1)
            ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
              a))))
    (coeff i
      ((monomial v.1 : (a : S) → MvPolynomial ι' S)
        ((aeval P.val : (a : MvPolynomial ι R) → S)
          ((monomial v.2 : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R))))
⊢ Eq.{v + 1} (α := S)
    (∑
      a_1 ∈
        Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding
          (support (R := R)
            ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
              a)) with
      a_1.1 = i,
      (aeval P.val : (a : MvPolynomial ι R) → S)
        ((monomial a_1.2 : (a : R) → MvPolynomial ι R)
          (coeff (σ := ι' ⊕ ι) ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) a_1)
            ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
              a))))
    (coeff i
      ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R) a)))

Tactic:
conv_rhs => simp only [e, Finsupp.sumFinsuppAddEquivProdFinsupp,
          Finsupp.sumFinsuppEquivProdFinsupp, AddEquiv.symm_mk, AddEquiv.coe_mk,
          Equiv.coe_fn_symm_mk, ofComp_toAlgHom_monomial_sumElim]

Premises used: Equiv.coe_fn_symm_mk, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, Finsupp.sumFinsuppEquivProdFinsupp, AddEquiv.coe_mk, AddEquiv.symm_mk, Finsupp.sumFinsuppAddEquivProdFinsupp