awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.LocalizationAway (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
⊢ HPow.hPow (α := Ideal (Generators.Ring (comp (localizationAway T g) P))) (β := ℕ)
      (ker (comp (localizationAway T g) P)) 2 ≤
    RingHom.ker (F :=
      Generators.Ring (comp (localizationAway T g) P) →ₐ[R]
        Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
          ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
            P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
      (compLocalizationAwayAlgHom T g P)
have hsple : ∀ {x : Generators.Ring (comp (localizationAway T g) P)}
  (hx :
    Membership.mem (γ := Ideal (Generators.Ring (comp (localizationAway T g) P)))
      (Ideal.span
        {HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
              ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
                MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
              (X (Sum.inl ())) -
            1})
      x),
  Eq (α :=
    Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
      ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
        P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
    ((compLocalizationAwayAlgHom T g P :
          (a : ((localizationAway T g).comp P).Ring) →
            Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)))
        x :
      Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
        ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
          P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
    (0 :
      Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
        ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
          P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
Tactic: have hsple {x} (hx : x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}) :
        (compLocalizationAwayAlgHom T g P) x = 0 := by
    obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton.mp hx
    rw [map_mul, compLocalizationAwayAlgHom_relation_eq_zero, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.LocalizationAway (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : Generators.Ring (comp (localizationAway T g) P)}
    (hx :
      Membership.mem (γ := Ideal (Generators.Ring (comp (localizationAway T g) P)))
        (Ideal.span
          {HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
                  MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                (X (Sum.inl ())) -
              1})
        x),
    Eq (α :=
      Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
        ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
          P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
      ((compLocalizationAwayAlgHom T g P :
            (a : ((localizationAway T g).comp P).Ring) →
              Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)))
          x :
        Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
          ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
            P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
      (0 :
        Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
          ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
            P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
⊢ HMul.hMul (α := Ideal (Generators.Ring (comp (localizationAway T g) P)))
      (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (comp (localizationAway T g) P))
        (Hom.toAlgHom (toComp (localizationAway T g) P)) P.ker)
      (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (comp (localizationAway T g) P))
        (Hom.toAlgHom (toComp (localizationAway T g) P)) P.ker) ≤
    RingHom.ker (F :=
      Generators.Ring (comp (localizationAway T g) P) →ₐ[R]
        Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
          ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
            P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
      (compLocalizationAwayAlgHom T g P)
have a : HPow.hPow (β := ℕ) P.ker 2 ≤
  Ideal.comap (F := P.Ring →ₐ[R] Generators.Ring (comp (localizationAway T g) P))
    (Hom.toAlgHom (toComp (localizationAway T g) P))
    (RingHom.ker (F :=
      Generators.Ring (comp (localizationAway T g) P) →ₐ[R]
        Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
          ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
            P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
      (compLocalizationAwayAlgHom T g P))
Tactic: rw [← Ideal.map_mul, Ideal.map_le_iff_le_comap, ← sq]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.LocalizationAway (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
x : Extension.Cotangent (toExtension (comp (localizationAway T g) P))
⊢ (cotangentCompAwaySec g P x :
        (a : (localizationAway T g).toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)
      (cMulXSubOneCotangent T g) =
    x
have rw : (cotangentCompAwaySec g P x :
      (a : (localizationAway T g).toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)
    ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) ()) =
  x
Tactic: rw [← basisCotangentAway_apply _ (), cotangentCompAwaySec, Module.Basis.constr_basis]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.LocalizationAway (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
x : Extension.Cotangent (toExtension (comp (localizationAway T g) P))
rw :
  (cotangentCompAwaySec g P x :
        (a : (localizationAway T g).toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)
      ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) ()) =
    x
⊢ (cotangentCompAwaySec g P x :
        (a : (localizationAway T g).toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)
      (cMulXSubOneCotangent T g) =
    x
have rw₁ : ((Module.Basis.constr (basisCotangentAway T g) T :
          (a : Unit → ((localizationAway T g).comp P).toExtension.Cotangent) →
            (localizationAway T g).toExtension.Cotangent →ₗ[T] ((localizationAway T g).comp P).toExtension.Cotangent)
        fun (x_1 : Unit) ↦ x :
      (a : (localizationAway T g).toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)
    ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) ()) =
  x
Tactic: rw [← basisCotangentAway_apply _ (), cotangentCompAwaySec, Module.Basis.constr_basis]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.LocalizationAway (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
x : Extension.Cotangent (toExtension (comp (localizationAway T g) P))
rw :
  (cotangentCompAwaySec g P x :
        (a : (localizationAway T g).toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)
      ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) ()) =
    x
rw₁ :
  ((Module.Basis.constr (basisCotangentAway T g) T :
            (a : Unit → ((localizationAway T g).comp P).toExtension.Cotangent) →
              (localizationAway T g).toExtension.Cotangent →ₗ[T] ((localizationAway T g).comp P).toExtension.Cotangent)
          fun (x_1 : Unit) ↦ x :
        (a : (localizationAway T g).toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)
      ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) ()) =
    x
⊢ (cotangentCompAwaySec g P x :
        (a : (localizationAway T g).toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)
      (cMulXSubOneCotangent T g) =
    x
have rw₂ : x = x
Tactic: rw [← basisCotangentAway_apply _ (), cotangentCompAwaySec, Module.Basis.constr_basis]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.LocalizationAway (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
x : Extension.Cotangent (toExtension (comp (localizationAway T g) P))
hx :
  Eq.{u_2 + 1} (α := Extension.Cotangent (toExtension (localizationAway T g)))
    ((Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway T g) P)) :
          (a : ((localizationAway T g).comp P).toExtension.Cotangent) → (localizationAway T g).toExtension.Cotangent)
        x :
      Extension.Cotangent (toExtension (localizationAway T g)))
    (cMulXSubOneCotangent T g : Extension.Cotangent (toExtension (localizationAway T g)))
⊢ Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway T g) P)) ∘ₗ cotangentCompAwaySec g P x =
    LinearMap.id
