awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
α : Type u_2
inst_3 : Finite α
P : Generators R S α
⊢ FiniteType R S

Tactic:
.of_surjective (IsScalarTower.toAlgHom R P.Ring S) P.algebraMap_surjective

Premises used: Algebra.FiniteType.of_surjective, Algebra.Generators.Ring, Algebra.Generators.algebraMap_surjective, IsScalarTower.toAlgHom
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ FiniteType R S ↔ ∃ (n : ℕ), Nonempty (Generators R S (Fin n))

Tactic:
⟨fun h ↦ ?_, fun ⟨n, ⟨P⟩⟩ ↦ P.finiteType⟩

Premises used: Algebra.FiniteType, Algebra.Generators.finiteType, Iff.intro, _private.0.Algebra.FiniteType.iff_exists_generators.match_1
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
refine : ∀ (h : FiniteType R S), ∃ (n : ℕ), Nonempty (Generators R S (Fin n))
⊢ FiniteType R S ↔ ∃ (n : ℕ), Nonempty (Generators R S (Fin n))

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨n, ⟨P⟩⟩ ↦ P.finiteType⟩
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : FiniteType R S
obtain :
  ∀ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S)
    (hf :
      Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
        (⇑f : (a : MvPolynomial (Fin n) R) → S)),
    ∃ (n : ℕ), Nonempty (Generators R S (Fin n))
⊢ ∃ (n : ℕ), Nonempty (Generators R S (Fin n))

Tactic:
obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp h

Premises used: Iff.mp, Algebra.FiniteType.iff_quotient_mvPolynomial''
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (hf :
      Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
        (⇑(aeval
              (Function.comp.{1, u + 1, v + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → S)
                X)) :
          (a : MvPolynomial (Fin n) R) → S)),
    Function.Surjective.{max (u + 1) 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
      (⇑(aeval fun (i : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X i)) : (a : MvPolynomial (Fin n) R) → S)
⊢ Function.Surjective.{max (u + 1) 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
    (⇑(aeval fun (i : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X i)) : (a : MvPolynomial (Fin n) R) → S)

Tactic:
rwa [aeval_unique f] at hf

Premises used: MvPolynomial.aeval_unique
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
⊢ ∃ (n : ℕ), Nonempty (Generators R S (Fin n))

Tactic:
exact ⟨n, ⟨.ofSurjective (fun i ↦ f (X i)) <| by rwa [aeval_unique f] at hf⟩⟩
-- 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
P : 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' ι'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f : P.Hom P'
x : P.Ring
suffices :
  Eq (α := P.Ring →ₐ[R] S') (AlgHom.comp (AlgHom.restrictScalars R (aeval P'.val)) f.toAlgHom)
    (AlgHom.comp (IsScalarTower.toAlgHom R S S') (aeval P.val))
⊢ Eq.{u_2 + 1} (α := S')
    ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f.toAlgHom : (a : P.Ring) → P'.Ring) x : P'.Ring) : S')
    ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S')

Tactic:
suffices ((MvPolynomial.aeval P'.val).restrictScalars R).comp f.toAlgHom =
      (IsScalarTower.toAlgHom R S S').comp (MvPolynomial.aeval P.val) from
    DFunLike.congr_fun this x
-- 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
P : 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' ι'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f : P.Hom P'
x : P.Ring
hf :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := S')
      ((AlgHom.comp (AlgHom.restrictScalars R (aeval P'.val)) f.toAlgHom : (a : MvPolynomial ι R) → S') (X i) : S')
      ((AlgHom.comp (IsScalarTower.toAlgHom R S S') (aeval P.val) : (a : MvPolynomial ι R) → S') (X i) : S')
⊢ Eq (α := P.Ring →ₐ[R] S') (AlgHom.comp (AlgHom.restrictScalars R (aeval P'.val)) f.toAlgHom)
    (AlgHom.comp (IsScalarTower.toAlgHom R S S') (aeval P.val))

Tactic:
apply MvPolynomial.algHom_ext

Premises used: MvPolynomial.algHom_ext
-- 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
P : 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' ι'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f : P.Hom P'
x : P.Ring
i : ι
⊢ Eq.{u_2 + 1} (α := S')
    ((AlgHom.comp (AlgHom.restrictScalars R (aeval P'.val)) f.toAlgHom : (a : MvPolynomial ι R) → S') (X i) : S')
    ((AlgHom.comp (IsScalarTower.toAlgHom R S S') (aeval P.val) : (a : MvPolynomial ι R) → S') (X i) : S')

Tactic:
simp [Hom.toAlgHom]

Premises used: Algebra.Generators.Hom.toAlgHom
-- 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
P : Generators R S ι
R' : Type u_1
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : Algebra R R'
inst_5 : Algebra R' S
inst_6 : IsScalarTower R R' S
P' : Generators R' S ι'
f : P.Hom P'
x : P.Ring
⊢ Eq.{v + 1} (α := S)
    ((aeval P'.val : (a : MvPolynomial ι' R') → S) ((f.toAlgHom : (a : P.Ring) → P'.Ring) x : P'.Ring) : S)
    ((aeval P.val : (a : MvPolynomial ι R) → S) x : S)

Tactic:
f.algebraMap_toAlgHom _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Algebra.Generators.Hom.algebraMap_toAlgHom, Finset.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
P : 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' ι'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
f : P.Hom P'
i : ι
⊢ (f.toAlgHom : (a : P.Ring) → P'.Ring) (X i) = f.val i

Tactic:
MvPolynomial.aeval_X f.val i

Premises used: MvPolynomial.aeval_X, Algebra.Generators.Hom.val
-- 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
P : 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' ι'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
f : P.Hom P'
r : R
⊢ Eq (α := P'.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) ((C : (a : R) → MvPolynomial ι R) r) : P'.Ring)
    ((C : (a : R') → MvPolynomial ι' R') ((algebraMap R R' : (a : R) → R') r) : MvPolynomial ι' R')

Tactic:
MvPolynomial.aeval_C f.val r

Premises used: Algebra.Generators.Hom.val, MvPolynomial.aeval_C
-- 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
P : 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' ι'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
f : P.Hom P'
v : ι →₀ ℕ
r : R
rw :
  (aeval f.val : (a : P.Ring) → P'.Ring) ((monomial v : (a : R) → MvPolynomial ι R) r) =
    HSMul.hSMul (β := P'.Ring) r (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f.val x1 ^ x2)
rw₁ :
  HMul.hMul (α := P'.Ring) (β := P'.Ring) ((algebraMap R P'.Ring : (a : R) → P'.Ring) r : P'.Ring)
      (v.prod fun (i : ι) (k : ℕ) ↦ f.val i ^ k : P'.Ring) =
    HSMul.hSMul (β := P'.Ring) r (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f.val x1 ^ x2)
rw₂ rw₃ :
  HMul.hMul (α := P'.Ring) (β := P'.Ring) ((algebraMap R P'.Ring : (a : R) → P'.Ring) r : P'.Ring)
      (v.prod fun (i : ι) (k : ℕ) ↦ f.val i ^ k : P'.Ring) =
    HMul.hMul (α := P'.Ring) (β := P'.Ring) ((algebraMap R P'.Ring : (a : R) → P'.Ring) r : P'.Ring)
      (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f.val x1 ^ x2 : P'.Ring)
⊢ (f.toAlgHom : (a : P.Ring) → P'.Ring) ((monomial v : (a : R) → MvPolynomial ι R) r) =
    HSMul.hSMul (β := P'.Ring) r (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f.val x1 ^ x2)

Tactic:
rw [toAlgHom, aeval_monomial, Algebra.smul_def]

Premises used: Algebra.Generators.Hom.toAlgHom, Algebra.smul_def, MvPolynomial.aeval_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
P : 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''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
inst_17 : IsScalarTower R S S'
f :
  { f : P.Ring →ₐ[R] P'.Ring //
    ∀ (x : P.Ring),
      Eq.{u_2 + 1} (α := S')
        ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) : S')
        ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S') }
i : ι
⊢ Eq.{u_2 + 1} (α := S')
    ((aeval P'.val : (a : MvPolynomial ι' R') → S')
        ((fun (i : ι) ↦ (((↑f : P.Ring →ₐ[R] P'.Ring) : (a : P.Ring) → P'.Ring) (X i) : P'.Ring)) i) :
      S')
    ((algebraMap S S' : (a : S) → S') (P.val i) : S')

Tactic:
simp [f.2]

Premises used: Subtype.property
-- 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
P : 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''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
inst_17 : IsScalarTower R S S'
f : P.Hom P'
x : ι
m : ι' →₀ ℕ
⊢ coeff m
      (val.{w, u, v, u_1, u_2, u_3} (R := R) (S := S) (P := P)
        ((fun
              (f :
                { f : P.Ring →ₐ[R] P'.Ring //
                  ∀ (x : P.Ring),
                    Eq.{u_2 + 1} (α := S')
                      ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) : S')
                      ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S') }) ↦
            ({ val := fun (i : ι) ↦ ((↑f : P.Ring →ₐ[R] P'.Ring) : (a : P.Ring) → P'.Ring) (X i), aeval_val := ⋯ } :
              P.Hom P'))
          ((fun (f : P.Hom P') ↦
              (Subtype.mk (p := fun (f : P.Ring →ₐ[R] P'.Ring) ↦
                  ∀ (x : P.Ring),
                    Eq.{u_2 + 1} (α := S')
                      ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) : S')
                      ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S'))
                  f.toAlgHom ⋯ :
                { f : P.Ring →ₐ[R] P'.Ring //
                  ∀ (x : P.Ring),
                    Eq.{u_2 + 1} (α := S')
                      ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) : S')
                      ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S') }))
            f))
        x) =
    coeff m (f.val x)

Tactic:
simp
-- 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
P : 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''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
inst_17 : IsScalarTower R S S'
f :
  { f : P.Ring →ₐ[R] P'.Ring //
    ∀ (x : P.Ring),
      Eq.{u_2 + 1} (α := S')
        ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) : S')
        ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S') }
i : ι
m : ι' →₀ ℕ
⊢ Eq.{u_1 + 1} (α := R')
    (coeff m
      (((↑((fun (f : P.Hom P') ↦
                  (Subtype.mk (p := fun (f : P.Ring →ₐ[R] P'.Ring) ↦
                      ∀ (x : P.Ring),
                        Eq.{u_2 + 1} (α := S')
                          ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) :
                            S')
                          ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S'))
                      f.toAlgHom ⋯ :
                    { f : P.Ring →ₐ[R] P'.Ring //
                      ∀ (x : P.Ring),
                        Eq.{u_2 + 1} (α := S')
                          ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) :
                            S')
                          ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S') }))
                ((fun
                      (f :
                        { f : P.Ring →ₐ[R] P'.Ring //
                          ∀ (x : P.Ring),
                            Eq.{u_2 + 1} (α := S')
                              ((aeval P'.val : (a : MvPolynomial ι' R') → S')
                                  ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) :
                                S')
                              ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) :
                                S') }) ↦
                    ({ val := fun (i : ι) ↦ ((↑f : P.Ring →ₐ[R] P'.Ring) : (a : P.Ring) → P'.Ring) (X i),
                        aeval_val := ⋯ } :
                      P.Hom P'))
                  f)) :
            P.Ring →ₐ[R] P'.Ring) :
          (a : MvPolynomial ι R) → P'.Ring)
        (X i)))
    (coeff m (((↑f : P.Ring →ₐ[R] P'.Ring) : (a : MvPolynomial ι R) → P'.Ring) (X i)))

Tactic:
simp
-- 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
P : 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''
x : ι
⊢ Eq.{u_2 + 1} (α := S')
    ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((P'.σ ∘ (⇑(algebraMap S S') : (a : S) → S') ∘ P.val) x) : S')
    ((algebraMap S S' : (a : S) → S') (P.val x) : S')

Tactic:
simp
-- 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
P : 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''
⊢ ∀ (i : ι),
    Eq.{v + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) (X i) : S)
      ((algebraMap S S : (a : S) → S) (P.val i) : S)

Tactic:
simp
-- 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
P : Generators R S ι
hf :
  ∀ (i : ι),
    Eq (α := P.Ring) (((Hom.id P).toAlgHom : (a : MvPolynomial ι R) → P.Ring) (X i) : P.Ring)
      ((AlgHom.id R P.Ring : (a : MvPolynomial ι R) → P.Ring) (X i) : P.Ring)
⊢ (Hom.id P).toAlgHom = AlgHom.id R P.Ring

Tactic:
ext1
-- 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
P : Generators R S ι
i : ι
⊢ Eq (α := P.Ring) (((Hom.id P).toAlgHom : (a : MvPolynomial ι R) → P.Ring) (X i) : P.Ring)
    ((AlgHom.id R P.Ring : (a : MvPolynomial ι R) → P.Ring) (X i) : P.Ring)

Tactic:
simp
-- 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
P : 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''
inst_15 : IsScalarTower R' R'' S''
inst_16 : IsScalarTower R' S' S''
inst_17 : IsScalarTower S S' S''
f : P'.Hom P''
g : P.Hom P'
x : ι
rw :
  Eq.{u_5 + 1} (α := S'')
    ((aeval P''.val : (a : MvPolynomial ι'' R'') → S'')
        ((aeval f.val : (a : MvPolynomial ι' R') → P''.Ring) (g.val x) : P''.Ring) :
      S'')
    ((algebraMap S' S'' : (a : S') → S'') ((aeval P'.val : (a : MvPolynomial ι' R') → S') (g.val x) : S') : S'')
⊢ Eq.{u_5 + 1} (α := S'')
    ((aeval P''.val : (a : MvPolynomial ι'' R'') → S'')
        ((aeval f.val : (a : MvPolynomial ι' R') → P''.Ring) (g.val x) : P''.Ring) :
      S'')
    ((algebraMap S S'' : (a : S) → S'') (P.val x) : S'')

Tactic:
rw [IsScalarTower.algebraMap_apply S S' S'', ← g.aeval_val]

Premises used: Algebra.Generators.Hom.aeval_val, IsScalarTower.algebraMap_apply
-- 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
P : 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''
inst_15 : IsScalarTower R' R'' S''
inst_16 : IsScalarTower R' S' S''
inst_17 : IsScalarTower S S' S''
f : P'.Hom P''
g : P.Hom P'
x : ι
r : R'
⊢ Eq.{u_5 + 1} (α := S'')
    ((aeval P''.val : (a : MvPolynomial ι'' R'') → S'')
        ((aeval f.val : (a : MvPolynomial ι' R') → P''.Ring) ((C : (a : R') → MvPolynomial ι' R') r) : P''.Ring) :
      S'')
    ((algebraMap S' S'' : (a : S') → S'')
        ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((C : (a : R') → MvPolynomial ι' R') r : MvPolynomial ι' R') :
          S') :
      S'')

Tactic:
simp [← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- 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
P : 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''
inst_15 : IsScalarTower R' R'' S''
inst_16 : IsScalarTower R' S' S''
inst_17 : IsScalarTower S S' S''
f : P'.Hom P''
g : P.Hom P'
x_1 : ι
x y : MvPolynomial ι' R'
hx :
  Eq.{u_5 + 1} (α := S'')
    ((aeval P''.val : (a : MvPolynomial ι'' R'') → S'')
        ((aeval f.val : (a : MvPolynomial ι' R') → P''.Ring) x : P''.Ring) :
      S'')
    ((algebraMap S' S'' : (a : S') → S'') ((aeval P'.val : (a : MvPolynomial ι' R') → S') x : S') : S'')
hy :
  Eq.{u_5 + 1} (α := S'')
    ((aeval P''.val : (a : MvPolynomial ι'' R'') → S'')
        ((aeval f.val : (a : MvPolynomial ι' R') → P''.Ring) y : P''.Ring) :
      S'')
    ((algebraMap S' S'' : (a : S') → S'') ((aeval P'.val : (a : MvPolynomial ι' R') → S') y : S') : S'')
⊢ Eq.{u_5 + 1} (α := S'')
    ((aeval P''.val : (a : MvPolynomial ι'' R'') → S'')
        ((aeval f.val : (a : MvPolynomial ι' R') → P''.Ring) (x + y) : P''.Ring) :
      S'')
    ((algebraMap S' S'' : (a : S') → S'') ((aeval P'.val : (a : MvPolynomial ι' R') → S') (x + y) : S') : S'')

Tactic:
simp only [map_add, hx, hy]

Premises used: map_add
-- 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
P : 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''
inst_15 : IsScalarTower R' R'' S''
inst_16 : IsScalarTower R' S' S''
inst_17 : IsScalarTower S S' S''
f : P'.Hom P''
g : P.Hom P'
x : ι
p : MvPolynomial ι' R'
i : ι'
hp :
  Eq.{u_5 + 1} (α := S'')
    ((aeval P''.val : (a : MvPolynomial ι'' R'') → S'')
        ((aeval f.val : (a : MvPolynomial ι' R') → P''.Ring) p : P''.Ring) :
      S'')
    ((algebraMap S' S'' : (a : S') → S'') ((aeval P'.val : (a : MvPolynomial ι' R') → S') p : S') : S'')
⊢ Eq.{u_5 + 1} (α := S'')
    ((aeval P''.val : (a : MvPolynomial ι'' R'') → S'')
        ((aeval f.val : (a : MvPolynomial ι' R') → P''.Ring) (p * X i) : P''.Ring) :
      S'')
    ((algebraMap S' S'' : (a : S') → S'') ((aeval P'.val : (a : MvPolynomial ι' R') → S') (p * X i) : S') : S'')

Tactic:
simp only [map_mul, hp, aeval_X, aeval_val]

Premises used: MvPolynomial.aeval_X, Algebra.Generators.Hom.aeval_val, map_mul