-- 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 :
  ∀ (v : ι' ⊕ ι →₀ ℕ) (a : R),
    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)))
a₁ :
  ∀ (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))),
    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 + q)) :
              MvPolynomial ι R)
        else 0)
      (coeff i ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (p + q)))
⊢ 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))

Tactic:
induction x using MvPolynomial.induction_on' with
      | monomial v a =>
        rw [finsum_eq_sum_of_support_subset _ (this _), ← Finset.sum_filter]
        obtain ⟨v, rfl⟩ := e.symm.surjective v
        -- Rewrite `e` in the right-hand side only.
        conv_rhs => simp only [e, Finsupp.sumFinsuppAddEquivProdFinsupp,
          Finsupp.sumFinsuppEquivProdFinsupp, AddEquiv.symm_mk, AddEquiv.coe_mk,
          Equiv.coe_fn_symm_mk, ofComp_toAlgHom_monomial_sumElim]
        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
      | add p q hp hq =>
        simp only [coeff_add, map_add, ite_add_zero]
        rw [finsum_add_distrib, hp, hq]
        · refine (((support p).map e).finite_toSet.subset ?_)
          convert! this p
        · refine (((support q).map e).finite_toSet.subset ?_)
          convert! this q

Premises used: MvPolynomial.mem_support_iff, Equiv.coe_fn_symm_mk, ite_self, ite_add_zero, MvPolynomial.monomial, Function.Injective.eq_iff, apply_ite, map_zero, map_add, ne_eq, AddEquiv.apply_symm_apply, Finset.mem_map_equiv, AddEquiv.coe_toEquiv_symm, finsum_eq_sum_of_support_subset, AddEquiv.injective, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, ite_not, MvPolynomial.coeff_add, reduceIte, Finset.mem_filter, MvPolynomial.coeff_monomial, Finsupp.sumFinsuppEquivProdFinsupp, AddEquiv.coe_mk, ite_and, Finset.sum_filter, finsum_add_distrib, AddEquiv.symm_mk, Finset.sum_ite_eq, rfl, Finsupp.sumFinsuppAddEquivProdFinsupp