have refine : ∀ (r : Unit),
  Eq (α := Extension.Cotangent (toExtension (localizationAway T g)))
    ((Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway T g) P)) ∘ₗ cotangentCompAwaySec g P x :
          (a : (localizationAway T g).toExtension.Cotangent) → (localizationAway T g).toExtension.Cotangent)
        ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) r) :
      Extension.Cotangent (toExtension (localizationAway T g)))
    ((LinearMap.id : (a : (localizationAway T g).toExtension.Cotangent) → (localizationAway T g).toExtension.Cotangent)
        ((basisCotangentAway T g : (a : Unit) → (localizationAway T g).toExtension.Cotangent) r) :
      Extension.Cotangent (toExtension (localizationAway T g)))
Tactic: refine (basisCotangentAway T g).ext fun r ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
x y : S
⊢ P.σ x • y = x * y
have rw : HMul.hMul (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) : S) y = x * y
Tactic: rw [Algebra.smul_def, algebraMap_apply, 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 ι
x y : S
rw : HMul.hMul (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) : S) y = x * y
⊢ P.σ x • y = x * y
have rw₁ : HMul.hMul (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ x) : S) y = x * y
Tactic: rw [Algebra.smul_def, algebraMap_apply, 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 ι
x y : S
rw : HMul.hMul (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) : S) y = x * y
rw₁ : HMul.hMul (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ x) : S) y = x * y
⊢ P.σ x • y = x * y
have rw₂ : x * y = x * y
Tactic: rw [Algebra.smul_def, algebraMap_apply, 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 ι
x y : S
e : P.σ x = P.σ y
⊢ x = y
have rw : (aeval P.val : (a : MvPolynomial ι R) → S) (P.σ x) = y
Tactic: rw [← P.aeval_val_σ x, ← P.aeval_val_σ y, e]
-- 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 y : S
e : P.σ x = P.σ y
rw : (aeval P.val : (a : MvPolynomial ι R) → S) (P.σ x) = y
⊢ x = y
have rw₁ : Eq.{v + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ x) : S)
  ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ y) : S)
Tactic: rw [← P.aeval_val_σ x, ← P.aeval_val_σ y, e]
-- 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 y : S
e : P.σ x = P.σ y
rw : (aeval P.val : (a : MvPolynomial ι R) → S) (P.σ x) = y
rw₁ :
  Eq.{v + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ x) : S)
    ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ y) : S)
⊢ x = y
have rw₂ : Eq.{v + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ y) : S)
  ((aeval P.val : (a : MvPolynomial ι R) → S) (P.σ y) : S)
