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
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)
⊢ (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)
have 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)
Tactic: rw [toAlgHom, aeval_monomial, Algebra.smul_def]
-- 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 : Generators R S ι
⊢ (Hom.id P).toAlgHom = AlgHom.id R P.Ring
have 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)
Tactic: ext1
-- 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 : 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 : ι
⊢ 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'')
have 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'')
Tactic: rw [IsScalarTower.algebraMap_apply S S' S'', ← g.aeval_val]
-- 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 : 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 : ι
⊢ 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'')
have induction : ∀ (x : P'.Ring),
  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'')
Tactic: induction g.val x using MvPolynomial.induction_on with
    | C r => simp [← IsScalarTower.algebraMap_apply]
    | add x y hx hy => simp only [map_add, hx, hy]
    | mul_X p i hp => simp only [map_mul, hp, aeval_X, aeval_val]
-- 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 : 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'
⊢ f.comp (Hom.id P) = f
have val : ∀ (x : ι) (m : ι' →₀ ℕ), coeff m (val (f.comp (Hom.id P)) x) = coeff m (f.val x)
Tactic: ext
-- 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 : 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 S S'
f : P.Hom P'
⊢ (Hom.id P').comp f = f
have val : ∀ (x : ι) (m : ι' →₀ ℕ), coeff m (val ((Hom.id P').comp f) x) = coeff m (f.val x)
Tactic: ext
-- 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 : 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 R''
inst_16 : IsScalarTower R R' R''
inst_17 : IsScalarTower R' R'' S''
inst_18 : IsScalarTower R' S' S''
inst_19 : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
p : MvPolynomial ι R
i : ι
hp :
  Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) p : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) p) : P''.Ring)
⊢ Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) (p * X i) : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) (p * X i)) : P''.Ring)
have mul_X : HMul.hMul (α := P''.Ring) (β := P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) p) : P''.Ring)
    ((aeval g.val : (a : MvPolynomial ι' R') → P''.Ring) (f.val i) : P''.Ring) =
  HMul.hMul (α := P''.Ring) (β := P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) p) : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) (f.val i) : P''.Ring)
Tactic: simp only [map_mul, hp, toAlgHom_X, comp_val]
-- 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 : 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 R''
inst_16 : IsScalarTower R R' R''
inst_17 : IsScalarTower R' R'' S''
inst_18 : IsScalarTower R' S' S''
inst_19 : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x : P.Ring
⊢ Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) x : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) x) : P''.Ring)
have C : ∀ (r : R),
  Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) ((C : (a : R) → MvPolynomial ι R) r) : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring)
        ((f.toAlgHom : (a : P.Ring) → P'.Ring) ((C : (a : R) → MvPolynomial ι R) r)) :
      P''.Ring)
Tactic: induction x using MvPolynomial.induction_on with
  | C r => simp only [← MvPolynomial.algebraMap_eq, AlgHom.map_algebraMap]
  | add x y hx hy => simp only [map_add, hx, hy]
  | mul_X p i hp => simp only [map_mul, hp, toAlgHom_X, comp_val]; rfl
Cleared hypotheses: 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
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 R''
inst_16 : IsScalarTower R R' R''
inst_17 : IsScalarTower R' R'' S''
inst_18 : IsScalarTower R' S' S''
inst_19 : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x : P.Ring
C :
  ∀ (r : R),
    Eq (α := P''.Ring)
      ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) ((MvPolynomial.C : (a : R) → MvPolynomial ι R) r) : P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring)
          ((f.toAlgHom : (a : P.Ring) → P'.Ring) ((MvPolynomial.C : (a : R) → MvPolynomial ι R) r)) :
        P''.Ring)
⊢ Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) x : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) x) : P''.Ring)
have add : ∀ (x y : MvPolynomial ι R)
  (hx :
    Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) x : P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) x) : P''.Ring))
  (hy :
    Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) y : P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) y) : P''.Ring)),
  Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) (x + y) : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) (x + y)) : P''.Ring)
