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_1 : Generators R S ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
x : T ⊗[R] S
⊢ ∃ (a : MvPolynomial ι T),
    ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        a =
      x
have zero : ∃ (a : MvPolynomial ι T),
  Eq (α := T ⊗[R] S)
    (((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        a :
      T ⊗[R] S)
    (0 : T ⊗[R] S)
Tactic: induction x using TensorProduct.induction_on with
  | zero => exact ⟨0, map_zero _⟩
  | tmul a b =>
    let X := P.σ b
    use a • MvPolynomial.map (algebraMap R T) X
    simp only [LinearMapClass.map_smul, X, aeval_map_algebraMap]
    have : ∀ y : P.Ring,
      aeval (fun x ↦ (1 ⊗ₜ[R] P.val x : T ⊗[R] S)) y = 1 ⊗ₜ aeval (fun x ↦ P.val x) y := by
      intro y
      induction y using MvPolynomial.induction_on with
      | C a =>
        rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]
      | add p q hp hq => simp [map_add, tmul_add, hp, hq]
      | mul_X p i hp => simp [hp]
    rw [this, P.aeval_val_σ, smul_tmul', smul_eq_mul, mul_one]
  | add x y ex ey =>
    obtain ⟨a, ha⟩ := ex
    obtain ⟨b, hb⟩ := ey
    use (a + b)
    rw [map_add, ha, hb]
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 ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
x : T ⊗[R] S
zero :
  ∃ (a : MvPolynomial ι T),
    Eq (α := T ⊗[R] S)
      (((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          a :
        T ⊗[R] S)
      (0 : T ⊗[R] S)
⊢ ∃ (a : MvPolynomial ι T),
    ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        a =
      x
have tmul : ∀ (a : T) (b : S),
  ∃ (a_1 : MvPolynomial ι T),
    Eq (α := T ⊗[R] S)
      (((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          a_1 :
        T ⊗[R] S)
      (a ⊗ₜ[R] b : T ⊗[R] S)
Tactic: induction x using TensorProduct.induction_on with
  | zero => exact ⟨0, map_zero _⟩
  | tmul a b =>
    let X := P.σ b
    use a • MvPolynomial.map (algebraMap R T) X
    simp only [LinearMapClass.map_smul, X, aeval_map_algebraMap]
    have : ∀ y : P.Ring,
      aeval (fun x ↦ (1 ⊗ₜ[R] P.val x : T ⊗[R] S)) y = 1 ⊗ₜ aeval (fun x ↦ P.val x) y := by
      intro y
      induction y using MvPolynomial.induction_on with
      | C a =>
        rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]
      | add p q hp hq => simp [map_add, tmul_add, hp, hq]
      | mul_X p i hp => simp [hp]
    rw [this, P.aeval_val_σ, smul_tmul', smul_eq_mul, mul_one]
  | add x y ex ey =>
    obtain ⟨a, ha⟩ := ex
    obtain ⟨b, hb⟩ := ey
    use (a + b)
    rw [map_add, ha, hb]
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 ι
ι' : Type u_1
T_1 : Type ?u.65480
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
P : Generators R S ι
x : T ⊗[R] S
zero :
  ∃ (a : MvPolynomial ι T),
    Eq (α := T ⊗[R] S)
      (((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          a :
        T ⊗[R] S)
      (0 : T ⊗[R] S)
tmul :
  ∀ (a : T) (b : S),
    ∃ (a_1 : MvPolynomial ι T),
      Eq (α := T ⊗[R] S)
        (((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
              (a : MvPolynomial ι T) → T ⊗[R] S)
            a_1 :
          T ⊗[R] S)
        (a ⊗ₜ[R] b : T ⊗[R] S)
⊢ ∃ (a : MvPolynomial ι T),
    ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        a =
      x
have add : ∀ (x y : T ⊗[R] S)
  (ex :
    ∃ (a : MvPolynomial ι T),
      ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          a =
        x)
  (ey :
    ∃ (a : MvPolynomial ι T),
      ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
            (a : MvPolynomial ι T) → T ⊗[R] S)
          a =
        y),
  ∃ (a : MvPolynomial ι T),
    ((aeval (R := T) (S₁ := T ⊗[R] S) fun (x : ι) ↦ 1 ⊗ₜ[R] P.val x : MvPolynomial ι T →ₐ[T] T ⊗[R] S) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        a =
      x + y
Tactic: induction x using TensorProduct.induction_on with
  | zero => exact ⟨0, map_zero _⟩
  | tmul a b =>
    let X := P.σ b
    use a • MvPolynomial.map (algebraMap R T) X
    simp only [LinearMapClass.map_smul, X, aeval_map_algebraMap]
    have : ∀ y : P.Ring,
      aeval (fun x ↦ (1 ⊗ₜ[R] P.val x : T ⊗[R] S)) y = 1 ⊗ₜ aeval (fun x ↦ P.val x) y := by
      intro y
      induction y using MvPolynomial.induction_on with
      | C a =>
        rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul,
          algebraMap_eq_smul_one]
      | add p q hp hq => simp [map_add, tmul_add, hp, hq]
      | mul_X p i hp => simp [hp]
    rw [this, P.aeval_val_σ, smul_tmul', smul_eq_mul, mul_one]
  | add x y ex ey =>
    obtain ⟨a, ha⟩ := ex
    obtain ⟨b, hb⟩ := ey
    use (a + b)
    rw [map_add, ha, hb]
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 ι
ι' : Type u_1
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
⊢ Eq (α := T ⊗[R] P.Ring →ₐ[T] T ⊗[R] S)
    (AlgHom.comp (B := Generators.Ring (S := T ⊗[R] S) (baseChange T P))
        (IsScalarTower.toAlgHom T (Generators.Ring (S := T ⊗[R] S) (baseChange T P)) (T ⊗[R] S))
        (↑(algebraTensorAlgEquiv R T) : T ⊗[R] MvPolynomial ι R →ₐ[T] MvPolynomial ι T) :
      T ⊗[R] P.Ring →ₐ[T] T ⊗[R] S)
    (AlgHom.comp (B := T ⊗[R] S) (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S))
        (IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S)) :
      T ⊗[R] P.Ring →ₐ[T] T ⊗[R] S)
have h : ∀ (i : ι),
  Eq (α := T ⊗[R] S)
    ((AlgHom.comp (B := T ⊗[R] P.Ring)
            (AlgHom.restrictScalars R
              (AlgHom.comp (B := Generators.Ring (S := T ⊗[R] S) (baseChange T P))
                (IsScalarTower.toAlgHom T (Generators.Ring (S := T ⊗[R] S) (baseChange T P)) (T ⊗[R] S))
                (↑(algebraTensorAlgEquiv R T) : T ⊗[R] MvPolynomial ι R →ₐ[T] MvPolynomial ι T)))
            TensorProduct.includeRight :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (X i) :
      T ⊗[R] S)
    ((AlgHom.comp (B := T ⊗[R] P.Ring)
            (AlgHom.restrictScalars R
              (AlgHom.comp (B := T ⊗[R] S) (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S))
                (IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S))))
            TensorProduct.includeRight :
          (a : MvPolynomial ι R) → T ⊗[R] S)
        (X i) :
      T ⊗[R] S)
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 ι
ι' : Type u_1
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
⊢ Eq (α := Generators.Ring (S := T ⊗[R] S) (baseChange T P) →ₐ[T] T ⊗[R] S)
    (AlgHom.comp (B := T ⊗[R] P.Ring) (IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S))
      (↑(AlgEquiv.symm (algebraTensorAlgEquiv R T)) : MvPolynomial ι T →ₐ[T] T ⊗[R] MvPolynomial ι R))
    (AlgHom.comp (B := T ⊗[R] S) (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S))
      (IsScalarTower.toAlgHom T (Generators.Ring (S := T ⊗[R] S) (baseChange T P)) (T ⊗[R] S)))
have hf : ∀ (i : ι),
  Eq (α := T ⊗[R] S)
    ((AlgHom.comp (B := T ⊗[R] P.Ring) (IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S))
            (↑(AlgEquiv.symm (algebraTensorAlgEquiv R T)) : MvPolynomial ι T →ₐ[T] T ⊗[R] MvPolynomial ι R) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        (X i) :
      T ⊗[R] S)
    ((AlgHom.comp (B := T ⊗[R] S) (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S))
            (IsScalarTower.toAlgHom T (Generators.Ring (S := T ⊗[R] S) (baseChange T P)) (T ⊗[R] S)) :
          (a : MvPolynomial ι T) → T ⊗[R] S)
        (X i) :
      T ⊗[R] S)
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_1 : Generators R S ι
ι' : Type u_1
T : Type ?u.128304
inst_3 : CommRing T
inst_4 : Algebra R T
P : Generators R S ι
b : ι' → S
s : S
⊢ ∃ (a : MvPolynomial (ι ⊕ ι') R), (aeval (Sum.elim P.val b) : (a : MvPolynomial (ι ⊕ ι') R) → S) a = s
have h : (aeval (Sum.elim P.val b) : (a : MvPolynomial (ι ⊕ ι') R) → S)
    ((rename Sum.inl : (a : MvPolynomial ι R) → MvPolynomial (ι ⊕ ι') R) (P.σ s) : MvPolynomial (ι ⊕ ι') R) =
  s
Tactic: use rename Sum.inl (P.σ s)
-- 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 ι
ι' : Type u_1
T : Type ?u.130410
inst_3 : CommRing T
inst_4 : Algebra R T
P : Generators R S ι'
e : ι ≃ ι'
s : S
| s
have rw : ((aeval P.val : (a : MvPolynomial ι' R) → S) (P.σ s) : S)
Tactic: rw [← P.aeval_val_σ s]
-- 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 ι
ι' : Type u_1
T : Type ?u.130410
inst_3 : CommRing T
inst_4 : Algebra R T
P : Generators R S ι'
e : ι ≃ ι'
s : S
⊢ (aeval (P.val ∘ (⇑e : (a : ι) → ι')) : (a : MvPolynomial ι R) → S)
      (((⇑(rename (⇑e.symm : (a : ι') → ι)) : (a : MvPolynomial ι' R) → MvPolynomial ι R) ∘ P.σ) s) =
    s
have conv_rhs : Eq.{v + 1} (α := S)
  ((aeval (P.val ∘ (⇑e : (a : ι) → ι')) : (a : MvPolynomial ι R) → S)
      (((⇑(rename (⇑e.symm : (a : ι') → ι)) : (a : MvPolynomial ι' R) → MvPolynomial ι R) ∘ P.σ) s) :
    S)
  ((aeval P.val : (a : MvPolynomial ι' R) → S) (P.σ s) : S)
Tactic: conv_rhs => rw [← P.aeval_val_σ s]
-- 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 ι
ι' : Type u_1
T : Type ?u.130410
inst_3 : CommRing T
inst_4 : Algebra R T
P : Generators R S ι'
e : ι ≃ ι'
s : S
⊢ Eq.{v + 1} (α := S)
    ((aeval (P.val ∘ (⇑e : (a : ι) → ι')) : (a : MvPolynomial ι R) → S)
        (((⇑(rename (⇑e.symm : (a : ι') → ι)) : (a : MvPolynomial ι' R) → MvPolynomial ι R) ∘ P.σ) s) :
      S)
    ((aeval P.val : (a : MvPolynomial ι' R) → S) (P.σ s) : S)
have rw : Eq.{v + 1} (α := S)
  ((aeval P.val : (a : MvPolynomial ι' R) → S)
      ((rename (⇑e : (a : ι) → ι') : (a : MvPolynomial ι R) → MvPolynomial ι' R)
        (((⇑(rename (⇑e.symm : (a : ι') → ι)) : (a : MvPolynomial ι' R) → MvPolynomial ι R) ∘ P.σ) s)) :
    S)
  ((aeval P.val : (a : MvPolynomial ι' R) → S) (P.σ s) : S)
Tactic: rw [← MvPolynomial.aeval_rename]
-- 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 ι
ι' : Type u_1
T : Type ?u.133356
inst_3 : CommRing T
inst_4 : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s_1 : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs_1 : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s_1 x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s x) = x
x : MvPolynomial σ R ⧸ I
| x
have rw : ((aeval
        (Function.comp (β := MvPolynomial σ R)
          (⇑(Ideal.Quotient.mkₐ R I) : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) X) :
      (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
    (s x) :
  MvPolynomial σ R ⧸ I)
Tactic: rw [← hs x, ← Ideal.Quotient.mkₐ_eq_mk R, aeval_unique (Ideal.Quotient.mkₐ _ 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 : Generators R S ι
ι' : Type u_1
T : Type ?u.133356
inst_3 : CommRing T
inst_4 : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s_1 : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs_1 : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s_1 x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s x) = x
x : MvPolynomial σ R ⧸ I
⊢ (aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i) :
        (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
      (s x) =
    x
have conv_rhs : Eq (α := MvPolynomial σ R ⧸ I)
  ((aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i) :
        (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
      (s x) :
    MvPolynomial σ R ⧸ I)
  ((aeval
          (Function.comp (β := MvPolynomial σ R)
            (⇑(Ideal.Quotient.mkₐ R I) : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) X) :
        (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
      (s x) :
    MvPolynomial σ R ⧸ I)
Tactic: conv_rhs => rw [← hs x, ← Ideal.Quotient.mkₐ_eq_mk R, aeval_unique (Ideal.Quotient.mkₐ _ 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 : Generators R S ι
ι' : Type u_1
T : Type ?u.133356
inst_3 : CommRing T
inst_4 : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s_1 : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs_1 : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s_1 x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s x) = x
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial σ R ⧸ I) (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I))
    (↑(aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i)) :
      MvPolynomial σ R →+* MvPolynomial σ R ⧸ I)
have hC : ∀ (x : R),
  Eq (α := MvPolynomial σ R ⧸ I)
    ((RingHom.comp (β := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I)) C :
          (a : R) → MvPolynomial σ R ⧸ I)
        x :
      MvPolynomial σ R ⧸ I)
    ((RingHom.comp
            (↑(aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i)) :
              MvPolynomial σ R →+* MvPolynomial σ R ⧸ I)
            C :
          (a : R) → MvPolynomial σ R ⧸ I)
        x :
      MvPolynomial σ R ⧸ I)
Tactic: ext 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 ι
ι' : Type u_1
T : Type ?u.133356
inst_3 : CommRing T
inst_4 : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s_1 : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs_1 : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s_1 x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (s x) = x
hC :
  ∀ (x : R),
    Eq (α := MvPolynomial σ R ⧸ I)
      ((RingHom.comp (β := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I)) C :
            (a : R) → MvPolynomial σ R ⧸ I)
          x :
        MvPolynomial σ R ⧸ I)
      ((RingHom.comp
              (↑(aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i)) :
                MvPolynomial σ R →+* MvPolynomial σ R ⧸ I)
              C :
            (a : R) → MvPolynomial σ R ⧸ I)
          x :
        MvPolynomial σ R ⧸ I)
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial σ R ⧸ I) (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I))
    (↑(aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i)) :
      MvPolynomial σ R →+* MvPolynomial σ R ⧸ I)
have hX : ∀ (x : σ),
  Eq (α := MvPolynomial σ R ⧸ I)
    ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I) : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X x) :
      MvPolynomial σ R ⧸ I)
    (((↑(aeval fun (i : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I) (X i)) :
            MvPolynomial σ R →+* MvPolynomial σ R ⧸ I) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ I)
        (X x) :
      MvPolynomial σ R ⧸ I)
Tactic: ext x
-- 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
⊢ FiniteType R S ↔ ∃ (n : ℕ), Nonempty (Generators R S (Fin n))
have refine : ∀ (h : FiniteType R S), ∃ (n : ℕ), Nonempty (Generators R S (Fin n))
Tactic: refine ⟨fun h ↦ ?_, fun ⟨n, ⟨P⟩⟩ ↦ P.finiteType⟩
-- 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
h : FiniteType R S
⊢ ∃ (n : ℕ), Nonempty (Generators R S (Fin n))
have 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))
Tactic: obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp h
-- 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
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)
⊢ 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)
have 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)
Tactic: rwa [aeval_unique f] at hf
Cleared hypotheses: hf
-- 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'
x : P.Ring
⊢ 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')
have 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))
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
-- 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'
x : P.Ring
⊢ 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))
have 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')
Tactic: apply MvPolynomial.algHom_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 R R'
inst_7 : Algebra S S'
f : P.Hom P'
v : ι →₀ ℕ
r : R
⊢ (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 : (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)
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 ι
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)
⊢ (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) =
  HSMul.hSMul (β := P'.Ring) r (v.prod fun (x1 : ι) (x2 : ℕ) ↦ f.val x1 ^ x2)
Tactic: rw [toAlgHom, aeval_monomial, Algebra.smul_def]