mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : ↑Γ(X, ↑U)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst✝³ : Algebra ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op U)) := (CommRingCat.Hom.hom αU).toAlgebra
algInst✝² : Algebra ↑Γ(X, X.basicOpen f) ↑(F.obj (Opposite.op (U.basicOpen f))) := (CommRingCat.Hom.hom αUf).toAlgebra
algInst✝¹ : Algebra ↑(F.obj (Opposite.op U)) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst✝ : Algebra ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst✝ : IsScalarTower ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op U)) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op (U.basicOpen f)))))
this✝ : IsScalarTower ↑Γ(X, U.toOpens) ↑Γ(X, X.basicOpen f) ↑(F.obj (Opposite.op (U.basicOpen f)))
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ Algebra.IsPushout ↑(X.presheaf.1 (Opposite.op ↑U)) ↑(X.presheaf.1 (Opposite.op (X.basicOpen f)))
      ↑(F.1 (Opposite.op U)) ↑(F.1 (Opposite.op (U.basicOpen f))) ↔
    IsLocalization.Away ((ConcreteCategory.hom αU) f) ↑(F.obj (Opposite.op (U.basicOpen f)))

Tactic:
rw [Algebra.IsPushout.comm]

Goal state after:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : ↑Γ(X, ↑U)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst✝³ : Algebra ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op U)) := (CommRingCat.Hom.hom αU).toAlgebra
algInst✝² : Algebra ↑Γ(X, X.basicOpen f) ↑(F.obj (Opposite.op (U.basicOpen f))) := (CommRingCat.Hom.hom αUf).toAlgebra
algInst✝¹ : Algebra ↑(F.obj (Opposite.op U)) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst✝ : Algebra ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst✝ : IsScalarTower ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op U)) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op (U.basicOpen f)))))
this✝ : IsScalarTower ↑Γ(X, U.toOpens) ↑Γ(X, X.basicOpen f) ↑(F.obj (Opposite.op (U.basicOpen f)))
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ Algebra.IsPushout ↑(X.presheaf.1 (Opposite.op ↑U)) ↑(F.1 (Opposite.op U))
      ↑(X.presheaf.1 (Opposite.op (X.basicOpen f))) ↑(F.1 (Opposite.op (U.basicOpen f))) ↔
    IsLocalization.Away ((ConcreteCategory.hom αU) f) ↑(F.obj (Opposite.op (U.basicOpen f)))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)).QuasiFinite
algInst✝ : Algebra ↑(X.presheaf.obj (Opposite.op V)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).toAlgebra
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hxV⟩)) (hV.primeIdealOf ⟨x, hxV⟩).asIdeal
e : ↑(X.presheaf.stalk ↑⟨x, hxV⟩) ≃ₐ[↑Γ(X, V)] Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal :=
  IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hxV⟩).asIdeal.primeCompl (↑(X.presheaf.stalk ↑⟨x, hxV⟩))
    (Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal)
⊢ ((↑↑e).comp (algebraMap ↑Γ(X, V) ↑(X.presheaf.stalk ↑⟨x, hxV⟩))).comp (algebraMap ↑Γ(Y, U) ↑Γ(X, V)) =
    (e.toRingEquiv.toRingHom.comp (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))).comp
      (CommRingCat.Hom.hom (appLE f U V ⋯))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f✝ : X ⟶ Y
inst✝² : LocallyQuasiFinite f✝
x : ↥X
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
x✝¹ : J.IsPrime
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.QuasiFinite R S
x✝ : R
⊢ (algebraMap S (Localization.AtPrime J)) (f x✝) = (algebraMap R (Localization.AtPrime J)) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
r : R
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) ((algebraMap R K[X]) r) }.toFractionRing =
    (algebraMap R (FractionRing K[X])) r

