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_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
have 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) q) :
          MvPolynomial ι R)
    else 0) ⊆
  (↑(Finset.map (↑e : (ι' ⊕ ι →₀ ℕ) ≃ (ι' →₀ ℕ) × (ι →₀ ℕ)).toEmbedding q.support) : Set ((ι' →₀ ℕ) × (ι →₀ ℕ)))
Tactic: refine (((support q).map e).finite_toSet.subset ?_)
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
⊢ ↥(ker (Q.comp P))
have refine_1 : (n : ι' →₀ ℕ) → (r : S) → Generators.Ring (Q.comp P)
Tactic: refine ⟨x.1.sum fun n r ↦ ?_, ?_⟩
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
refine_1 : (n : ι' →₀ ℕ) → (r : S) → Generators.Ring (Q.comp P)
⊢ ↥(ker (Q.comp P))
have refine_2 : Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P))
  (Finsupp.sum (↑x : Q.Ring) fun (n : ι' →₀ ℕ) (r : S) ↦
    HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
      ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R))
Tactic: refine ⟨x.1.sum fun n r ↦ ?_, ?_⟩
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
n : ι' →₀ ℕ
r : S
⊢ Generators.Ring (Q.comp P)
have refine_1 : ι → ι' ⊕ ι
Tactic: refine rename ?_ (P.σ r) * monomial ?_ 1
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
n : ι' →₀ ℕ
r : S
refine_1 : ι → ι' ⊕ ι
⊢ Generators.Ring (Q.comp P)
have refine_1₁ : ι' ⊕ ι →₀ ℕ
Tactic: refine rename ?_ (P.σ r) * monomial ?_ 1
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
⊢ Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P))
    (Finsupp.sum (↑x : Q.Ring) fun (n : ι' →₀ ℕ) (r : S) ↦
      HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
        ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R))
have refine_2 : Eq.{u_7 + 1} (α := T)
  ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T)
      (Finsupp.sum (↑x : Q.Ring) fun (n : ι' →₀ ℕ) (r : S) ↦
        HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
          ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R)) :
    T)
  (0 : T)
Tactic: simp only [ker_eq_ker_aeval_val, RingHom.mem_ker]
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
| (0 : T)
have rw : ((aeval Q.val : (a : MvPolynomial ι' S) → T)
    (∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring))) :
  T)
