awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
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)))
⊢ (↑(cotangentCompLocalizationAwayEquiv g P hx).symm :
        T ⊗[S] P.toExtension.Cotangent × (localizationAway T g).toExtension.Cotangent →ₗ[T]
          ((localizationAway T g).comp P).toExtension.Cotangent) ∘ₗ
      LinearMap.inl T (T ⊗[S] P.toExtension.Cotangent) (Extension.Cotangent (toExtension (localizationAway T g))) =
    LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (toComp (localizationAway T g) P)))

Tactic:
((Cotangent.exact (localizationAway g (S := T)) P).splitSurjectiveEquiv
    (liftBaseChange_injective_of_isLocalizationAway _ P)
    ⟨cotangentCompAwaySec g P x,
      map_comp_cotangentCompAwaySec g P hx⟩).2.left.symm

Premises used: Algebra.Generators.cotangentCompAwaySec, Algebra.Generators.liftBaseChange_injective_of_isLocalizationAway, Set.Mem, Algebra.Generators.cotangentCompLocalizationAwayEquiv, Algebra.Generators.map_comp_cotangentCompAwaySec, Algebra.Generators.Cotangent.exact, Subtype.mk, And.left, Eq.symm, Function.Exact.splitSurjectiveEquiv, DFunLike.coe, Subtype.property, Algebra.Generators.localizationAway
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
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)))
a : T ⊗[S] P.toExtension.Cotangent
⊢ Eq (α := Extension.Cotangent (toExtension (comp (localizationAway T g) P)))
    (((cotangentCompLocalizationAwayEquiv g P hx).symm :
          (a : T ⊗[S] P.toExtension.Cotangent × (localizationAway T g).toExtension.Cotangent) →
            ((localizationAway T g).comp P).toExtension.Cotangent)
        (a, 0) :
      Extension.Cotangent (toExtension (comp (localizationAway T g) P)))
    ((LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (toComp (localizationAway T g) P))) :
          (a : T ⊗[S] P.toExtension.Cotangent) → ((localizationAway T g).comp P).toExtension.Cotangent)
        a :
      Extension.Cotangent (toExtension (comp (localizationAway T g) P)))

Tactic:
simp [← cotangentCompLocalizationAwayEquiv_symm_comp_inl g P hx]

Premises used: Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_comp_inl
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
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)))
⊢ LinearMap.snd T (T ⊗[S] P.toExtension.Cotangent) (Extension.Cotangent (toExtension (localizationAway T g))) ∘ₗ
      (↑(cotangentCompLocalizationAwayEquiv g P hx) :
        ((localizationAway T g).comp P).toExtension.Cotangent →ₗ[T]
          T ⊗[S] P.toExtension.Cotangent × (localizationAway T g).toExtension.Cotangent) =
    Extension.Cotangent.map (Hom.toExtensionHom (ofComp (localizationAway T g) P))

Tactic:
((Cotangent.exact (localizationAway T g) P).splitSurjectiveEquiv
    (liftBaseChange_injective_of_isLocalizationAway _ P)
    ⟨cotangentCompAwaySec g P x, map_comp_cotangentCompAwaySec g P hx⟩).2.right.symm

Premises used: Algebra.Generators.cotangentCompAwaySec, Algebra.Generators.liftBaseChange_injective_of_isLocalizationAway, Set.Mem, Algebra.Generators.map_comp_cotangentCompAwaySec, Algebra.Generators.Cotangent.exact, Subtype.mk, And.right, Eq.symm, Function.Exact.splitSurjectiveEquiv, DFunLike.coe, Subtype.property, Algebra.Generators.localizationAway
-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
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)))
a : Extension.Cotangent (toExtension (comp (localizationAway T g) P))
⊢ Eq.{u_2 + 1} (α := Extension.Cotangent (toExtension (localizationAway T g)))
    (((cotangentCompLocalizationAwayEquiv g P hx :
            (a : ((localizationAway T g).comp P).toExtension.Cotangent) →
              T ⊗[S] P.toExtension.Cotangent × (localizationAway T g).toExtension.Cotangent)
          a).2 :
      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)
        a :
      Extension.Cotangent (toExtension (localizationAway T g)))

Tactic:
simp [← snd_comp_cotangentCompLocalizationAwayEquiv g P hx]

Premises used: Algebra.Generators.snd_comp_cotangentCompLocalizationAwayEquiv
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
s : S
⊢ (aeval P.val : (a : MvPolynomial ι R) → S) (P.σ s) = s

