-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
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} (ι' →₀ ℕ) (ι →₀ ℕ)
⊢ 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))))
have 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
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