Tactic: rw [← P.aeval_val_σ x, ← P.aeval_val_σ y, e]
-- 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 ι
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
s : S
⊢ ∃ (a : MvPolynomial PEmpty.{w + 1} R), (aeval PEmpty.elim : (a : MvPolynomial PEmpty.{w + 1} R) → S) a = s
have h₁ : (aeval PEmpty.elim : (a : MvPolynomial PEmpty.{w + 1} R) → S)
    ((C : (a : R) → MvPolynomial PEmpty.{w + 1} R)
        (sorry.choose (p := fun (a : R) ↦ (algebraMap R S : (a : R) → S) a = s)) :
      MvPolynomial PEmpty.{w + 1} R) =
  s
Tactic: use C (h s).choose
-- 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 ι
⊢ Function.Surjective (α := R) (β := R) (⇑(algebraMap R R) : (a : R) → R)
have rw : Function.Surjective (α := R) (β := R) (⇑(RingHom.id R) : (a : R) → R)
Tactic: rw [algebraMap_self]
-- 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 ι
I : Type u_1
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective (α := MvPolynomial I R) (β := S) (⇑f : (a : MvPolynomial I R) → S)
⊢ aeval (Function.comp (β := MvPolynomial I R) (⇑f : (a : MvPolynomial I R) → S) X) = f
have hf : ∀ (i : I),
  Eq.{v + 1} (α := S)
    ((aeval (Function.comp (β := MvPolynomial I R) (⇑f : (a : MvPolynomial I R) → S) X) : (a : MvPolynomial I R) → S)
        (X i) :
      S)
    ((f : (a : MvPolynomial I R) → S) (X i) : 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 ι
s : Set S
hs : Eq (α := Subalgebra R S) (adjoin R s) ⊤
⊢ Generators R S (↑s : Type v)
have refine : Function.Surjective (α := MvPolynomial.{v, u} (↑s : Type v) R) (β := S)
  (⇑(aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s))) : (a : MvPolynomial (↑s : Type v) R) → S)
Tactic: refine ofSurjective (Subtype.val : s → 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 : Generators R S ι
s : Set S
hs : Eq (α := Subalgebra R S) (adjoin R s) ⊤
⊢ Function.Surjective (α := MvPolynomial.{v, u} (↑s : Type v) R) (β := S)
    (⇑(aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s))) : (a : MvPolynomial (↑s : Type v) R) → S)
