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_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)
    (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)
⊢ 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:
rw [← apply_ite, Finset.sum_ite_eq]

Premises used: apply_ite, Finset.sum_ite_eq
-- 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)
    (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)
⊢ 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)

Tactic:
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]

Premises used: MvPolynomial.mem_support_iff, ne_eq, Finset.mem_map_equiv, AddEquiv.coe_toEquiv_symm, ite_not, reduceIte, Finset.mem_filter, MvPolynomial.coeff_monomial, ite_and
-- 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₁ :
  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 = 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)
    (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)

Tactic:
split
-- 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} (ι' →₀ ℕ) (ι →₀ ℕ)
h : 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)

Tactic:
simp only [*, map_zero, ite_self]

Premises used: ite_self, map_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_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} (ι' →₀ ℕ) (ι →₀ ℕ)
h : ¬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)

Tactic:
congr
-- 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))
⊢ 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

Tactic:
(((support p).map e).finite_toSet.subset ?_)

Premises used: Function.HasFiniteSupport, Finset.map, Set.Finite.subset, MvPolynomial.support, Finset.finite_toSet
-- 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.support (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) ⊆
    (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding p.support) : Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))
⊢ 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

Tactic:
refine (((support p).map e).finite_toSet.subset ?_)

Premises used: Finset.map, Set.Finite.subset, MvPolynomial.support, Finset.finite_toSet
-- 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))
⊢ (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) p) :
            MvPolynomial ι R)
      else 0) ⊆
    (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding p.support) : Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))

Tactic:
this p
-- 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))
⊢ (Function.support (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) ⊆
    (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding p.support) : Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))

Tactic:
convert! this p
-- 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))
⊢ 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

Tactic:
(((support q).map e).finite_toSet.subset ?_)

Premises used: Function.HasFiniteSupport, Finset.map, Set.Finite.subset, MvPolynomial.support, Finset.finite_toSet