mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
A : Type u_2
S : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : IsStandardEtale R A
Sf : Type u_4
inst✝⁴ : CommRing Sf
inst✝³ : Algebra R Sf
inst✝² : Algebra S Sf
inst✝¹ : IsScalarTower R S Sf
f : S
inst✝ : IsLocalization.Away f Sf
φ : A →ₐ[R] Sf
H : Function.Surjective ⇑φ
P : StandardEtalePresentation R A := ⋯.some
⊢ Function.Surjective
    ⇑((↑(AlgEquiv.restrictScalars R (IsLocalization.algEquiv (Submonoid.powers f) (Localization.Away f) Sf)).symm).comp
        (φ.comp ↑P.equivRing.symm))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f g : S
H : HasStandardEtaleSurjectionOn R f
h : f ∣ g
⊢ HasStandardEtaleSurjectionOn R g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
⊢ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (aeval x).toRingHom) =
    RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom

Tactic:
let e : P.Fiber S ≃ₐ[P.ResidueField]
      P.ResidueField[X] ⧸ I.map (mapRingHom (algebraMap _ P.ResidueField)) :=
    Polynomial.fiberEquivQuotient (aeval (R := R) x) hx' _

Goal state after:
R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
e : P.Fiber S ≃ₐ[P.ResidueField] P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I :=
  fiberEquivQuotient (aeval x) hx' P
⊢ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (aeval x).toRingHom) =
    RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ P.Ring ≃ₐ[R] Localization.Away ((AdjoinRoot.mk P.f) P.g)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ P.Ring ≃ₐ[R] Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ Ideal.span {(Bivariate.equivMvPolynomial R) (C P.f), (Bivariate.equivMvPolynomial R) (Y * C P.g - 1)} =
    Ideal.map (↑(Bivariate.equivMvPolynomial R)) (Ideal.span {C P.f, Y * C P.g - 1})

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : StandardEtalePair R
⊢ P.equivMvPolynomialQuotient.symm
      ((Ideal.Quotient.mk
          (Ideal.span {(Bivariate.equivMvPolynomial R) (C P.f), (Bivariate.equivMvPolynomial R) (Y * C P.g - 1)}))
        (MvPolynomial.X 0)) =
    P.X

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
f : R →+* S
⊢ ∃ p₁ p₂ n, derivative (map f P.f) * p₁ + map f P.f * p₂ = map f P.g ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
P : StandardEtalePair R
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : T
H : P.HasMap x
⊢ (P.map (algebraMap R S)).HasMap x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ Function.Injective ⇑↑(P.lift P.x ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ Function.Injective ⇑↑↑P.equivMvPolynomialQuotient.symm

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B✝ : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
B : Type u_4
inst✝¹ : CommRing B
inst✝ : Algebra R B
x : S ⊗[R] ↥(integralClosure R B)
⊢ (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R B).val) x ∈ integralClosure S (S ⊗[R] B)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
⊢ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (aeval x).toRingHom) =
    RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Module.Flat R S