have rwa : Eq.{v + 1} (α := Subalgebra R S)
  (AlgHom.range (A := MvPolynomial.{v, u} (↑s : Type v) R) (aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ⊤
Tactic: rwa [← AlgHom.range_eq_top, ← Algebra.adjoin_range_eq_range_aeval,
    Subtype.range_coe_subtype, Set.setOf_mem_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 ι
s : Set S
hs : Eq (α := Subalgebra R S) (adjoin R s) ⊤
rwa :
  Eq.{v + 1} (α := Subalgebra R S)
    (AlgHom.range (A := MvPolynomial.{v, u} (↑s : Type v) R) (aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ⊤
⊢ Function.Surjective (α := MvPolynomial.{v, u} (↑s : Type v) R) (β := S)
    (⇑(aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s))) : (a : MvPolynomial (↑s : Type v) R) → S)
have rwa₁ : Eq.{v + 1} (α := Subalgebra R S) (adjoin R (Set.range (ι := (↑s : Type v)) (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ⊤
Tactic: rwa [← AlgHom.range_eq_top, ← Algebra.adjoin_range_eq_range_aeval,
    Subtype.range_coe_subtype, Set.setOf_mem_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 ι
s : Set S
hs : Eq (α := Subalgebra R S) (adjoin R s) ⊤
rwa :
  Eq.{v + 1} (α := Subalgebra R S)
    (AlgHom.range (A := MvPolynomial.{v, u} (↑s : Type v) R) (aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ⊤
rwa₁ :
  Eq.{v + 1} (α := Subalgebra R S) (adjoin R (Set.range (ι := (↑s : Type v)) (Subtype.val (p := fun (x : S) ↦ x ∈ s))))
    ⊤
⊢ Function.Surjective (α := MvPolynomial.{v, u} (↑s : Type v) R) (β := S)
    (⇑(aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s))) : (a : MvPolynomial (↑s : Type v) R) → S)
have rwa₂ : Eq.{v + 1} (α := Subalgebra R S) (adjoin R {x : S | x ∈ s}) ⊤
Tactic: rwa [← AlgHom.range_eq_top, ← Algebra.adjoin_range_eq_range_aeval,
    Subtype.range_coe_subtype, Set.setOf_mem_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_1 P : Generators R S ι
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
t : T
⊢ (aeval ((⇑e : (a : S) → T) ∘ P.val) : (a : MvPolynomial ι R) → T) ((P.σ ∘ (⇑e.symm : (a : T) → S)) t) = t
have rw : ((↑e : S →ₐ[R] T) : (a : S) → T) ((aeval P.val : (a : MvPolynomial ι R) → S) ((P.σ ∘ (⇑e.symm : (a : T) → S)) t) : S) =
  t
Tactic: rw [Function.comp_def, ← AlgHom.coe_coe e, ← MvPolynomial.comp_aeval_apply]
-- 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 : R
inst_3 : IsLocalization.Away r S
s : S
⊢ (aeval fun (x : Unit) ↦ IsLocalization.Away.invSelf r : (a : MvPolynomial Unit R) → S)
      (HMul.hMul (α := MvPolynomial Unit R)
        ((C : (a : R) → MvPolynomial Unit R) (IsLocalization.Away.sec r s).1 : MvPolynomial Unit R)
        (HPow.hPow (α := MvPolynomial Unit R) (X ()) (IsLocalization.Away.sec r s).2)) =
    s
have rw : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (IsLocalization.Away.sec r s).1 : S)
    (HPow.hPow (α := S) (IsLocalization.Away.invSelf r) (IsLocalization.Away.sec r s).2) =
  s
Tactic: rw [map_mul, algHom_C, map_pow, aeval_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 : R
inst_3 : IsLocalization.Away r S
s : S
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (IsLocalization.Away.sec r s).1 : S)
      (HPow.hPow (α := S) (IsLocalization.Away.invSelf r) (IsLocalization.Away.sec r s).2) =
    s
have simp : s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) (IsLocalization.Away.sec r s).2 *
    IsLocalization.mk' S 1
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) r sorry) ^
      (IsLocalization.Away.sec r s).2 =
  s
Tactic: simp only [← IsLocalization.Away.sec_spec, map_pow, IsLocalization.Away.invSelf]
-- 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 : R
inst_3 : IsLocalization.Away r S
s : S
⊢ s * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) (IsLocalization.Away.sec r s).2 *
      IsLocalization.mk' S 1
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) r ⋯) ^
        (IsLocalization.Away.sec r s).2 =
    s
have rw : s * IsLocalization.mk' (M := Submonoid.powers r) S r 1 ^ (IsLocalization.Away.sec r s).2 *
    IsLocalization.mk' S 1
      (HPow.hPow (α := ↥(Submonoid.powers r))
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) r sorry)
        (IsLocalization.Away.sec r s).2) =
  s
Tactic: rw [← IsLocalization.mk'_pow, one_pow, ← IsLocalization.mk'_one (M := Submonoid.powers r) S r]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
r : R
inst_3 : IsLocalization.Away r S
s : S
⊢ s * IsLocalization.mk' (M := Submonoid.powers r) S r 1 ^ (IsLocalization.Away.sec r s).2 *
      IsLocalization.mk' S 1
        (HPow.hPow (α := ↥(Submonoid.powers r))
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) r ⋯)
          (IsLocalization.Away.sec r s).2) =
    s
have rw : s *
    IsLocalization.mk' S (r ^ (IsLocalization.Away.sec r s).2 * 1)
      (1 *
        HPow.hPow (α := ↥(Submonoid.powers r))
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) r sorry)
          (IsLocalization.Away.sec r s).2) =
  s
Tactic: rw [← IsLocalization.mk'_pow, one_pow, mul_assoc, ← IsLocalization.mk'_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
r : R
inst_3 : IsLocalization.Away r S
s : S
⊢ s *
      IsLocalization.mk' S (r ^ (IsLocalization.Away.sec r s).2 * 1)
        (1 *
          HPow.hPow (α := ↥(Submonoid.powers r))
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) r ⋯)
            (IsLocalization.Away.sec r s).2) =
    s
have rw : s *
    IsLocalization.mk' S r
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) r sorry) ^
      (IsLocalization.Away.sec r s).2 =
  s
Tactic: rw [mul_one, one_mul, IsLocalization.mk'_pow]