-- 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₁ :
  if v.1 = i then
    Eq.{v + 1} (α := S)
      (∑
          x ∈
            Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding
              (support (R := R)
                ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
                  a)) with
          x.1 = i,
          if v = x then
            (aeval P.val : (a : MvPolynomial ι R) → S)
              ((monomial x.2 : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)
          else 0 :
        S)
      ((aeval P.val : (a : MvPolynomial ι R) → S) ((monomial v.2 : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R) :
        S)
  else
    Eq.{v + 1} (α := S)
      (∑
        x ∈
          Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding
            (support (R := R)
              ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
                a)) with
        x.1 = i,
        if v = x then
          (aeval P.val : (a : MvPolynomial ι R) → S) ((monomial x.2 : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)
        else 0)
      0
a₂ :
  Eq.{v + 1} (α := S)
    (if
          v ∈
            {a ∈
                Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding
                  (support (R := R)
                    ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) v) :
                        (a : R) → MvPolynomial (ι' ⊕ ι) R)
                      a)) |
              a.1 = i} then
        (aeval P.val : (a : MvPolynomial ι R) → S) ((monomial v.2 : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)
      else 0 :
      S)
    (if v.1 = i then
        (aeval P.val : (a : MvPolynomial ι R) → S) ((monomial v.2 : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)
      else 0 :
      S)
a₃ :
  Eq.{v + 1} (α := S)
    (if a = 0 then 0
      else
        if v.1 = i then
          (aeval P.val : (a : MvPolynomial ι R) → S) ((monomial v.2 : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)
        else 0 :
      S)
    (if v.1 = i then
        (aeval P.val : (a : MvPolynomial ι R) → S) ((monomial v.2 : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)
      else 0 :
      S)
a₄ :
  a = 0 →
    Eq.{v + 1} (α := S) (0 : S)
      (if v.1 = i then
          (aeval P.val : (a : MvPolynomial ι R) → S) ((monomial v.2 : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)
        else 0 :
        S)
a₅ a₆ :
  ¬a = 0 →
    Eq.{v + 1} (α := S)
      (if v.1 = i then
          (aeval P.val : (a : MvPolynomial ι R) → S) ((monomial v.2 : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)
        else 0 :
        S)
      (if v.1 = i then
          (aeval P.val : (a : MvPolynomial ι R) → S) ((monomial v.2 : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)
        else 0 :
        S)
⊢ 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))))

Tactic:
classical
        simp only [coeff_monomial, ← e.injective.eq_iff,
          map_zero, AddEquiv.apply_symm_apply, apply_ite]
        rw [← apply_ite, Finset.sum_ite_eq]
        simp only [Finset.mem_filter, Finset.mem_map_equiv, AddEquiv.coe_toEquiv_symm,
          mem_support_iff, coeff_monomial, ↓reduceIte, ne_eq, ite_and, ite_not]
        split
        · simp only [*, map_zero, ite_self]
        · congr

Premises used: MvPolynomial.mem_support_iff, ite_self, Function.Injective.eq_iff, apply_ite, map_zero, ne_eq, AddEquiv.apply_symm_apply, Finset.mem_map_equiv, AddEquiv.coe_toEquiv_symm, AddEquiv.injective, ite_not, reduceIte, Finset.mem_filter, MvPolynomial.coeff_monomial, ite_and, Finset.sum_ite_eq