awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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 (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))
have 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)))
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)) ∈ _
-- 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 : 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)))
⊢ 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))
have 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))))
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)) ∈ _
-- 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 : 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))
⊢ ∑ 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)))
have 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)))
Tactic: rw [map_sum, Finset.mul_sum]
-- 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 : 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)))
have 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))
Tactic: refine Finset.sum_congr rfl fun j hj ↦ ?_
-- 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 : 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}
⊢ (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))
have 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))
Tactic: obtain rfl := (Finset.mem_filter.mp hj).2
Cleared hypotheses: i, hi, hj
-- 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 : 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}
⊢ (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))
have 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))
Tactic: obtain ⟨i, j⟩ := j
Cleared hypotheses: j, hi, hj
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (hypothesis)
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 : ι →₀ ℕ
⊢ (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))
have 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)
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 ..
-- 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 (ι' →₀ ℕ)
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)
⊢ (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))
have 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)
Tactic: simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
          this]
-- 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 (ι' →₀ ℕ)
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)
⊢ (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)
have h : Eq (α := MvPolynomial (ι' ⊕ ι) R)
  ((monomial ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) : (a : R) → MvPolynomial (ι' ⊕ ι) R)
      (coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
    MvPolynomial (ι' ⊕ ι) R)
  ((monomial
          (HAdd.hAdd (α := ι' ⊕ ι →₀ ℕ) (β := ι' ⊕ ι →₀ ℕ)
            ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, 0) : ι' ⊕ ι →₀ ℕ)
            ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (0, j) : ι' ⊕ ι →₀ ℕ)) :
        (a : R) → MvPolynomial (ι' ⊕ ι) R)
      (1 * coeff ((e.symm : (a : (ι' →₀ ℕ) × (ι →₀ ℕ)) → ι' ⊕ ι →₀ ℕ) (i, j)) x) :
    MvPolynomial (ι' ⊕ ι) R)
Tactic: rw [monomial_mul, ← map_add, Prod.mk_add_mk, add_zero, zero_add, one_mul]