Tactic:
P.aeval_val_σ' s

Premises used: Algebra.Generators.aeval_val_σ', Algebra.Generators.σ
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
⊢ IsScalarTower R₀ P.Ring S

Tactic:
IsScalarTower.of_algebraMap_eq' <|
  P.algebraMap_eq ▸ ((aeval (R := R) P.val).comp_algebraMap_of_tower R₀).symm

Premises used: MvPolynomial.aeval, Algebra.Generators.algebraMap_eq, Eq.rec, AlgHom.comp_algebraMap_of_tower, IsScalarTower.of_algebraMap_eq', Algebra.Generators.val, Eq.symm
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
x : P.Ring
⊢ Eq.{v + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) x : S)
    ((aeval P.val : (a : MvPolynomial ι R) → S) x : S)

Tactic:
simp [algebraMap_eq]

Premises used: Algebra.Generators.algebraMap_eq
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
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
rw₂ rw₃ : x * y = x * y
⊢ P.σ x • y = x * y

Tactic:
rw [Algebra.smul_def, algebraMap_apply, aeval_val_σ]

Premises used: Algebra.Generators.algebraMap_apply, Algebra.Generators.aeval_val_σ, Algebra.smul_def
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
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)
rw₂ 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)
⊢ x = y

Tactic:
rw [← P.aeval_val_σ x, ← P.aeval_val_σ y, e]

Premises used: Algebra.Generators.aeval_val_σ
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
x : S
⊢ (aeval P.val : (a : MvPolynomial ι R) → S) (P.σ x) = x

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
⊢ Function.Surjective (α := P.Ring) (β := S) (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)

Tactic:
(⟨_, P.algebraMap_apply _ ▸ P.aeval_val_σ ·⟩)

Premises used: Exists.intro, Function.Surjective
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
s : S
h₁ :
  (aeval PEmpty.elim : (a : MvPolynomial PEmpty.{w + 1} R) → S)
      ((C : (a : R) → MvPolynomial PEmpty.{w + 1} R)
          (⋯.choose (p := fun (a : R) ↦ (algebraMap R S : (a : R) → S) a = s)) :
        MvPolynomial PEmpty.{w + 1} R) =
    s
⊢ ∃ (a : MvPolynomial PEmpty.{w + 1} R), (aeval PEmpty.elim : (a : MvPolynomial PEmpty.{w + 1} R) → S) a = s

Tactic:
use C (h s).choose

Premises used: Exists.choose, MvPolynomial.C, DFunLike.coe
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
h : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
s : S
⊢ (aeval PEmpty.elim : (a : MvPolynomial PEmpty.{w + 1} R) → S)
      ((C : (a : R) → MvPolynomial PEmpty.{w + 1} R)
          (⋯.choose (p := fun (a : R) ↦ (algebraMap R S : (a : R) → S) a = s)) :
        MvPolynomial PEmpty.{w + 1} R) =
    s

Tactic:
simp [(h s).choose_spec]

Premises used: Exists.choose_spec
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
rw : Function.Surjective (α := R) (β := R) (⇑(RingHom.id R) : (a : R) → R)
⊢ Function.Surjective (α := R) (β := R) (⇑(algebraMap R R) : (a : R) → R)

Tactic:
rw [algebraMap_self]

Premises used: Algebra.algebraMap_self
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
⊢ Function.Surjective (α := R) (β := R) (⇑(RingHom.id R) : (a : R) → R)

Tactic:
RingHomSurjective.is_surjective

Premises used: RingHomSurjective.is_surjective
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
⊢ Function.Surjective (α := R) (β := R) (⇑(RingHom.id R) : (a : R) → R)

Tactic:
exact RingHomSurjective.is_surjective

Premises used: RingHomSurjective.is_surjective
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
I : Type u_1
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective (α := MvPolynomial I R) (β := S) (⇑f : (a : MvPolynomial I R) → S)
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)
⊢ aeval (Function.comp (β := MvPolynomial I R) (⇑f : (a : MvPolynomial I R) → S) X) = f

Tactic:
ext
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
I : Type u_1
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective (α := MvPolynomial I R) (β := S) (⇑f : (a : MvPolynomial I R) → S)
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:
simp
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
I : Type u_1
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective (α := MvPolynomial I R) (β := S) (⇑f : (a : MvPolynomial I R) → S)
rwa rwa₁ rwa₂ rwa₃ : Function.Surjective (α := MvPolynomial I R) (β := S) (⇑f : (a : MvPolynomial I R) → S)
⊢ Function.Surjective (α := MvPolynomial I R) (β := S)
    (⇑(aeval (Function.comp (β := MvPolynomial I R) (⇑f : (a : MvPolynomial I R) → S) X)) : (a : MvPolynomial I R) → S)

