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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
⊢ 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))
have nth_rw : HMul.hMul (α := Q.Ring) ((C : (a : S) → MvPolynomial ι' S) ((algebraMap R S : (a : R) → S) a) : MvPolynomial ι' S)
    (HMul.hMul (α := Q.Ring) ((C : (a : S) → Q.Ring) (v₂.prod fun (a : ι) ↦ HPow.hPow (P.val a)))
      (v₁.prod fun (x : ι') (x2 : ℕ) ↦ HPow.hPow (α := Q.Ring) (X x) x2)) =
  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: nth_rw 2 [mul_comm]
-- 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 ι
j : ι →₀ ℕ
a : R
⊢ Eq (α := Generators.Ring (Q.comp P))
    ((Hom.toAlgHom (Q.toComp P) : (a : P.Ring) → (Q.comp P).Ring) ((monomial j : (a : R) → MvPolynomial ι R) a) :
      Generators.Ring (Q.comp P))
    ((monomial (Finsupp.sumElim 0 j) : (a : R) → MvPolynomial (ι' ⊕ ι) R) a : MvPolynomial (ι' ⊕ ι) R)
have h : Eq (α := (g : ι →₀ ℕ) → ι' ⊕ ι →₀ ℕ) (Finsupp.sumElim 0) (Finsupp.mapDomain Sum.inr)
Tactic: convert! rename_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 ι
j : ι →₀ ℕ
a : R
⊢ Eq (α := (g : ι →₀ ℕ) → ι' ⊕ ι →₀ ℕ) (Finsupp.sumElim 0) (Finsupp.mapDomain Sum.inr)
have h : ∀ (f : ι →₀ ℕ) (i₁ : ι'),
  Eq (α := ℕ) ((Finsupp.sumElim 0 f : (a : ι' ⊕ ι) → ℕ) (Sum.inl i₁) : ℕ)
    ((Finsupp.mapDomain Sum.inr f : (a : ι' ⊕ ι) → ℕ) (Sum.inl i₁) : ℕ)
Tactic: ext f (i₁ | 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 ι
j : ι →₀ ℕ
a : R
h :
  ∀ (f : ι →₀ ℕ) (i₁ : ι'),
    Eq (α := ℕ) ((Finsupp.sumElim 0 f : (a : ι' ⊕ ι) → ℕ) (Sum.inl i₁) : ℕ)
      ((Finsupp.mapDomain Sum.inr f : (a : ι' ⊕ ι) → ℕ) (Sum.inl i₁) : ℕ)
⊢ Eq (α := (g : ι →₀ ℕ) → ι' ⊕ ι →₀ ℕ) (Finsupp.sumElim 0) (Finsupp.mapDomain Sum.inr)
have h₁ : ∀ (f : ι →₀ ℕ) (i₂ : ι),
  Eq (α := ℕ) ((Finsupp.sumElim 0 f : (a : ι' ⊕ ι) → ℕ) (Sum.inr i₂) : ℕ)
    ((Finsupp.mapDomain Sum.inr f : (a : ι' ⊕ ι) → ℕ) (Sum.inr i₂) : ℕ)
Tactic: ext f (i₁ | 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 ι
p : P.Ring
⊢ Eq (α := MvPolynomial ι R →ₐ[R] Q.Ring)
    (AlgHom.comp (B := Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.ofComp P)) (rename Sum.inr))
    (AlgHom.comp (IsScalarTower.toAlgHom R S Q.Ring) (IsScalarTower.toAlgHom R P.Ring S))
have hf : ∀ (i : ι) (m : ι' →₀ ℕ),
  Eq.{v + 1} (α := S)
    (coeff m
      ((AlgHom.comp (B := Generators.Ring (Q.comp P)) (Hom.toAlgHom (Q.ofComp P)) (rename Sum.inr) :
          (a : MvPolynomial ι R) → Q.Ring)
        (X i)))
    (coeff m
      ((AlgHom.comp (IsScalarTower.toAlgHom R S Q.Ring) (IsScalarTower.toAlgHom R P.Ring S) :
          (a : MvPolynomial ι R) → Q.Ring)
        (X i)))
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
ι' : 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 ι
a : S
⊢ ∃ (a_1 : Generators.Ring (Q.comp P)),
    Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a_1 : Q.Ring)
      ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
have h : Eq (α := Q.Ring)
  ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
      ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ a)) :
    Q.Ring)
  ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
Tactic: use MvPolynomial.rename Sum.inr (P.σ a)
-- 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 ι
a : S
⊢ Eq (α := Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring)
        ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (ι' ⊕ ι) R) (P.σ a)) :
      Q.Ring)
    ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
have h : Eq (α := Q.Ring)
  ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → Q.Ring) (P.σ a) : Q.Ring)
  ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
Tactic: simp only [Hom.toAlgHom, ofComp, Generators.comp, MvPolynomial.aeval_rename,
        Sum.elim_comp_inr]
-- 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 ι
a : S
⊢ Eq (α := Q.Ring)
    ((aeval ((⇑C : (a : S) → MvPolynomial ι' S) ∘ P.val) : (a : MvPolynomial ι R) → Q.Ring) (P.σ a) : Q.Ring)
    ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
have h : Eq (α := Q.Ring)
  ((AlgHom.comp (IsScalarTower.toAlgHom R S (MvPolynomial ι' S)) (aeval P.val) : (a : MvPolynomial ι R) → Q.Ring)
      (P.σ a) :
    Q.Ring)
  ((IsScalarTower.toAlgHom R S (MvPolynomial ι' S) : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
Tactic: simp_rw [Function.comp_def, ← MvPolynomial.algebraMap_eq, ← IsScalarTower.toAlgHom_apply R,
        ← MvPolynomial.comp_aeval]
-- 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 ι
p q : MvPolynomial ι' S
hp : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p
hq : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = q
⊢ ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p + q
have add : ∀ (p : Generators.Ring (Q.comp P)),
  ∃ (a : Generators.Ring (Q.comp P)),
    (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a =
      HAdd.hAdd (α := MvPolynomial ι' S) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring) q
Tactic: obtain ⟨p, rfl⟩ := hp
Cleared hypotheses: p, hp
-- 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 ι
q : MvPolynomial ι' S
hq : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = q
p : Generators.Ring (Q.comp P)
⊢ ∃ (a : Generators.Ring (Q.comp P)),
    (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a =
      HAdd.hAdd (α := MvPolynomial ι' S) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring) q
have add : ∀ (q : Generators.Ring (Q.comp P)),
  ∃ (a : Generators.Ring (Q.comp P)),
    (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a =
      HAdd.hAdd (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring)
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) q : Q.Ring)
Tactic: obtain ⟨q, rfl⟩ := hq
Cleared hypotheses: q, hq
-- 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 ι
p q : Generators.Ring (Q.comp P)
⊢ ∃ (a : Generators.Ring (Q.comp P)),
    (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a =
      HAdd.hAdd (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring)
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) q : Q.Ring)
have h : (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (p + q) =
  HAdd.hAdd (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) q : Q.Ring)
Tactic: use p + q
-- 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 ι
p : MvPolynomial ι' S
i : ι'
hp : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p
⊢ ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p * X i
have mul_X : ∀ (p : MvPolynomial (ι' ⊕ ι) R),
  ∃ (a : Generators.Ring (Q.comp P)),
    (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a =
      HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring) (X i)
Tactic: obtain ⟨(p : MvPolynomial (ι' ⊕ ι) R), rfl⟩ := hp
Cleared hypotheses: p, hp
-- 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 ι
i : ι'
p : MvPolynomial (ι' ⊕ ι) R
⊢ ∃ (a : Generators.Ring (Q.comp P)),
    (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a =
      HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring) (X i)
have h : (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) (p * X (Sum.inl i)) =
  HMul.hMul (α := MvPolynomial ι' S) (β := MvPolynomial ι' S)
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p : Q.Ring) (X i)
Tactic: use p * MvPolynomial.X (R := R) (Sum.inl 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 ι
p : Q.Ring
⊢ ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p
have C : ∀ (a : S),
  ∃ (a_1 : Generators.Ring (Q.comp P)),
    Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a_1 : Q.Ring)
      ((C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
Tactic: induction p using MvPolynomial.induction_on with
  | C a =>
      use MvPolynomial.rename Sum.inr (P.σ a)
      simp only [Hom.toAlgHom, ofComp, Generators.comp, MvPolynomial.aeval_rename,
        Sum.elim_comp_inr]
      simp_rw [Function.comp_def, ← MvPolynomial.algebraMap_eq, ← IsScalarTower.toAlgHom_apply R,
        ← MvPolynomial.comp_aeval]
      simp
  | add p q hp hq =>
      obtain ⟨p, rfl⟩ := hp
      obtain ⟨q, rfl⟩ := hq
      use p + q
      simp
  | mul_X p i hp =>
      obtain ⟨(p : MvPolynomial (ι' ⊕ ι) R), rfl⟩ := hp
      use p * MvPolynomial.X (R := R) (Sum.inl i)
      simp [Algebra.Generators.ofComp, Algebra.Generators.Hom.toAlgHom]
Cleared hypotheses: p
-- 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 ι
p : Q.Ring
C :
  ∀ (a : S),
    ∃ (a_1 : Generators.Ring (Q.comp P)),
      Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a_1 : Q.Ring)
        ((MvPolynomial.C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
⊢ ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p
have add : ∀ (p q : MvPolynomial ι' S)
  (hp : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p)
  (hq : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = q),
  ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p + q
Tactic: induction p using MvPolynomial.induction_on with
  | C a =>
      use MvPolynomial.rename Sum.inr (P.σ a)
      simp only [Hom.toAlgHom, ofComp, Generators.comp, MvPolynomial.aeval_rename,
        Sum.elim_comp_inr]
      simp_rw [Function.comp_def, ← MvPolynomial.algebraMap_eq, ← IsScalarTower.toAlgHom_apply R,
        ← MvPolynomial.comp_aeval]
      simp
  | add p q hp hq =>
      obtain ⟨p, rfl⟩ := hp
      obtain ⟨q, rfl⟩ := hq
      use p + q
      simp
  | mul_X p i hp =>
      obtain ⟨(p : MvPolynomial (ι' ⊕ ι) R), rfl⟩ := hp
      use p * MvPolynomial.X (R := R) (Sum.inl i)
      simp [Algebra.Generators.ofComp, Algebra.Generators.Hom.toAlgHom]
Cleared hypotheses: p
-- 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 ι
p : Q.Ring
C :
  ∀ (a : S),
    ∃ (a_1 : Generators.Ring (Q.comp P)),
      Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a_1 : Q.Ring)
        ((MvPolynomial.C : (a : S) → MvPolynomial ι' S) a : MvPolynomial ι' S)
add :
  ∀ (p q : MvPolynomial ι' S)
    (hp : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p)
    (hq : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = q),
    ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p + q
⊢ ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p
have mul_X : ∀ (p : MvPolynomial ι' S) (i : ι')
  (hp : ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p),
  ∃ (a : Generators.Ring (Q.comp P)), (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) a = p * X i
Tactic: induction p using MvPolynomial.induction_on with
  | C a =>
      use MvPolynomial.rename Sum.inr (P.σ a)
      simp only [Hom.toAlgHom, ofComp, Generators.comp, MvPolynomial.aeval_rename,
        Sum.elim_comp_inr]
      simp_rw [Function.comp_def, ← MvPolynomial.algebraMap_eq, ← IsScalarTower.toAlgHom_apply R,
        ← MvPolynomial.comp_aeval]
      simp
  | add p q hp hq =>
      obtain ⟨p, rfl⟩ := hp
      obtain ⟨q, rfl⟩ := hq
      use p + q
      simp
  | mul_X p i hp =>
      obtain ⟨(p : MvPolynomial (ι' ⊕ ι) R), rfl⟩ := hp
      use p * MvPolynomial.X (R := R) (Sum.inl i)
      simp [Algebra.Generators.ofComp, Algebra.Generators.Hom.toAlgHom]
Cleared hypotheses: p
-- 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).toExtensionHom = Extension.Hom.id P.toExtension
have toRingHom : ∀ (x : P.toExtension.Ring),
  Eq (α := P.toExtension.Ring)
    ((Extension.Hom.toRingHom (Hom.id P).toExtensionHom : (a : P.toExtension.Ring) → P.toExtension.Ring) x :
      P.toExtension.Ring)
    (((Extension.Hom.id P.toExtension).toRingHom : (a : P.toExtension.Ring) → P.toExtension.Ring) x :
      P.toExtension.Ring)
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 S'
inst_16 : IsScalarTower R S S'
inst_17 : Algebra R R''
inst_18 : Algebra R S''
inst_19 : IsScalarTower R R'' S''
inst_20 : IsScalarTower R S S''
inst_21 : IsScalarTower R' R'' S''
inst_22 : IsScalarTower R' S' S''
inst_23 : IsScalarTower S S' S''
inst_24 : IsScalarTower R R' R''
inst_25 : IsScalarTower R R' S'
f : P'.Hom P''
g : P.Hom P'
⊢ Eq (α := P.toExtension.Hom P''.toExtension) (toExtensionHom (f.comp g))
    (Extension.Hom.comp f.toExtensionHom g.toExtensionHom)
have toRingHom : ∀ (x : P.toExtension.Ring),
  Eq (α := P''.toExtension.Ring)
    ((Extension.Hom.toRingHom (toExtensionHom (f.comp g)) : (a : P.toExtension.Ring) → P''.toExtension.Ring) x :
      P''.toExtension.Ring)
    ((Extension.Hom.toRingHom (Extension.Hom.comp f.toExtensionHom g.toExtensionHom) :
          (a : P.toExtension.Ring) → P''.toExtension.Ring)
        x :
      P''.toExtension.Ring)
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 ι
⊢ P.ker = RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val)
have simp : Eq (α := Ideal P.Ring) (RingHom.ker (F := P.Ring →+* S) (↑(aeval P.val) : MvPolynomial ι R →+* S))
  (RingHom.ker (F := MvPolynomial ι R →ₐ[R] S) (aeval P.val))
Tactic: simp only [ker, Extension.ker, toExtension_Ring, algebraMap_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
P : Generators R S ι
x : P.Ring
hx : x ∈ P.ker
⊢ Eq.{v + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) (0 : S)
have rwa : Eq.{v + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) x : S) (0 : S)
Tactic: rwa [← algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_8
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective (α := MvPolynomial I R) (β := S) (⇑f : (a : MvPolynomial I R) → S)
⊢ (ofAlgHom f h).ker = RingHom.ker f.toRingHom
have change : Eq (α := Ideal (ofAlgHom f h).toExtension.Ring)
  (RingHom.ker (F := (ofAlgHom f h).toExtension.Ring →+* S) (algebraMap (ofAlgHom f h).toExtension.Ring S))
  (RingHom.ker f.toRingHom)
Tactic: change RingHom.ker _ = _
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_8
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective (α := MvPolynomial I R) (β := S) (⇑f : (a : MvPolynomial I R) → S)
⊢ Eq (α := Ideal (ofAlgHom f h).toExtension.Ring)
    (RingHom.ker (F := (ofAlgHom f h).toExtension.Ring →+* S) (algebraMap (ofAlgHom f h).toExtension.Ring S))
    (RingHom.ker f.toRingHom)
have e_f : algebraMap (ofAlgHom f h).toExtension.Ring S = f.toRingHom
Tactic: congr
-- 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 ι
T : Type u_8
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
⊢ (P.ofAlgEquiv e).ker = P.ker
have rw : RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (aeval (P.ofAlgEquiv e).val) = P.ker
Tactic: rw [ker_eq_ker_aeval_val, ofAlgEquiv_val, Function.comp_def, ← AlgHom.coe_coe,
    ← MvPolynomial.comp_aeval, ← AlgHom.comap_ker, ← RingHom.ker_coe_toRingHom,
    AlgHomClass.toRingHom_toAlgHom, AlgHom.ker_coe_equiv, ← RingHom.ker_eq_comap_bot,
    ← ker_eq_ker_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 ι
T : Type u_8
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
rw : RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (aeval (P.ofAlgEquiv e).val) = P.ker
⊢ (P.ofAlgEquiv e).ker = P.ker
have rw₁ : RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (aeval ((⇑e : (a : S) → T) ∘ P.val)) = P.ker
Tactic: rw [ker_eq_ker_aeval_val, ofAlgEquiv_val, Function.comp_def, ← AlgHom.coe_coe,
    ← MvPolynomial.comp_aeval, ← AlgHom.comap_ker, ← RingHom.ker_coe_toRingHom,
    AlgHomClass.toRingHom_toAlgHom, AlgHom.ker_coe_equiv, ← RingHom.ker_eq_comap_bot,
    ← ker_eq_ker_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 ι
T : Type u_8
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
rw : RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (aeval (P.ofAlgEquiv e).val) = P.ker
rw₁ : RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (aeval ((⇑e : (a : S) → T) ∘ P.val)) = P.ker
⊢ (P.ofAlgEquiv e).ker = P.ker
have rw₂ : RingHom.ker (F := MvPolynomial ι R →ₐ[R] T) (aeval fun (x : ι) ↦ (e : (a : S) → T) (P.val x)) = P.ker
Tactic: rw [ker_eq_ker_aeval_val, ofAlgEquiv_val, Function.comp_def, ← AlgHom.coe_coe,
    ← MvPolynomial.comp_aeval, ← AlgHom.comap_ker, ← RingHom.ker_coe_toRingHom,
    AlgHomClass.toRingHom_toAlgHom, AlgHom.ker_coe_equiv, ← RingHom.ker_eq_comap_bot,
    ← ker_eq_ker_aeval_val]