Tactic: induction x using MvPolynomial.induction_on with
  | C r => simp only [← MvPolynomial.algebraMap_eq, AlgHom.map_algebraMap]
  | add x y hx hy => simp only [map_add, hx, hy]
  | mul_X p i hp => simp only [map_mul, hp, toAlgHom_X, comp_val]; rfl
Cleared hypotheses: 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
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 R''
inst_16 : IsScalarTower R R' R''
inst_17 : IsScalarTower R' R'' S''
inst_18 : IsScalarTower R' S' S''
inst_19 : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x : P.Ring
C :
  ∀ (r : R),
    Eq (α := P''.Ring)
      ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) ((MvPolynomial.C : (a : R) → MvPolynomial ι R) r) : P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring)
          ((f.toAlgHom : (a : P.Ring) → P'.Ring) ((MvPolynomial.C : (a : R) → MvPolynomial ι R) r)) :
        P''.Ring)
add :
  ∀ (x y : MvPolynomial ι R)
    (hx :
      Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) x : P''.Ring)
        ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) x) : P''.Ring))
    (hy :
      Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) y : P''.Ring)
        ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) y) : P''.Ring)),
    Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) (x + y) : P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) (x + y)) : P''.Ring)
⊢ Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) x : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) x) : P''.Ring)
have mul_X : ∀ (p : MvPolynomial ι R) (i : ι)
  (hp :
    Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) p : P''.Ring)
      ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) p) : P''.Ring)),
  Eq (α := P''.Ring) ((toAlgHom (g.comp f) : (a : P.Ring) → P''.Ring) (p * X i) : P''.Ring)
    ((g.toAlgHom : (a : P'.Ring) → P''.Ring) ((f.toAlgHom : (a : P.Ring) → P'.Ring) (p * X i)) : P''.Ring)
Tactic: induction x using MvPolynomial.induction_on with
  | C r => simp only [← MvPolynomial.algebraMap_eq, AlgHom.map_algebraMap]
  | add x y hx hy => simp only [map_add, hx, hy]
  | mul_X p i hp => simp only [map_mul, hp, toAlgHom_X, comp_val]; rfl
Cleared hypotheses: 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
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 ι
i : ι' ⊕ ι
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) : T)
    ((algebraMap T T : (a : T) → T) (val (Q.comp P) i) : T)
have inl : ∀ (val : ι'),
  Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T)
        (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) (Sum.inl val)) :
      T)
    ((algebraMap T T : (a : T) → T) (Generators.val (Q.comp P) (Sum.inl val)) : T)
Tactic: cases i
Cleared hypotheses: 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 ι
i : ι' ⊕ ι
inl :
  ∀ (val : ι'),
    Eq.{u_7 + 1} (α := T)
      ((aeval Q.val : (a : MvPolynomial ι' S) → T)
          (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) (Sum.inl val)) :
        T)
      ((algebraMap T T : (a : T) → T) (Generators.val (Q.comp P) (Sum.inl val)) : T)
⊢ Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) i) : T)
    ((algebraMap T T : (a : T) → T) (val (Q.comp P) i) : T)
have inr : ∀ (val : ι),
  Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T)
        (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) (Sum.inr val)) :
      T)
    ((algebraMap T T : (a : T) → T) (Generators.val (Q.comp P) (Sum.inr val)) : T)
