awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePresentation R S
x : S
⊢ ∃ (p : R[X]) (n : ℕ), x * HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n = (aeval P.x : (a : R[X]) → S) p
have obtain : ∀
  (x :
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)),
  ∃ (p : R[X]) (n : ℕ),
    HMul.hMul (α := S)
        (((P.equivRing.trans P.equivAwayAdjoinRoot).symm :
              (a : Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g)) → S)
            x :
          S)
        (HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n) =
      (aeval P.x : (a : R[X]) → S) p
Tactic: obtain ⟨x, rfl⟩ := (P.equivRing.trans P.P.equivAwayAdjoinRoot).symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePresentation R S
x : Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
⊢ ∃ (p : R[X]) (n : ℕ),
    HMul.hMul (α := S)
        (((P.equivRing.trans P.equivAwayAdjoinRoot).symm :
              (a : Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g)) → S)
            x :
          S)
        (HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n) =
      (aeval P.x : (a : R[X]) → S) p
have obtain : ∀ (p : AdjoinRoot P.f) (n : ℕ)
  (e :
    HMul.hMul (β :=
        Localization.Away (M := AdjoinRoot P.f)
          ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
        x
        ((algebraMap (AdjoinRoot P.f)
                (Localization.Away (M := AdjoinRoot P.f)
                  ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
              (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
            (↑(p,
                    Subtype.mk (p := fun (x : AdjoinRoot P.f) ↦
                      Membership.mem (γ := Submonoid (AdjoinRoot P.f))
                        (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) :
                          Submonoid (AdjoinRoot P.f))
                        x)
                      ((fun (x : ℕ) ↦
                          HPow.hPow (α := AdjoinRoot P.f)
                            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) x)
                        n)
                      sorry).2 :
              AdjoinRoot P.f) :
          Localization.Away (M := AdjoinRoot P.f)
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) =
      (algebraMap (AdjoinRoot P.f)
            (Localization.Away (M := AdjoinRoot P.f)
              ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
          (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
        (p,
            Subtype.mk (p := fun (x : AdjoinRoot P.f) ↦
              Membership.mem (γ := Submonoid (AdjoinRoot P.f))
                (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) : Submonoid (AdjoinRoot P.f))
                x)
              ((fun (x : ℕ) ↦
                  HPow.hPow (α := AdjoinRoot P.f)
                    ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) x)
                n)
              sorry).1),
  ∃ (p : R[X]) (n : ℕ),
    HMul.hMul (α := S)
        (((P.equivRing.trans P.equivAwayAdjoinRoot).symm :
              (a : Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g)) → S)
            x :
          S)
        (HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n) =
      (aeval P.x : (a : R[X]) → S) p
Tactic: obtain ⟨⟨p, ⟨_, n, rfl⟩⟩, e⟩ := IsLocalization.surj (.powers (AdjoinRoot.mk P.f P.g)) x
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) P.x : T) ((f₂ : (a : S) → T) P.x : T)
⊢ f₁ = f₂
have this : f₁.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S) = f₂.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S)
Tactic: have : f₁.comp P.equivRing.symm.toAlgHom = f₂.comp P.equivRing.symm.toAlgHom :=
    P.P.hom_ext (by simpa)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) P.x : T) ((f₂ : (a : S) → T) P.x : T)
this : f₁.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S) = f₂.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S)
⊢ f₁ = f₂
have H : ∀ (x : S), Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) x : T) ((f₂ : (a : S) → T) x : T)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) P.x : T) ((f₂ : (a : S) → T) P.x : T)
this : f₁.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S) = f₂.comp (↑P.equivRing.symm : P.Ring →ₐ[R] S)
x : S
⊢ Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) x : T) ((f₂ : (a : S) → T) x : T)
have H : ∀ (x : P.Ring),
  Eq.{u_3 + 1} (α := T) ((f₁ : (a : S) → T) ((P.equivRing.symm : (a : P.Ring) → S) x : S) : T)
    ((f₂ : (a : S) → T) ((P.equivRing.symm : (a : P.Ring) → S) x : S) : T)
Tactic: obtain ⟨x, rfl⟩ := P.equivRing.symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P_1 : StandardEtalePair R
P : StandardEtalePresentation R S
algInst : Algebra.{u_1, u_3} R (StandardEtalePair.Ring (P.map (algebraMap R T))) :=
  RingHom.toAlgebra
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (StandardEtalePair.Ring (P.map (algebraMap R T)))) (algebraMap R T))
scalarTowerInst : IsScalarTower R T (StandardEtalePair.Ring (P.map (algebraMap R T))) := ⋯
H : P.HasMap (S := StandardEtalePair.Ring (P.map (algebraMap R T))) (StandardEtalePair.X (P.map (algebraMap R T)))
f : T ⊗[R] S →ₐ[T] StandardEtalePair.Ring (P.map (algebraMap R T)) :=
  Algebra.TensorProduct.lift (Algebra.ofId T (StandardEtalePair.Ring (P.map (algebraMap R T))))
    ((P.lift (StandardEtalePair.X (P.map (algebraMap R T))) H).comp (↑P.equivRing : S →ₐ[R] P.Ring)) ⋯
⊢ f.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) =
    AlgHom.id T (StandardEtalePair.Ring (P.map (algebraMap R T)))
have H₁ : Eq (α := StandardEtalePair.Ring (P.map (algebraMap R T)))
  ((f.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) sorry) :
        (a : (P.map (algebraMap R T)).Ring) → (P.map (algebraMap R T)).Ring)
      (StandardEtalePair.X (P.map (algebraMap R T))) :
    StandardEtalePair.Ring (P.map (algebraMap R T)))
  ((AlgHom.id T (StandardEtalePair.Ring (P.map (algebraMap R T))) :
        (a : (P.map (algebraMap R T)).Ring) → (P.map (algebraMap R T)).Ring)
      (StandardEtalePair.X (P.map (algebraMap R T))) :
    StandardEtalePair.Ring (P.map (algebraMap R T)))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P_1 : StandardEtalePair R
P : StandardEtalePresentation R S
algInst : Algebra.{u_1, u_3} R (StandardEtalePair.Ring (P.map (algebraMap R T))) :=
  RingHom.toAlgebra
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (StandardEtalePair.Ring (P.map (algebraMap R T)))) (algebraMap R T))
scalarTowerInst : IsScalarTower R T (StandardEtalePair.Ring (P.map (algebraMap R T))) := ⋯
H : P.HasMap (S := StandardEtalePair.Ring (P.map (algebraMap R T))) (StandardEtalePair.X (P.map (algebraMap R T)))
f : T ⊗[R] S →ₐ[T] StandardEtalePair.Ring (P.map (algebraMap R T)) :=
  Algebra.TensorProduct.lift (Algebra.ofId T (StandardEtalePair.Ring (P.map (algebraMap R T))))
    ((P.lift (StandardEtalePair.X (P.map (algebraMap R T))) H).comp (↑P.equivRing : S →ₐ[R] P.Ring)) ⋯
⊢ Eq (α := T ⊗[R] S →ₐ[T] T ⊗[R] S)
    (AlgHom.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) f :
      T ⊗[R] S →ₐ[T] T ⊗[R] S)
    (AlgHom.id T (T ⊗[R] S) : T ⊗[R] S →ₐ[T] T ⊗[R] S)
have h : Eq (α := S →ₐ[R] T ⊗[R] S)
  (AlgHom.comp (B := T ⊗[R] S)
      (AlgHom.restrictScalars R (S := T)
        (AlgHom.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) sorry) f))
      Algebra.TensorProduct.includeRight :
    S →ₐ[R] T ⊗[R] S)
  (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] S))) Algebra.TensorProduct.includeRight :
    S →ₐ[R] T ⊗[R] S)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P_1 : StandardEtalePair R
P : StandardEtalePresentation R S
algInst : Algebra.{u_1, u_3} R (StandardEtalePair.Ring (P.map (algebraMap R T))) :=
  RingHom.toAlgebra
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (algebraMap T (StandardEtalePair.Ring (P.map (algebraMap R T)))) (algebraMap R T))
scalarTowerInst : IsScalarTower R T (StandardEtalePair.Ring (P.map (algebraMap R T))) := ⋯
H : P.HasMap (S := StandardEtalePair.Ring (P.map (algebraMap R T))) (StandardEtalePair.X (P.map (algebraMap R T)))
f : T ⊗[R] S →ₐ[T] StandardEtalePair.Ring (P.map (algebraMap R T)) :=
  Algebra.TensorProduct.lift (Algebra.ofId T (StandardEtalePair.Ring (P.map (algebraMap R T))))
    ((P.lift (StandardEtalePair.X (P.map (algebraMap R T))) H).comp (↑P.equivRing : S →ₐ[R] P.Ring)) ⋯