⊢ Function.Injective ⇑(toIntegralClosure R S B)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ Ideal.span (Set.range ![(Bivariate.equivMvPolynomial R) (C P.f), (Bivariate.equivMvPolynomial R) (Y * C P.g - 1)]) =
    (Algebra.Generators.ofAlgHom
        ((P.lift P.x ⋯).comp
          ((↑P.equivMvPolynomialQuotient.symm).comp
            (Ideal.Quotient.mkₐ R
              (Ideal.span {(Bivariate.equivMvPolynomial R) (C P.f), (Bivariate.equivMvPolynomial R) (Y * C P.g - 1)}))))
        ⋯).ker

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePresentation R S
p : R[X]
⊢ (MvPolynomial.aeval P.toPresentation.val) ((Bivariate.equivMvPolynomial R) (C p)) = (aeval P.x) p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ IsUnit { toPresentation := P.toPresentation, map := id, map_inj := ⋯ }.jacobian

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
T : Type u_4
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
H : Function.Bijective ⇑(toIntegralClosure R S B)
H' : Function.Bijective ⇑(toIntegralClosure S T (S ⊗[R] B))
⊢ Function.Bijective ⇑(toIntegralClosure R T B)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePresentation R S
⊢ P.toSubmersivePresentation.jacobian = (aeval P.x) (derivative P.f) * (aeval P.x) P.g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePresentation R S
x : S
⊢ ∃ p n, x * (aeval P.x) P.g ^ n = (aeval P.x) p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
s : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
r : ↑s
⊢ IsLocalizedModule.Away (↑r)
    (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
e : S ≃ₐ[R] T
⊢ (P.lift (e P.x) ⋯) P.X = ((↑e).comp (P.lift P.x ⋯)) P.X

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
Q' : Ideal (P.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S P) ⟨Q, ⋯⟩).asIdeal
this✝³ : Q'.LiesOver Q
this✝² : Q'.LiesOver P
this✝¹ : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver Q Q'
this✝ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver P Q'
this : IsUnramifiedAt P.ResidueField Q'
⊢ Function.Surjective ⇑(aeval (1 ⊗ₜ[R] x))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : f₁ P.x = f₂ P.x
⊢ (f₁.comp ↑P.equivRing.symm) P.X = (f₂.comp ↑P.equivRing.symm) P.X

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : f₁ P.x = f₂ P.x
⊢ f₁ = f₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
s : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
this :
  ∀ (r : ↑s),
    IsLocalizedModule.Away (↑r)
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
r : ↑s
⊢ ∀ (x : ↥(integralClosure S (S ⊗[R] B))),
    ((Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R B)).comp (integralClosure S (S ⊗[R] B)).val) x ∈
      Subalgebra.restrictScalars S (integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
algInst✝ : Algebra R (P.map (algebraMap R T)).Ring :=
  ((algebraMap T (P.map (algebraMap R T)).Ring).comp (algebraMap R T)).toAlgebra
scalarTowerInst✝ : IsScalarTower R T (P.map (algebraMap R T)).Ring :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R (P.map (algebraMap R T)).Ring))
⊢ P.HasMap (P.map (algebraMap R T)).X

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
algInst✝ : Algebra R (P.map (algebraMap R T)).Ring :=
  ((algebraMap T (P.map (algebraMap R T)).Ring).comp (algebraMap R T)).toAlgebra
scalarTowerInst✝ : IsScalarTower R T (P.map (algebraMap R T)).Ring :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R (P.map (algebraMap R T)).Ring))
H : P.HasMap (P.map (algebraMap R T)).X
f : T ⊗[R] S →ₐ[T] (P.map (algebraMap R T)).Ring :=
  Algebra.TensorProduct.lift (Algebra.ofId T (P.map (algebraMap R T)).Ring)
    ((P.lift (P.map (algebraMap R T)).X H).comp ↑P.equivRing) ⋯
⊢ f.comp ((P.map (algebraMap R T)).lift (1 ⊗ₜ[R] P.x) ⋯) = AlgHom.id T (P.map (algebraMap R T)).Ring

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
algInst✝ : Algebra R (P.map (algebraMap R T)).Ring :=
  ((algebraMap T (P.map (algebraMap R T)).Ring).comp (algebraMap R T)).toAlgebra
scalarTowerInst✝ : IsScalarTower R T (P.map (algebraMap R T)).Ring :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R (P.map (algebraMap R T)).Ring))
H : P.HasMap (P.map (algebraMap R T)).X
f : T ⊗[R] S →ₐ[T] (P.map (algebraMap R T)).Ring :=
  Algebra.TensorProduct.lift (Algebra.ofId T (P.map (algebraMap R T)).Ring)
    ((P.lift (P.map (algebraMap R T)).X H).comp ↑P.equivRing) ⋯