Tactic: rw [← aeval_val_eq_zero x.2, ← x.1.support_sum_monomial_coeff]
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T)
        (Finsupp.sum (↑x : Q.Ring) fun (n : ι' →₀ ℕ) (r : S) ↦
          HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
            ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
            ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
              MvPolynomial (ι' ⊕ ι) R)) :
      T)
    (0 : T)
have refine_2 : Eq.{u_7 + 1} (α := T)
  ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T)
      (Finsupp.sum (↑x : Q.Ring) fun (n : ι' →₀ ℕ) (r : S) ↦
        HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
          ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 : MvPolynomial (ι' ⊕ ι) R)) :
    T)
  ((aeval Q.val : (a : MvPolynomial ι' S) → T)
      (∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring))) :
    T)
Tactic: conv_rhs => rw [← aeval_val_eq_zero x.2, ← x.1.support_sum_monomial_coeff]
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval (val (Q.comp P)) : (a : (Q.comp P).Ring) → T)
        (Finsupp.sum (↑x : Q.Ring) fun (n : ι' →₀ ℕ) (r : S) ↦
          HMul.hMul (α := MvPolynomial (ι' ⊕ ι) R) (β := MvPolynomial (ι' ⊕ ι) R)
            ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ r) : MvPolynomial (ι' ⊕ ι) R)
            ((monomial (Finsupp.mapDomain Sum.inl n) : (a : R) → MvPolynomial (ι' ⊕ ι) R) 1 :
              MvPolynomial (ι' ⊕ ι) R)) :
      T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T)
        (∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring))) :
      T)
have refine_2 : Eq.{u_7 + 1} (α := T)
  (∑ x_1 ∈ (↑x : Q.Ring).support,
    HMul.hMul (α := T) (β := T)
      ((aeval fun (x : ι) ↦ (algebraMap S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
          (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) x_1)) :
        T)
      (x_1.prod fun (a : ι') (b : ℕ) ↦ Q.val a ^ b : T))
  (∑ x_1 ∈ support (↑x : Q.Ring),
    HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) (coeff x_1 (↑x : Q.Ring)) : T)
      (x_1.prod fun (a : ι') (b : ℕ) ↦ Q.val a ^ b : T))
Tactic: simp only [Finsupp.sum, map_sum, map_mul, aeval_rename, Function.comp_def, comp_val,
      Sum.elim_inr, aeval_monomial, map_one, Finsupp.prod_mapDomain_index_inj Sum.inl_injective,
      Sum.elim_inl, one_mul]
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
⊢ Eq.{u_7 + 1} (α := T)
    (∑ x_1 ∈ (↑x : Q.Ring).support,
      HMul.hMul (α := T) (β := T)
        ((aeval fun (x : ι) ↦ (algebraMap S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
            (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) x_1)) :
          T)
        (x_1.prod fun (a : ι') (b : ℕ) ↦ Q.val a ^ b : T))
    (∑ x_1 ∈ support (↑x : Q.Ring),
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) (coeff x_1 (↑x : Q.Ring)) : T)
        (x_1.prod fun (a : ι') (b : ℕ) ↦ Q.val a ^ b : T))
have refine_2 : ∀ (v : ι' →₀ ℕ) (i : v ∈ support (↑x : Q.Ring)),
  Eq.{u_7 + 1} (α := T)
    ((aeval fun (x : ι) ↦ (algebraMap S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((algebraMap S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
Tactic: congr! with v i
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
v : ι' →₀ ℕ
i : v ∈ support (↑x : Q.Ring)
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval fun (x : ι) ↦ (algebraMap S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((algebraMap S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
have refine_2 : Eq.{u_7 + 1} (α := T)
  ((aeval fun (x : ι) ↦ (IsScalarTower.toAlgHom R S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
      (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
    T)
  ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
Tactic: simp_rw [← IsScalarTower.toAlgHom_apply R, ← comp_aeval, AlgHom.comp_apply, P.aeval_val_σ,
      coeff]
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
v : ι' →₀ ℕ
i : v ∈ support (↑x : Q.Ring)
refine_2 :
  Eq.{u_7 + 1} (α := T)
    ((aeval fun (x : ι) ↦ (IsScalarTower.toAlgHom R S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval fun (x : ι) ↦ (algebraMap S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((algebraMap S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
have refine_2₁ : Eq.{u_7 + 1} (α := T)
  ((AlgHom.comp (IsScalarTower.toAlgHom R S T) (aeval P.val) : (a : MvPolynomial ι R) → T)
      (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
    T)
  ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
Tactic: simp_rw [← IsScalarTower.toAlgHom_apply R, ← comp_aeval, AlgHom.comp_apply, P.aeval_val_σ,
      coeff]
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
v : ι' →₀ ℕ
i : v ∈ support (↑x : Q.Ring)
refine_2 :
  Eq.{u_7 + 1} (α := T)
    ((aeval fun (x : ι) ↦ (IsScalarTower.toAlgHom R S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
refine_2₁ :
  Eq.{u_7 + 1} (α := T)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S T) (aeval P.val) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval fun (x : ι) ↦ (algebraMap S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((algebraMap S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
have refine_2₂ : Eq.{u_7 + 1} (α := T)
  ((IsScalarTower.toAlgHom R S T : (a : S) → T)
      ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) : S) :
    T)
  ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
Tactic: simp_rw [← IsScalarTower.toAlgHom_apply R, ← comp_aeval, AlgHom.comp_apply, P.aeval_val_σ,
      coeff]
-- 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
P_1 : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_7
inst_15 : CommRing T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : ↥Q.ker
v : ι' →₀ ℕ
i : v ∈ support (↑x : Q.Ring)
refine_2 :
  Eq.{u_7 + 1} (α := T)
    ((aeval fun (x : ι) ↦ (IsScalarTower.toAlgHom R S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
refine_2₁ :
  Eq.{u_7 + 1} (α := T)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S T) (aeval P.val) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
refine_2₂ :
  Eq.{u_7 + 1} (α := T)
    ((IsScalarTower.toAlgHom R S T : (a : S) → T)
        ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) : S) :
      T)
    ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval fun (x : ι) ↦ (algebraMap S T : (a : S) → T) (P.val x) : (a : MvPolynomial ι R) → T)
        (P.σ (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v)) :
      T)
    ((algebraMap S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
have refine_2₃ : Eq.{u_7 + 1} (α := T) ((IsScalarTower.toAlgHom R S T : (a : S) → T) (((↑x : Q.Ring) : (a : ι' →₀ ℕ) → S) v : S) : T)
  ((IsScalarTower.toAlgHom R S T : (a : S) → T) (coeff v (↑x : Q.Ring)) : T)
Tactic: simp_rw [← IsScalarTower.toAlgHom_apply R, ← comp_aeval, AlgHom.comp_apply, P.aeval_val_σ,
      coeff]
-- 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 ι
x : ↥Q.ker
| (↑x : Q.Ring)
have rw : ∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring))
Tactic: rw [← x.1.support_sum_monomial_coeff]
-- 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 ι
x : ↥Q.ker
⊢ (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (↑(Q.kerCompPreimage P x) : (Q.comp P).Ring) =
    (↑x : Q.Ring)
have conv_rhs : Eq (α := Q.Ring)
  ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (↑(Q.kerCompPreimage P x) : (Q.comp P).Ring) : Q.Ring)
  (∑ v ∈ support (↑x : Q.Ring), (monomial v : (a : S) → MvPolynomial ι' S) (coeff v (↑x : Q.Ring)) : MvPolynomial ι' S)
Tactic: conv_rhs => rw [← x.1.support_sum_monomial_coeff]