Tactic: cases i
Cleared hypotheses: 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
ι' : 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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
⊢ Eq (α := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((monomial (v₁.sumElim v₂) : (a : R) → MvPolynomial (ι' ⊕ ι) R) a) :
      Q.Ring)
    ((monomial v₁ : (a : S) → MvPolynomial ι' S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((monomial v₂ : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)) :
      MvPolynomial ι' S)
have rw : HSMul.hSMul (β := Q.Ring) a
    ((v₁.sumElim v₂).prod fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦ Hom.val (P := Q.comp P) (Q.ofComp P) x1 ^ x2) =
  HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
    ((C : (a : S) → MvPolynomial ι' S)
        ((aeval P.val : (a : MvPolynomial ι R) → S) ((monomial v₂ : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)) :
      MvPolynomial ι' S)
    (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)
Tactic: rw [Hom.toAlgHom_monomial, monomial_eq]
-- 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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
⊢ HSMul.hSMul (β := Q.Ring) a
      ((v₁.sumElim v₂).prod fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦ Hom.val (P := Q.comp P) (Q.ofComp P) x1 ^ x2) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S)
          ((aeval P.val : (a : MvPolynomial ι R) → S)
            ((monomial v₂ : (a : R) → MvPolynomial ι R) a : MvPolynomial ι R)) :
        MvPolynomial ι' S)
      (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)
have simp : HSMul.hSMul (β := Q.Ring) a
    ((v₁.sumElim v₂).prod fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
      HPow.hPow (α := Q.Ring) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) x1) x2) =
  HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
    ((C : (a : S) → MvPolynomial ι' S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
          (v₂.prod fun (i : ι) (k : ℕ) ↦ P.val i ^ k : S)) :
      MvPolynomial ι' S)
    (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)
Tactic: simp only [ofComp_val, aeval_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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
⊢ HSMul.hSMul (β := Q.Ring) a
      ((v₁.sumElim v₂).prod fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
        HPow.hPow (α := Q.Ring) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) x1) x2) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
            (v₂.prod fun (i : ι) (k : ℕ) ↦ P.val i ^ k : S)) :
        MvPolynomial ι' S)
      (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)
have rw : a •
    HMul.hMul (α := Q.Ring)
      (v₁.prod
        ((fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
            HPow.hPow (α := Q.Ring) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) x1) x2) ∘
          Sum.inl))
      (v₂.prod
        ((fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
            HPow.hPow (α := Q.Ring) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) x1) x2) ∘
          Sum.inr)) =
  HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
    ((C : (a : S) → MvPolynomial ι' S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
          (v₂.prod fun (i : ι) (k : ℕ) ↦ P.val i ^ k : S)) :
      MvPolynomial ι' S)
    (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)
Tactic: rw [Finsupp.prod_sumElim]
-- 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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
⊢ a •
      HMul.hMul (α := Q.Ring)
        (v₁.prod
          ((fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
              HPow.hPow (α := Q.Ring) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) x1) x2) ∘
            Sum.inl))
        (v₂.prod
          ((fun (x1 : ι' ⊕ ι) (x2 : ℕ) ↦
              HPow.hPow (α := Q.Ring) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) x1) x2) ∘
            Sum.inr)) =
    HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
      ((C : (a : S) → MvPolynomial ι' S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
            (v₂.prod fun (i : ι) (k : ℕ) ↦ P.val i ^ k : S)) :
        MvPolynomial ι' S)
      (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e : MvPolynomial ι' S)
have simp : HMul.hMul (α := Q.Ring) ((C : (a : S) → MvPolynomial ι' S) ((algebraMap R S : (a : R) → S) a) : MvPolynomial ι' S)
    (HMul.hMul (α := Q.Ring) (v₁.prod fun (x : ι') (x2 : ℕ) ↦ HPow.hPow (α := Q.Ring) (X x) x2)
      ((C : (a : S) → Q.Ring) (v₂.prod fun (a : ι) ↦ HPow.hPow (P.val a)))) =
  HMul.hMul (α := MvPolynomial ι' S)
    ((C : (a : S) → MvPolynomial ι' S) ((algebraMap R S : (a : R) → S) a) : MvPolynomial ι' S)
    (HMul.hMul (α := MvPolynomial ι' S) ((C : (a : S) → MvPolynomial ι' S) (v₂.prod fun (i : ι) (k : ℕ) ↦ P.val i ^ k))
      (v₁.prod fun (n : ι') (e : ℕ) ↦ HPow.hPow (α := MvPolynomial ι' S) (X n) e))
Tactic: simp only [Function.comp_def, Sum.elim_inl, Sum.elim_inr, ← map_pow, ← map_finsuppProd,
    C_mul, Algebra.smul_def, MvPolynomial.algebraMap_apply, mul_assoc]