Tactic:
rfl

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
x : R
⊢ (algebraMap R K⟮X⟯) x = RatFunc.mk ((algebraMap R K[X]) x) 1

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case e'_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this✝ :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy : (Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x) = f ((pullback.fst f (Y.affineCover.f i)) x)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
H : ⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x} = ⇑(pullback.fst f ι) ⁻¹' ⇑f ⁻¹' {f ((pullback.fst f ι) x)}
f' : ↑(⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x}) → ↑(⇑f ⁻¹' {f ((pullback.fst f ι) x)}) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι)) (⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x})
    (⇑f ⁻¹' {f ((pullback.fst f ι) x)}) ⋯
this : Topology.IsOpenEmbedding f'
⊢ IsOpen {⟨(pullback.fst f (Y.affineCover.f i)) x, ⋯⟩} ↔ IsOpen (f' '' {⟨x, ⋯⟩})

Tactic:
Set.image_singleton

Goal state after:
case e'_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this✝ :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy : (Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x) = f ((pullback.fst f (Y.affineCover.f i)) x)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
H : ⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x} = ⇑(pullback.fst f ι) ⁻¹' ⇑f ⁻¹' {f ((pullback.fst f ι) x)}
f' : ↑(⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x}) → ↑(⇑f ⁻¹' {f ((pullback.fst f ι) x)}) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι)) (⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x})
    (⇑f ⁻¹' {f ((pullback.fst f ι) x)}) ⋯
this : Topology.IsOpenEmbedding f'
⊢ IsOpen {⟨(pullback.fst f (Y.affineCover.f i)) x, ⋯⟩} ↔ IsOpen {f' ⟨x, ⋯⟩}
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case e'_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this✝ :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy : (Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x) = f ((pullback.fst f (Y.affineCover.f i)) x)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
H : ⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x} = ⇑(pullback.fst f ι) ⁻¹' ⇑f ⁻¹' {f ((pullback.fst f ι) x)}
f' : ↑(⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x}) → ↑(⇑f ⁻¹' {f ((pullback.fst f ι) x)}) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι)) (⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x})
    (⇑f ⁻¹' {f ((pullback.fst f ι) x)}) ⋯
this : Topology.IsOpenEmbedding f'
⊢ IsOpen {⟨(pullback.fst f (Y.affineCover.f i)) x, ⋯⟩} ↔ IsOpen {f' ⟨x, ⋯⟩}

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case e'_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X : Scheme} {x : ↥X} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∃ S, X = Spec S) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := X.affineCover.f i
⊢ IsOpen {⟨(X.affineCover.f i) x, ⋯⟩} ↔ IsOpen ((⇑f ⁻¹' {f (ι x)}).restrictPreimage ⇑ι '' {⟨x, ⋯⟩})

Tactic:
Set.image_singleton

Goal state after:
case e'_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X : Scheme} {x : ↥X} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∃ S, X = Spec S) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := X.affineCover.f i
⊢ IsOpen {⟨(X.affineCover.f i) x, ⋯⟩} ↔ IsOpen {(⇑f ⁻¹' {f (ι x)}).restrictPreimage ⇑ι ⟨x, ⋯⟩}
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case e'_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X : Scheme} {x : ↥X} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∃ S, X = Spec S) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := X.affineCover.f i
⊢ IsOpen {⟨(X.affineCover.f i) x, ⋯⟩} ↔ IsOpen {(⇑f ⁻¹' {f (ι x)}).restrictPreimage ⇑ι ⟨x, ⋯⟩}

Tactic:
rfl

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 : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ ((aeval x) P.f * -b) ^ 2 = 0

Tactic:
grind

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ (aeval x) P.f + (aeval x) (derivative P.f) * ((aeval x) P.f * -b) = 0

Tactic:
grind

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

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝¹ : (aeval x) P.f ^ 2 = 0
this✝ : (aeval x) P.f * ε = 0
ε' : S
hε'I : ε' ∈ I
hε' : (aeval x) P.f + (aeval x) (derivative P.f) * ε' = 0
hε'' : IsUnit ((aeval (x + ε')) P.g)
this : ε * ε' = 0
⊢ ε' = (aeval x) P.f * -b

Tactic:
grind

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.span {↑(Bivariate.equivMvPolynomial R) (C P.f), ↑(Bivariate.equivMvPolynomial R) (Y * C P.g - 1)}

Tactic:
rfl

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

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

Tactic:
rfl

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
inst✝¹ : IsStandardEtale R S
inst✝ : Etale R T
f : S →ₐ[R] T
hf : Function.Surjective ⇑f
⊢ IsStandardEtale R T

Tactic:
by
  let := f.toAlgebra
  have : IsScalarTower R S T := .of_algebraMap_eq' f.comp_algebraMap.symm
  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)))
  have := IsLocalization.away_of_isIdempotentElem he.one_sub (hfe.trans (by simp)) hf
  exact .of_isLocalizationAway (1 - e)

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

Goal state before:
pp: case hb
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
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
x : ↥(integralClosure R B)
⊢ (algebraMap B (S ⊗[R] B)) ↑x = ↑((algebraMap ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))) x)

Tactic:
rfl

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
w : P.ResidueField[X]
hw : (mapRingHom (algebraMap R P.ResidueField)) (minpoly R x) = Polynomial.map (algebraMap R P.ResidueField) p * w
⊢ ¬m ∣ 1 + w * Polynomial.map (algebraMap R P.ResidueField) (minpoly R x) ^ (p.natDegree + 1)

Tactic:
rw [dvd_add_left (dvd_mul_of_dvd_right (dvd_pow (by simp [m, minpoly.dvd_iff]) (by simp)) _),
        ← isUnit_iff_dvd_one]

Goal state after:
case refine_2
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
w : P.ResidueField[X]
hw : (mapRingHom (algebraMap R P.ResidueField)) (minpoly R x) = Polynomial.map (algebraMap R P.ResidueField) p * w
⊢ ¬IsUnit m
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[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
⊢ f.natDegree ≠ 0

Tactic:
rw [ne_eq, hf.natDegree_eq_zero]

Goal state after:
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[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
⊢ ¬f = 1
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✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e✝ : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e✝.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e✝.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
this✝ : Module.Finite R (AdjoinRoot 𝓟.f)
e : AdjoinRoot 𝓟.f →ₐ[R] AdjoinRoot 𝓟'.f := AdjoinRoot.mapAlgHom (Algebra.ofId R B) 𝓟.f 𝓟'.f ⋯
this : (AdjoinRoot.mk 𝓟'.f).comp (mapRingHom (algebraMap R B)) = e.comp (AdjoinRoot.mk 𝓟.f)
⊢ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g = e ((AdjoinRoot.mk 𝓟.f) 𝓟.g)

Tactic:
exact congr($this 𝓟.g)

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✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hfg : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
g : R[X]
⊢ (aeval (1 ⊗ₜ[R] 𝓟.x)) g = (aeval 𝓟'.x) g

Tactic:
rfl

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
this✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'
ht : (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
p : Ideal R := Ideal.under R Q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
⊢ (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] ≤
    (IsScalarTower.toAlgHom p.ResidueField (Ideal.under (↥R[t]) Q).ResidueField Q.ResidueField).range

Tactic:
refine adjoin_singleton_le ?_

Goal state after:
case refine_2
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
this✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'
ht : (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
p : Ideal R := Ideal.under R Q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
⊢ (algebraMap S Q.ResidueField) t ∈
    (IsScalarTower.toAlgHom p.ResidueField (Ideal.under (↥R[t]) Q).ResidueField Q.ResidueField).range
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case h
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
this✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'
ht : (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
p : Ideal R := Ideal.under R Q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
⊢ (algebraMap (↥R[t]) Q.ResidueField) ⟨t, ⋯⟩ = (algebraMap S Q.ResidueField) t

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this✝ : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra (↥R') L := adjoin ↥R' ↑(algebraMap S L).range
f : S →ₐ[R] ↥S' := (IsScalarTower.toAlgHom R S L).codRestrict (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
y : S
⊢ ↑(f y) = (algebraMap S L) y

Tactic:
rfl

Goal state after: