awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
e : S ≃ₐ[R] T
inst_5 : IsStandardEtale R S
⊢ IsStandardEtale R T

Tactic:
⟨⟨IsStandardEtale.nonempty_standardEtalePresentation.some.mapEquiv e⟩⟩

Premises used: StandardEtalePresentation.mapEquiv, Nonempty.some, Nonempty.intro, Algebra.IsStandardEtale.mk, Algebra.IsStandardEtale.nonempty_standardEtalePresentation
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
⊢ Monic.{u_1} (R := R) X

Tactic:
simp
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) X : R[X]) (1 : R[X]) + HMul.hMul (α := R[X]) X 0 =
    HPow.hPow (α := R[X]) (β := ℕ) 1 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
⊢ Eq.{u_1 + 1} (α := R)
    ((aeval 0 : (a : R[X]) → R) (StandardEtalePair.f { f := X, monic_f := ⋯, g := 1, cond := ⋯ }) : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
⊢ IsUnit.{u_1} (M := R)
    ((aeval 0 : (a : R[X]) → R) (StandardEtalePair.g { f := X, monic_f := ⋯, g := 1, cond := ⋯ }) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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 := ⋯ }
⊢ P.X = 0

Tactic:
have : P.X = 0 := Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span (Set.mem_insert _ _))
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
⊢ Eq (α := R) ((aeval 0 : (a : R[X]) → R) P.f : R) (0 : R)

Tactic:
simp [P]
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
⊢ IsUnit (M := R) ((aeval 0 : (a : R[X]) → R) P.g : R)

Tactic:
simp [P]
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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 (P.lift 0 ⋯) (ofId R P.Ring) = AlgHom.id R R

Tactic:
ext
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
H :
  Eq (α := P.Ring) ((AlgHom.comp (ofId R P.Ring) (P.lift 0 ⋯) : (a : P.Ring) → P.Ring) P.X : P.Ring)
    ((AlgHom.id R P.Ring : (a : P.Ring) → P.Ring) P.X : P.Ring)
⊢ AlgHom.comp (ofId R P.Ring) (P.lift 0 ⋯) = AlgHom.id R P.Ring

Tactic:
ext
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
⊢ Eq (α := P.Ring) ((AlgHom.comp (ofId R P.Ring) (P.lift 0 ⋯) : (a : P.Ring) → P.Ring) P.X : P.Ring)
    ((AlgHom.id R P.Ring : (a : P.Ring) → P.Ring) P.X : P.Ring)

Tactic:
simp [this]
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
e : P.Ring ≃ₐ[R] R := AlgEquiv.ofAlgHom (P.lift 0 ⋯) (ofId R P.Ring) ⋯ ⋯
⊢ 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)

Tactic:
e.bijective

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, setOf, StandardEtalePair.Ring, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, AlgEquiv.bijective
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
e : P.Ring ≃ₐ[R] R := AlgEquiv.ofAlgHom (P.lift 0 ⋯) (ofId R P.Ring) ⋯ ⋯
⊢ 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)

Tactic:
exact e.bijective

Premises used: AlgEquiv.bijective
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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ₛ
have : ∀ (P : StandardEtalePresentation R S), IsStandardEtale R Sₛ
⊢ IsStandardEtale R Sₛ

Tactic:
have P : StandardEtalePresentation R S := IsStandardEtale.nonempty_standardEtalePresentation.some
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
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ₛ
⊢ IsStandardEtale R Sₛ

Tactic:
obtain ⟨p, n, hp⟩ := P.exists_mul_aeval_x_g_pow_eq_aeval_x s

Premises used: StandardEtalePresentation.exists_mul_aeval_x_g_pow_eq_aeval_x
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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₁ p₂ : R[X]
m : ℕ
e : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) p₁ + P.f * p₂ = P.g ^ m
⊢ HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) P.f : R[X]) (p₁ * p ^ m) + P.f * (p₂ * p ^ m) = (p * P.g) ^ m

Tactic:
linear_combination e * p ^ m
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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'))
⊢ 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

Premises used: map_mul
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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'))
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)
⊢ AlgHom.comp ((↑e.symm : S' →ₐ[R] S).comp (IsScalarTower.toAlgHom R (AdjoinRoot P.f) S')) (AdjoinRoot.mkₐ P.f) =
    aeval P.x

Tactic:
ext
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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.{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:
simp [e, StandardEtalePair.equivAwayAdjoinRoot]

Premises used: StandardEtalePair.equivAwayAdjoinRoot
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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

Tactic:
have : ((e.symm.toAlgHom.comp (IsScalarTower.toAlgHom R _ S')).comp (AdjoinRoot.mkₐ P.f)) =
      aeval P.x := by ext; simp [e, StandardEtalePair.equivAwayAdjoinRoot]
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
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)
⊢ 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:
rw [Submonoid.map_powers]

Premises used: Submonoid.map_powers
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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.{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:
congr(Submonoid.powers ($this p))

Premises used: congrArg, id, Submonoid.powers, DFunLike.coe
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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.{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:
exact congr(Submonoid.powers ($this p))
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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))

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))
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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))
⊢ 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⟩
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
inst_5 : IsStandardEtale R S
inst_6 : Etale R T
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
this : Algebra S T := f.toAlgebra
⊢ IsScalarTower R S T

Tactic:
have : IsScalarTower R S T := .of_algebraMap_eq' f.comp_algebraMap.symm
-- Module: Mathlib.RingTheory.Etale.StandardEtale
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
inst_5 : IsStandardEtale R S
inst_6 : Etale R T
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
this_1 : Algebra S T := f.toAlgebra
this : IsScalarTower R S T
obtain :
  ∀ (e : S) (he : IsIdempotentElem e) (hfe : Eq (α := Ideal S) (RingHom.ker f.toRingHom) (S ∙ e)), IsStandardEtale R T
⊢ IsStandardEtale R T

Tactic:
obtain ⟨e, he, hfe⟩ :=
    (Ideal.isIdempotentElem_iff_of_fg _ (Algebra.FinitePresentation.ker_fG_of_surjective f hf)).mp
      ((Algebra.FormallyEtale.iff_of_surjective hf).mp (.of_restrictScalars (R := R)))

Premises used: Ideal.isIdempotentElem_iff_of_fg, Algebra.FinitePresentation.ker_fG_of_surjective, Algebra.FormallyEtale.of_restrictScalars, Iff.mp, Algebra.FormallyEtale.iff_of_surjective