⊢ Eq (α := S →ₐ[R] T ⊗[R] S)
    (AlgHom.comp (B := T ⊗[R] S)
        (AlgHom.restrictScalars R (S := T)
          (AlgHom.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) ⋯) f))
        Algebra.TensorProduct.includeRight :
      S →ₐ[R] T ⊗[R] S)
    (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] S))) Algebra.TensorProduct.includeRight :
      S →ₐ[R] T ⊗[R] S)
have h : Eq (α := T ⊗[R] S)
  (((AlgHom.comp (B := T ⊗[R] S)
            (AlgHom.restrictScalars R (S := T)
              (AlgHom.comp (StandardEtalePair.lift (S := T ⊗[R] S) (P.map (algebraMap R T)) (1 ⊗ₜ[R] P.x) sorry) f))
            Algebra.TensorProduct.includeRight :
          S →ₐ[R] T ⊗[R] S) :
        (a : S) → T ⊗[R] S)
      P.x :
    T ⊗[R] S)
  ((AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] S))) Algebra.TensorProduct.includeRight :
        (a : S) → T ⊗[R] S)
      P.x :
    T ⊗[R] S)
Tactic: apply P.hom_ext
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P_1 : StandardEtalePair R
P_2 : StandardEtalePresentation R S
P : StandardEtalePair R := { f := X, monic_f := ⋯, g := 1, cond := ⋯ }
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α :=
    StandardEtalePair.Ring (R := R) { f := X, monic_f := ⋯, g := 1, cond := ⋯ }) (β := R)
    (⇑(StandardEtalePair.lift { f := X, monic_f := ⋯, g := 1, cond := ⋯ } 0 ⋯) :
      (a : { f := X, monic_f := ⋯, g := 1, cond := ⋯ }.Ring) → R)
have this : P.X = 0
Tactic: have : P.X = 0 := Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span (Set.mem_insert _ _))
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P_1 : StandardEtalePair R
P_2 : StandardEtalePresentation R S
P : StandardEtalePair R := { f := X, monic_f := ⋯, g := 1, cond := ⋯ }
this : P.X = 0
⊢ AlgHom.comp (ofId R P.Ring) (P.lift 0 ⋯) = AlgHom.id R P.Ring
have H : Eq (α := P.Ring) ((AlgHom.comp (ofId R P.Ring) (P.lift 0 sorry) : (a : P.Ring) → P.Ring) P.X : P.Ring)
  ((AlgHom.id R P.Ring : (a : P.Ring) → P.Ring) P.X : P.Ring)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardEtale R S
Sₛ : Type u_4
inst_4 : CommRing Sₛ
inst_5 : Algebra S Sₛ
inst_6 : Algebra R Sₛ
inst_7 : IsScalarTower R S Sₛ
s : S
inst_8 : IsLocalization.Away s Sₛ
⊢ IsStandardEtale R Sₛ
have have : ∀ (P : StandardEtalePresentation R S), IsStandardEtale R Sₛ
Tactic: have P : StandardEtalePresentation R S := IsStandardEtale.nonempty_standardEtalePresentation.some
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardEtale R S
Sₛ : Type u_4
inst_4 : CommRing Sₛ
inst_5 : Algebra S Sₛ
inst_6 : Algebra R Sₛ
inst_7 : IsScalarTower R S Sₛ
s : S
inst_8 : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
⊢ IsStandardEtale R Sₛ
have obtain : ∀ (p : R[X]) (n : ℕ)
  (hp : s * HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n = (aeval P.x : (a : R[X]) → S) p),
  IsStandardEtale R Sₛ
Tactic: obtain ⟨p, n, hp⟩ := P.exists_mul_aeval_x_g_pow_eq_aeval_x s
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardEtale R S
Sₛ : Type u_4
inst_4 : CommRing Sₛ
inst_5 : Algebra S Sₛ
inst_6 : Algebra R Sₛ
inst_7 : IsScalarTower R S Sₛ
s : S
inst_8 : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n = (aeval P.x : (a : R[X]) → S) p
P' : StandardEtalePair R := { f := P.f, monic_f := ⋯, g := p * P.g, cond := ⋯ }
S' : Type u_1 :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
e : S ≃ₐ[R] S' := P.equivRing.trans P.equivAwayAdjoinRoot
this :
  IsLocalization.Away
    (HMul.hMul (α := AdjoinRoot P.f) (β := AdjoinRoot P.f)
      ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p : AdjoinRoot P.f)
      ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    (Localization.Away (M := S')
      ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
          ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
        S'))
⊢ IsStandardEtale R Sₛ
have this₁ : IsLocalization.Away (R := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) (p * P.g) : AdjoinRoot P.f)
  (Localization.Away (M := S')
    ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
        ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
      S'))
Tactic: rw [← map_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardEtale R S
Sₛ : Type u_4
inst_4 : CommRing Sₛ
inst_5 : Algebra S Sₛ
inst_6 : Algebra R Sₛ
inst_7 : IsScalarTower R S Sₛ
s : S
inst_8 : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n = (aeval P.x : (a : R[X]) → S) p
P' : StandardEtalePair R := { f := P.f, monic_f := ⋯, g := p * P.g, cond := ⋯ }
S' : Type u_1 :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
e : S ≃ₐ[R] S' := P.equivRing.trans P.equivAwayAdjoinRoot
this :
  IsLocalization.Away (R := AdjoinRoot P.f)
    ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) (p * P.g) : AdjoinRoot P.f)
    (Localization.Away (M := S')
      ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
          ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
        S'))
⊢ AlgHom.comp ((↑e.symm : S' →ₐ[R] S).comp (IsScalarTower.toAlgHom R (AdjoinRoot P.f) S')) (AdjoinRoot.mkₐ P.f) =
    aeval P.x
have hX : Eq.{u_2 + 1} (α := S)
  ((AlgHom.comp ((↑e.symm : S' →ₐ[R] S).comp (IsScalarTower.toAlgHom R (AdjoinRoot P.f) S')) (AdjoinRoot.mkₐ P.f) :
        (a : R[X]) → S)
      X :
    S)
  ((aeval P.x : (a : R[X]) → S) X : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardEtale R S
Sₛ : Type u_4
inst_4 : CommRing Sₛ
inst_5 : Algebra S Sₛ
inst_6 : Algebra R Sₛ
inst_7 : IsScalarTower R S Sₛ
s : S
inst_8 : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n = (aeval P.x : (a : R[X]) → S) p
P' : StandardEtalePair R := { f := P.f, monic_f := ⋯, g := p * P.g, cond := ⋯ }
S' : Type u_1 :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
e : S ≃ₐ[R] S' := P.equivRing.trans P.equivAwayAdjoinRoot
this :
  IsLocalization.Away (R := AdjoinRoot P.f)
    ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) (p * P.g) : AdjoinRoot P.f)
    (Localization.Away (M := S')
      ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
          ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
        S'))
⊢ Eq (α := Submonoid S)
    (Submonoid.map (M := S') e.symm.toRingEquiv.toMonoidHom
      (Submonoid.powers
          ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p)) :
        Submonoid S'))
    (Submonoid.powers ((aeval P.x : (a : R[X]) → S) p))
have this₁ : AlgHom.comp ((↑e.symm : S' →ₐ[R] S).comp (IsScalarTower.toAlgHom R (AdjoinRoot P.f) S')) (AdjoinRoot.mkₐ P.f) =
  aeval P.x
Tactic: have : ((e.symm.toAlgHom.comp (IsScalarTower.toAlgHom R _ S')).comp (AdjoinRoot.mkₐ P.f)) =
      aeval P.x := by ext; simp [e, StandardEtalePair.equivAwayAdjoinRoot]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardEtale R S
Sₛ : Type u_4
inst_4 : CommRing Sₛ
inst_5 : Algebra S Sₛ
inst_6 : Algebra R Sₛ
inst_7 : IsScalarTower R S Sₛ
s : S
inst_8 : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n = (aeval P.x : (a : R[X]) → S) p
P' : StandardEtalePair R := { f := P.f, monic_f := ⋯, g := p * P.g, cond := ⋯ }
S' : Type u_1 :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
e : S ≃ₐ[R] S' := P.equivRing.trans P.equivAwayAdjoinRoot
this_1 :
  IsLocalization.Away (R := AdjoinRoot P.f)
    ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) (p * P.g) : AdjoinRoot P.f)
    (Localization.Away (M := S')
      ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
          ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
        S'))
this :
  AlgHom.comp ((↑e.symm : S' →ₐ[R] S).comp (IsScalarTower.toAlgHom R (AdjoinRoot P.f) S')) (AdjoinRoot.mkₐ P.f) =
    aeval P.x
⊢ Eq (α := Submonoid S)
    (Submonoid.map (M := S') e.symm.toRingEquiv.toMonoidHom
      (Submonoid.powers
          ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p)) :
        Submonoid S'))
    (Submonoid.powers ((aeval P.x : (a : R[X]) → S) p))
have rw : Eq.{u_2 + 1} (α := Submonoid S)
  (Submonoid.powers
      ((e.symm.toRingEquiv.toMonoidHom : (a : S') → S)
        ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
          S')) :
    Submonoid S)
  (Submonoid.powers ((aeval P.x : (a : R[X]) → S) p) : Submonoid S)
Tactic: rw [Submonoid.map_powers]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardEtale R S
Sₛ : Type u_4
inst_4 : CommRing Sₛ
inst_5 : Algebra S Sₛ
inst_6 : Algebra R Sₛ
inst_7 : IsScalarTower R S Sₛ
s : S
inst_8 : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n = (aeval P.x : (a : R[X]) → S) p
P' : StandardEtalePair R := { f := P.f, monic_f := ⋯, g := p * P.g, cond := ⋯ }
S' : Type u_1 :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
e : S ≃ₐ[R] S' := P.equivRing.trans P.equivAwayAdjoinRoot
this :
  IsLocalization.Away (R := AdjoinRoot P.f)
    ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) (p * P.g) : AdjoinRoot P.f)
    (Localization.Away (M := S')
      ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
          ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
        S'))
⊢ IsStandardEtale R Sₛ
have H : Eq (α := Submonoid S)
  (Submonoid.map (M := S') e.symm.toRingEquiv.toMonoidHom
    (Submonoid.powers
        ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
          ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p)) :
      Submonoid S'))
  (Submonoid.powers ((aeval P.x : (a : R[X]) → S) p))
Tactic: have H : Submonoid.map e.symm.toRingEquiv.toMonoidHom (.powers
      (algebraMap _ S' (AdjoinRoot.mk P.f p))) = .powers (aeval P.x p) := by
    have : ((e.symm.toAlgHom.comp (IsScalarTower.toAlgHom R _ S')).comp (AdjoinRoot.mkₐ P.f)) =
      aeval P.x := by ext; simp [e, StandardEtalePair.equivAwayAdjoinRoot]
    rw [Submonoid.map_powers]
    exact congr(Submonoid.powers ($this p))
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardEtale R S
Sₛ : Type u_4
inst_4 : CommRing Sₛ
inst_5 : Algebra S Sₛ
inst_6 : Algebra R Sₛ
inst_7 : IsScalarTower R S Sₛ
s : S
inst_8 : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n = (aeval P.x : (a : R[X]) → S) p
P' : StandardEtalePair R := { f := P.f, monic_f := ⋯, g := p * P.g, cond := ⋯ }
S' : Type u_1 :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
e : S ≃ₐ[R] S' := P.equivRing.trans P.equivAwayAdjoinRoot
this :
  IsLocalization.Away (R := AdjoinRoot P.f)
    ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) (p * P.g) : AdjoinRoot P.f)
    (Localization.Away (M := S')
      ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
          ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
        S'))
H :
  Eq (α := Submonoid S)
    (Submonoid.map (M := S') e.symm.toRingEquiv.toMonoidHom
      (Submonoid.powers
          ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p)) :
        Submonoid S'))
    (Submonoid.powers ((aeval P.x : (a : R[X]) → S) p))
⊢ IsStandardEtale R Sₛ
have this₁ : IsLocalization.Away.{u_2, u_4} (R := S) ((aeval P.x : (a : R[X]) → S) p : S) Sₛ
Tactic: have : IsLocalization.Away (aeval P.x p) Sₛ :=
    IsLocalization.Away.of_associated (r := s) ⟨(P.hasMap.2.pow n).unit, hp⟩