⊢ ((P.map (algebraMap R T)).lift (1 ⊗ₜ[R] P.x) ⋯).comp f = AlgHom.id T (T ⊗[R] S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ Function.Bijective ⇑((P.map (algebraMap R T)).lift (1 ⊗ₜ[R] P.x) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝¹ : StandardEtalePair R
P✝ : StandardEtalePresentation R S
P : StandardEtalePair R
⊢ Function.Bijective ⇑(P.lift P.X ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
s : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
this✝² :
  ∀ (r : ↑s),
    IsLocalizedModule.Away (↑r)
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
φ : (r : ↑s) → ↥(integralClosure S (S ⊗[R] B)) →ₐ[S] ↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B)) :=
  fun r ↦
    ((Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R B)).comp
          (integralClosure S (S ⊗[R] B)).val).codRestrict
      (Subalgebra.restrictScalars S (integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B))) ⋯
r : ↑s
this✝¹ : Algebra (S ⊗[R] B) (Sᵣ r ⊗[R] B) :=
  (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R B)).toAlgebra
this✝ : Algebra ↥(integralClosure S (S ⊗[R] B)) ↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B)) := (φ r).toAlgebra
this : IsScalarTower (↥(integralClosure S (S ⊗[R] B))) (↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B))) (Sᵣ r ⊗[R] B)
⊢ IsLocalization (Algebra.algebraMapSubmonoid (S ⊗[R] B) (Submonoid.powers ↑r)) (Sᵣ r ⊗[R] B)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ X.Monic

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ derivative X * 1 + X * 0 = 1 ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ (aeval 0) { f := X, monic_f := ⋯, g := 1, cond := ⋯ }.f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ IsUnit ((aeval 0) { f := X, monic_f := ⋯, g := 1, cond := ⋯ }.g)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
s : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
this :
  ∀ (r : ↑s),
    IsLocalizedModule.Away (↑r)
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
φ : (r : ↑s) → ↥(integralClosure S (S ⊗[R] B)) →ₐ[S] ↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B)) :=
  fun r ↦
    ((Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R B)).comp
          (integralClosure S (S ⊗[R] B)).val).codRestrict
      (Subalgebra.restrictScalars S (integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B))) ⋯
r : ↑s
⊢ IsLocalizedModule.Away (↑r) (φ r).toLinearMap

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝¹ : StandardEtalePair R
P✝ : StandardEtalePresentation R S
P : StandardEtalePair R := { f := X, monic_f := ⋯, g := 1, cond := ⋯ }
this : P.X = 0
⊢ (aeval 0) P.f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝¹ : StandardEtalePair R
P✝ : StandardEtalePresentation R S
P : StandardEtalePair R := { f := X, monic_f := ⋯, g := 1, cond := ⋯ }
this : P.X = 0
⊢ IsUnit ((aeval 0) P.g)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝¹ : StandardEtalePair R
P✝ : StandardEtalePresentation R S
P : StandardEtalePair R := { f := X, monic_f := ⋯, g := 1, cond := ⋯ }
this : P.X = 0
⊢ (P.lift 0 ⋯).comp (ofId R P.Ring) = AlgHom.id R R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝¹ : StandardEtalePair R
P✝ : StandardEtalePresentation R S
P : StandardEtalePair R := { f := X, monic_f := ⋯, g := 1, cond := ⋯ }
this : P.X = 0
⊢ (ofId R P.Ring).comp (P.lift 0 ⋯) = AlgHom.id R P.Ring

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ Function.Bijective ⇑({ f := X, monic_f := ⋯, g := 1, cond := ⋯ }.lift 0 ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * (aeval P.x) P.g ^ n = (aeval P.x) p
p₁ p₂ : R[X]
m : ℕ
e : derivative P.f * p₁ + P.f * p₂ = P.g ^ m
⊢ derivative P.f * (p₁ * p ^ m) + P.f * (p₂ * p ^ m) = (p * P.g) ^ m

Tactic:
linear_combination e * p ^ m

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * (aeval P.x) P.g ^ n = (aeval P.x) p
p₁ p₂ : R[X]
m : ℕ
e : derivative P.f * p₁ + P.f * p₂ = P.g ^ m
⊢ derivative P.f * (p₁ * p ^ m) + P.f * (p₂ * p ^ m) = (p * P.g) ^ m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
s : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
⊢ ¬minpoly P.ResidueField ((algebraMap S Q.ResidueField) x) ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p

Tactic:
by

Goal state after: