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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
a :
  ∀ (i : ι' →₀ ℕ)
    (hi : i ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x))),
    Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
      (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
      (∑ i ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with i.1 = i,
        (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
          (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) x))
⊢ Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (∑ j ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x)),
      ∑ i ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with i.1 = j,
        (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
          (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) x))

Tactic:
refine sum_mem fun i hi ↦ ?_

Premises used: sum_mem
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x))
h :
  ∑ i ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with i.1 = i,
      (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) x) =
    HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R)
      ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1)
      ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
        (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i,
          (monomial j.2 : (a : R) → MvPolynomial ι R)
            (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x)))
a :
  Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R)
      ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1)
      ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
        (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i,
          (monomial j.2 : (a : R) → MvPolynomial ι R)
            (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x))))
⊢ Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (∑ i ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with i.1 = i,
      (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) x))

Tactic:
convert_to monomial (e.symm (i, 0)) 1 * (Q.toComp P).toAlgHom.toRingHom
      (∑ j ∈ (support x).map e.toEmbedding with j.1 = i, monomial j.2 (coeff (e.symm j) x)) ∈ _

Premises used: Algebra.Generators.toComp, Algebra.Generators.Hom.toAlgHom, MvPolynomial.monomial, Finset.map, Prod.mk, MvPolynomial.support, MvPolynomial.coeff, Equiv.toEmbedding, AlgHom.toRingHom, AddEquiv.toEquiv, OfNat.ofNat, Finset.filter, Eq, Prod.snd, DFunLike.coe, Finset.sum, AddEquiv.symm
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x))
h :
  Eq (α := MvPolynomial (ι' ⊕ ι) R)
    (∑ i ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with i.1 = i,
      (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) x))
    (∑ i_1 ∈ Finset.map e.toEmbedding (support x) with i_1.1 = i,
      HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
        ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
          MvPolynomial (ι' ⊕ ι) R)
        ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
            ((monomial i_1.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i_1) x)) :
          Generators.Ring (Q.comp P)))
⊢ ∑ i ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with i.1 = i,
      (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) x) =
    HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R)
      ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1)
      ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
        (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i,
          (monomial j.2 : (a : R) → MvPolynomial ι R)
            (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x)))

Tactic:
rw [map_sum, Finset.mul_sum]

Premises used: Finset.mul_sum, map_sum
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x))
⊢ Eq (α := MvPolynomial (ι' ⊕ ι) R)
    (∑ i ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with i.1 = i,
      (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) x))
    (∑ i_1 ∈ Finset.map e.toEmbedding (support x) with i_1.1 = i,
      HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
        ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
          MvPolynomial (ι' ⊕ ι) R)
        ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
            ((monomial i_1.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i_1) x)) :
          Generators.Ring (Q.comp P)))

Tactic:
Finset.sum_congr rfl fun j hj ↦ ?_

Premises used: Finset.sum_congr, rfl
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x))
h :
  ∀ (j : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)) (hj : j ∈ {j ∈ Finset.map e.toEmbedding (support x) | j.1 = i}),
    (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x) =
      HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
        ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
          MvPolynomial (ι' ⊕ ι) R)
        ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
            ((monomial j.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x)) :
          Generators.Ring (Q.comp P))
⊢ Eq (α := MvPolynomial (ι' ⊕ ι) R)
    (∑ i ∈ Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x) with i.1 = i,
      (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i) x))
    (∑ i_1 ∈ Finset.map e.toEmbedding (support x) with i_1.1 = i,
      HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
        ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
          MvPolynomial (ι' ⊕ ι) R)
        ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
            ((monomial i_1.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) i_1) x)) :
          Generators.Ring (Q.comp P)))

Tactic:
refine Finset.sum_congr rfl fun j hj ↦ ?_

Premises used: Finset.sum_congr, rfl
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x))
j : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)
hj : j ∈ {j ∈ Finset.map e.toEmbedding (support x) | j.1 = i}
h :
  ∀ (hi : j.1 ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x)))
    (hj : j ∈ {j_1 ∈ Finset.map e.toEmbedding (support x) | j_1.1 = j.1}),
    (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x) =
      HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
        ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (j.1, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
            1 :
          MvPolynomial (ι' ⊕ ι) R)
        ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
            ((monomial j.2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x)) :
          Generators.Ring (Q.comp P))
⊢ (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
      (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x) =
    HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
      ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
        MvPolynomial (ι' ⊕ ι) R)
      ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
          ((monomial j.2 : (a : R) → MvPolynomial ι R)
            (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x)) :
        Generators.Ring (Q.comp P))

Tactic:
obtain rfl := (Finset.mem_filter.mp hj).2

Premises used: And.right, Iff.mp, Finset.mem_filter, rfl
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
j : Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ)
hi : j.1 ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x))
hj : j ∈ {j_1 ∈ Finset.map e.toEmbedding (support x) | j_1.1 = j.1}
h :
  ∀ (i : ι' →₀ ℕ) (j : ι →₀ ℕ)
    (hi :
      (i, j).1 ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x)))
    (hj : (i, j) ∈ {j_1 ∈ Finset.map e.toEmbedding (support x) | j_1.1 = (i, j).1}),
    (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) =
      HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
        ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) ((i, j).1, 0)) :
              (a : R) → MvPolynomial (ι' ⊕ ι) R)
            1 :
          MvPolynomial (ι' ⊕ ι) R)
        ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
            ((monomial (i, j).2 : (a : R) → MvPolynomial ι R)
              (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x)) :
          Generators.Ring (Q.comp P))
⊢ (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
      (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x) =
    HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
      ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (j.1, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
        MvPolynomial (ι' ⊕ ι) R)
      ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
          ((monomial j.2 : (a : R) → MvPolynomial ι R)
            (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x)) :
        Generators.Ring (Q.comp P))

Tactic:
obtain ⟨i, j⟩ := j
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
j : ι →₀ ℕ
⊢ Eq (α := Generators.Ring (Q.comp P))
    ((Hom.toAlgHom (Q.toComp P) : (a : P.Ring) → (Q.comp P).Ring)
        ((monomial j : (a : R) → MvPolynomial ι R)
          (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x)) :
      Generators.Ring (Q.comp P))
    ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (0, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
      MvPolynomial (ι' ⊕ ι) R)

Tactic:
have : (Q.toComp P).toAlgHom (monomial j (coeff (e.symm (i, j)) x)) =
          monomial (e.symm (0, j)) (coeff (e.symm (i, j)) x) :=
        toComp_toAlgHom_monomial ..
-- 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)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
j : ι →₀ ℕ
this :
  Eq (α := Generators.Ring (Q.comp P))
    ((Hom.toAlgHom (Q.toComp P) : (a : P.Ring) → (Q.comp P).Ring)
        ((monomial j : (a : R) → MvPolynomial ι R)
          (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x)) :
      Generators.Ring (Q.comp P))
    ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (0, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
        (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
      MvPolynomial (ι' ⊕ ι) R)
h :
  (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
      (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) =
    HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
      ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
        MvPolynomial (ι' ⊕ ι) R)
      ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (0, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
          (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
        MvPolynomial (ι' ⊕ ι) R)
⊢ (monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
      (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) =
    HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
      ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) ((i, j).1, 0)) :
            (a : R) → MvPolynomial (ι' ⊕ ι) R)
          1 :
        MvPolynomial (ι' ⊕ ι) R)
      ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
          ((monomial (i, j).2 : (a : R) → MvPolynomial ι R)
            (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x)) :
        Generators.Ring (Q.comp P))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
          this]

Premises used: RingHom.coe_coe, AlgHom.toRingHom_eq_coe
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x))
a :
  Membership.mem (γ := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
      (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i,
        (monomial j.2 : (a : R) → MvPolynomial ι R) (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x)))
⊢ Membership.mem (γ := Ideal (Generators.Ring (Q.comp P)))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    (HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R)
      ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0)) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1)
      ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
        (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i,
          (monomial j.2 : (a : R) → MvPolynomial ι R)
            (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x))))

Tactic:
apply Ideal.mul_mem_left

Premises used: Ideal.mul_mem_left
-- 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 : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : Generators.Ring (Q.comp P)
h₂ : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
e : (ι' ⊕ ι →₀ ℕ) ≃+ Prod.{u_3, w} (ι' →₀ ℕ) (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding (support x))
⊢ Membership.mem (γ := Ideal (MvPolynomial (ι' ⊕ ι) R))
    (Ideal.map (F := P.Ring →+* Generators.Ring (Q.comp P)) (AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P))) P.ker)
    ((AlgHom.toRingHom (Hom.toAlgHom (Q.toComp P)) : (a : P.Ring) → (Q.comp P).Ring)
      (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i,
        (monomial j.2 : (a : R) → MvPolynomial ι R) (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) j) x)))

Tactic:
Ideal.mem_map_of_mem _ ?_

Premises used: Ideal.mem_map_of_mem, Set.Mem, setOf