-- 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.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) p) :
          MvPolynomial ι R)
    else 0
a₁ :
  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
⊢ ∑ᶠ (i_1 : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)),
      HAdd.hAdd (α := S) (β := S)
        (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 :
          S)
        (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 :
          S) =
    HAdd.hAdd (α := S) (coeff i ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p))
      (coeff i ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) q))

Tactic:
rw [finsum_add_distrib, hp, hq]

Premises used: finsum_add_distrib