mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
this : map (Ideal.Quotient.mk P) p = X ^ p.natDegree
j : ℕ
hj : j ≤ p.natDegree
a : (R ⧸ P)[X]ˣ
r : R ⧸ P
ha : map (Ideal.Quotient.mk P) q = X ^ j * C r
hr : IsUnit r
e : C r = ↑a⁻¹
⊢ j = q.natDegree

Tactic:
by
    simpa [hq.natDegree_map, hr.ne_zero] using congr(($ha).natDegree).symm

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : x ∈ Ideal.map (algebraMap R S) I
A : Subalgebra R R[X] := Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}
⊢ ∃ p, p.Monic ∧ (aeval x) p = 0 ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)

Tactic:
let := Polynomial.algebra R S

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : x ∈ Ideal.map (algebraMap R S) I
A : Subalgebra R R[X] := Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}
this : Algebra R[X] S[X] := algebra R S
⊢ ∃ p, p.Monic ∧ (aeval x) p = 0 ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
z : S
hz : z ∈ R[x]
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
this : z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I) ↔ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥R[x]) I
a : ↥R[x]
ha : a ∈ ↑(Ideal.map (algebraMap R ↥R[x]) I) ∧ (algebraMap (↥R[x]) S) a = (algebraMap R S) p * z
⊢ (algebraMap (↥R[x]) S) (a + (algebraMap R ↥R[x]) q * ⟨z, hz⟩) = (algebraMap R S) p * z + (algebraMap R S) q * z

Tactic:
by
          simp only [ha.right, map_add, map_mul, add_right_inj]; rfl

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
⊢ C p.leadingCoeff ∈ completeIntegralClosure R[X] S[X]

Tactic:
obtain ⟨r, hr, hr'⟩ := H hp

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • p.leadingCoeff ^ n ∈ (algebraMap R S).range
⊢ C p.leadingCoeff ∈ completeIntegralClosure R[X] S[X]
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) (∑ v ∈ f.support, (monomial v) (coeff v f))