Tactic:
rwa [show aeval (f ∘ X) = f by ext; simp]
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
s : Set S
hs : Eq (α := Subalgebra R S) (adjoin R s) ⊤
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)
⊢ Generators R S (↑s : Type v)

Tactic:
refine ofSurjective (Subtype.val : s → S) ?_

Premises used: Algebra.Generators.ofSurjective, Subtype.val
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
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))))
    ⊤
rwa₂ : Eq.{v + 1} (α := Subalgebra R S) (adjoin R {x : S | x ∈ s}) ⊤
rwa₃ rwa₄ rwa₅ rwa₆ : 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)

Tactic:
rwa [← AlgHom.range_eq_top, ← Algebra.adjoin_range_eq_range_aeval,
    Subtype.range_coe_subtype, Set.setOf_mem_eq]

Premises used: Subtype.range_coe_subtype, AlgHom.range_eq_top, Set.setOf_mem_eq, Algebra.adjoin_range_eq_range_aeval
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
⊢ ∀ (x : S), (algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) = x

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 P : Generators R S ι
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
t : T
rw :
  ((↑e : S →ₐ[R] T) : (a : S) → T)
      ((aeval P.val : (a : MvPolynomial ι R) → S) ((P.σ ∘ (⇑e.symm : (a : T) → S)) t) : S) =
    t
⊢ (aeval ((⇑e : (a : S) → T) ∘ P.val) : (a : MvPolynomial ι R) → T) ((P.σ ∘ (⇑e.symm : (a : T) → S)) t) = t

Tactic:
rw [Function.comp_def, ← AlgHom.coe_coe e, ← MvPolynomial.comp_aeval_apply]

Premises used: AlgHom.coe_coe, Function.comp_def, MvPolynomial.comp_aeval_apply
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 P : Generators R S ι
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
t : T
⊢ ((↑e : S →ₐ[R] T) : (a : S) → T)
      ((aeval P.val : (a : MvPolynomial ι R) → S) ((P.σ ∘ (⇑e.symm : (a : T) → S)) t) : S) =
    t

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
⊢ (P.ofAlgEquiv e).val = (⇑e : (a : S) → T) ∘ P.val

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
r : R
inst_3 : IsLocalization.Away r S
s : S
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
⊢ (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

Tactic:
rw [map_mul, algHom_C, map_pow, aeval_X]

Premises used: MvPolynomial.aeval_X, map_pow, MvPolynomial.algHom_C, map_mul
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
r : R
inst_3 : IsLocalization.Away r S
s : S
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 ⋯) ^
        (IsLocalization.Away.sec r s).2 =
    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

Tactic:
simp only [← IsLocalization.Away.sec_spec, map_pow, IsLocalization.Away.invSelf]

Premises used: IsLocalization.Away.sec_spec, map_pow, IsLocalization.Away.invSelf
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
r : R
inst_3 : IsLocalization.Away r S
s : S
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 ⋯)
          (IsLocalization.Away.sec r s).2) =
    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

Tactic:
rw [← IsLocalization.mk'_pow, one_pow, ← IsLocalization.mk'_one (M := Submonoid.powers r) S r]

Premises used: one_pow, IsLocalization.mk'_pow, IsLocalization.mk'_one
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
r : R
inst_3 : IsLocalization.Away r S
s : S
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 ⋯)
            (IsLocalization.Away.sec r s).2) =
    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

Tactic:
rw [← IsLocalization.mk'_pow, one_pow, mul_assoc, ← IsLocalization.mk'_mul]

Premises used: one_pow, IsLocalization.mk'_pow, mul_assoc, IsLocalization.mk'_mul
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
r : R
inst_3 : IsLocalization.Away r S
s : S
rw :
  s *
      IsLocalization.mk' S r
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) r ⋯) ^
        (IsLocalization.Away.sec r s).2 =
    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

Tactic:
rw [mul_one, one_mul, IsLocalization.mk'_pow]

Premises used: IsLocalization.mk'_pow, mul_one, one_mul
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
r : R
inst_3 : IsLocalization.Away r S
s : S
⊢ s *
      IsLocalization.mk' S r
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x) r ⋯) ^
        (IsLocalization.Away.sec r s).2 =
    s

Tactic:
simp