Tactic:
monomial_eq

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) (∑ x ∈ f.support, C (coeff x f) * x.prod fun n e ↦ X n ^ e)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
⊢ (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f → ∀ (n : β →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
H

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f
⊢ ∀ (n : β →₀ ℕ), IsIntegral R (coeff n f)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
⊢ (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f →
    ∀ (n : PEmpty.{w + 1} →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
H

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
⊢ ∀ (n : PEmpty.{w + 1} →₀ ℕ), IsIntegral R (coeff n f)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
⊢ (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f →
    ∀ (n : Option α →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
H

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
H : (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f
⊢ ∀ (n : Option α →₀ ℕ), IsIntegral R (coeff n f)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e :
  p * (algebraMap (R ⧸ P)[X] P.ResidueField[X]) ↑(⟨(mapRingHom (algebraMap R (R ⧸ P))) r, hr⟩, s).2 =
    (algebraMap (R ⧸ P)[X] P.ResidueField[X]) ↑(⟨(mapRingHom (algebraMap R (R ⧸ P))) r, hr⟩, s).1
⊢ ∃ p ∈ I, Ideal.span {map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I

Tactic:
simp only [algebraMap_def, coe_mapRingHom,
    Polynomial.map_map, ← IsScalarTower.algebraMap_eq] at e

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e : p * map (algebraMap (R ⧸ P) P.ResidueField) ↑s = map (algebraMap R P.ResidueField) r
⊢ ∃ p ∈ I, Ideal.span {map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
⊢ U.presieveOfSections s = Presieve.ofArrows (fun i ↦ U.basicOpen ↑i) fun i ↦ homOfLE ⋯

Tactic:
refine funext₂ fun ⟨V, hV⟩ ⟨f, hf⟩ ↦ eq_iff_iff.mpr ⟨?_, ?_⟩
  · rintro ⟨f, hfs, rfl⟩
    exact .mk (ι := s) ⟨f, hfs⟩
  · rintro ⟨⟨f, hfs⟩⟩
    exact ⟨f, hfs, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case mpr
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
V : X.Opens
hV : IsAffineOpen V
f : ⟨V, hV⟩ ⟶ U
⊢ (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨V, hV⟩) → (Sieve.generate (U.presieveOfSections s)).arrows f

Tactic:
rintro ⟨f₁, hf₁s, f₂, rfl⟩
    refine ⟨U.basicOpen f₁, ⟨f₂ |_ _, ?_⟩, ⟨f₁, rfl⟩, ⟨f₁, hf₁s, rfl⟩, rfl⟩
    exact (X.basicOpen_res _ _).trans (X.basicOpen_mul _ _).symm

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
⊢ (Localization.localRingHom (Ideal.comap f J) J f ⋯).QuasiFinite

Tactic:
refine .of_comp (g := algebraMap R _) ?_

Goal state after:
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
⊢ ((Localization.localRingHom (Ideal.comap f J) J f ⋯).comp
      (algebraMap R (Localization.AtPrime (Ideal.comap f J)))).QuasiFinite
Module: Mathlib.RingTheory.Etale.StandardEtale

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

Tactic:
simp [StandardEtalePair.Ring, StandardEtalePair.X]

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
f g : P.Ring →ₐ[R] S
H✝ : f P.X = g P.X
H :
  (f.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom =
    (g.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom
⊢ (aeval P.X) X = ((Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom) X

Tactic:
simp [StandardEtalePair.Ring, StandardEtalePair.X]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
h : x.num = 0
⊢ x = 0

Tactic:
← num_div_denom x,

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
h : x.num = 0
⊢ (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom = 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
| x * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p

Tactic:
rw [← num_div_denom x]

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
| (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
| x + y

Tactic:
← num_div_denom x,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
| (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom + y
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
| x * y

Tactic:
← num_div_denom x,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
| (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom * y
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hq : q ≠ 0
⊢ (∃ p, x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) → x.denom ∣ q

Tactic:
rintro ⟨p, rfl⟩
    exact denom_div_dvd p q

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
M : Submonoid R
inst✝ : IsLocalization M S
x✝ : ↥(integralClosure R B)
x : B
hx : x ∈ integralClosure R B
⊢ (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val) ⟨x, hx⟩ ∈
    Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))

Tactic:
refine .of_comp (f := algebraMap R S) ?_

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
M : Submonoid R
inst✝ : IsLocalization M S
x✝ : ↥(integralClosure R B)
x : B
hx : x ∈ integralClosure R B
⊢ ((algebraMap S (S ⊗[R] B)).comp (algebraMap R S)).IsIntegralElem
    ((Algebra.TensorProduct.includeRight.comp (integralClosure R B).val) ⟨x, hx⟩)
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
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁴ : p.IsPrime
this✝³ : Module p.ResidueField (p.Fiber S) := leftModule
this✝² : SMul p.ResidueField (p.Fiber S) := this✝³.toSMul
this✝¹ : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : Q.ResidueField
hx0 : x ≠ 0
hx : p.ResidueField[x] = ⊤
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Fiber.lift_residueField_surjective p _ x

Goal state after:
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
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁴ : p.IsPrime
this✝³ : Module p.ResidueField (p.Fiber S) := leftModule
this✝² : SMul p.ResidueField (p.Fiber S) := this✝³.toSMul
this✝¹ : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
hx0 : (TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯) x ≠ 0
hx :
  p.ResidueField[(TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯)
        x] =
    ⊤
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝³ : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝² : Algebra (↥R₂) St := R₂.toAlgebra
this✝¹ : Algebra (↥R₁) St := R₁.toAlgebra
this✝ : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
⊢ eval₂ ((algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩)) ((algebraMap S St) t) q = (algebraMap S St) 0

Tactic:
← hq',

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝³ : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝² : Algebra (↥R₂) St := R₂.toAlgebra
this✝¹ : Algebra (↥R₁) St := R₁.toAlgebra
this✝ : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
⊢ eval₂ ((algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩)) ((algebraMap S St) t) q =
    (algebraMap S St) (eval₂ φ.toRingHom t q)
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
φ : R[X] →ₐ[R] S
t : S
ht : φ.IsIntegralElem t
r : R[X]
hpm : Monic 1
hr : φ r = φ 1 * t
⊢ IsIntegral R (t - φ r)

Tactic:
simp_all [isIntegral_zero]

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 S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg : φ.Etale
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
algebraize [φ]

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr
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
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsReduced S]
    {x : S},
    (aeval x).Finite →
      ∀ (P : Ideal S) [inst_4 : P.IsPrime] [WeaklyQuasiFiniteAt R P],
        IsDomain S ∧ FaithfulSMul R S → ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : p ∈ ⊥.minimalPrimes
hpP : p ≤ P
inst✝¹ : p.IsPrime
inst✝ : (Ideal.map (Ideal.Quotient.mk p) P).IsPrime
inst : WeaklyQuasiFiniteAt (R ⧸ Ideal.under R p) (Ideal.map (Ideal.Quotient.mk p) P)
⊢ False

Tactic:
refine this (R := R ⧸ p.under R) ?_ (P.map (Ideal.Quotient.mk p)) ⟨inferInstance, inferInstance⟩
      ((isStronglyTranscendental_mk_of_mem_minimalPrimes hx p hp).of_surjective_left
        Ideal.Quotient.mk_surjective)

Goal state after:
case inr
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
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsReduced S]
    {x : S},
    (aeval x).Finite →
      ∀ (P : Ideal S) [inst_4 : P.IsPrime] [WeaklyQuasiFiniteAt R P],
        IsDomain S ∧ FaithfulSMul R S → ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : p ∈ ⊥.minimalPrimes
hpP : p ≤ P
inst✝¹ : p.IsPrime
inst✝ : (Ideal.map (Ideal.Quotient.mk p) P).IsPrime
inst : WeaklyQuasiFiniteAt (R ⧸ Ideal.under R p) (Ideal.map (Ideal.Quotient.mk p) P)
⊢ (aeval ((Ideal.Quotient.mk p) x)).Finite
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
⊢ ↑((addLinearEquiv R m n).symm PQ) =
    ↑((addLinearEquiv R m n).symm ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n) PQ.1 + (LinearMap.inr R (↥R[X]_m) ↥R[X]_n) PQ.2))

Tactic:
LinearMap.inl_apply,

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
⊢ ↑((addLinearEquiv R m n).symm PQ) =
    ↑((addLinearEquiv R m n).symm ((PQ.1, 0) + (LinearMap.inr R (↥R[X]_m) ↥R[X]_n) PQ.2))
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case h.zero
R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
n : ℕ
IH :
  ∀ m < 0,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m → ZariskisMainProperty R p
r : R
hf : (aeval x) (C r) = 0
hfn : (algebraMap R S) ((C r).coeff n) ∉ p
hm : (C r).natDegree = 0
⊢ ZariskisMainProperty R p

Tactic:
cases n <;> aesop

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ (∏ x,
      ∏ x_1 > x,
        if finSumFinEquiv (finSumFinEquiv.symm x).swap < finSumFinEquiv (finSumFinEquiv.symm x_1).swap then 1 else -1) =
    (-1) ^ (m * n)

Tactic:
← finSumFinEquiv.prod_comp,

Goal state after:
case e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ (∏ i,
      ∏ x > finSumFinEquiv i,
        if
            finSumFinEquiv (finSumFinEquiv.symm (finSumFinEquiv i)).swap <
              finSumFinEquiv (finSumFinEquiv.symm x).swap then
          1
        else -1) =
    (-1) ^ (m * n)