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

Goal state before:
pp: case e_f.h₁
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
x✝ : R
⊢ (((algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩)).comp C) x✝ =
    (((algebraMap S St).comp φ.toRingHom).comp C) x✝

pp: case h₂
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 := ⋯
t' : St := ⋯
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := ⋯
R₂ : Subalgebra (↥R₁) St := ⋯
this✝³ : Algebra ↥R₁ ↥R₂ := ⋯
this✝² : Algebra (↥R₂) St := ⋯
this✝¹ : Algebra (↥R₁) St := ⋯
this✝ : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
⊢ ((algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩)) X = ((algebraMap S St).comp φ.toRingHom) X

Tactic:
<;>

Goal state after:
case e_f.h₁
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
x✝ : R
⊢ (((algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩)).comp C) x✝ =
    (((algebraMap S St).comp φ.toRingHom).comp C) x✝

case h₂
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 := ⋯
t' : St := ⋯
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := ⋯
R₂ : Subalgebra (↥R₁) St := ⋯
this✝³ : Algebra ↥R₁ ↥R₂ := ⋯
this✝² : Algebra (↥R₂) St := ⋯
this✝¹ : Algebra (↥R₁) St := ⋯
this✝ : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
⊢ ((algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩)) X = ((algebraMap S St).comp φ.toRingHom) X
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case h₁
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[X]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
x✝ : R
⊢ (((aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R'))).comp C) x✝ =
    (((algebraMap S S').comp ↑φ).comp C) x✝

pp: case h₂
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[X]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
a : R := ⋯
R' : Type u_1 := ⋯
S' : Type u_2 := ⋯
this✝ : Algebra R' S' := ⋯
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
⊢ ((aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R'))) X = ((algebraMap S S').comp ↑φ) X

Tactic:
<;>

Goal state after:
case h₁
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[X]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
x✝ : R
⊢ (((aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R'))).comp C) x✝ =
    (((algebraMap S S').comp ↑φ).comp C) x✝

case h₂
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[X]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
a : R := ⋯
R' : Type u_1 := ⋯
S' : Type u_2 := ⋯
this✝ : Algebra R' S' := ⋯
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
⊢ ((aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R'))) X = ((algebraMap S S').comp ↑φ) X
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case refine_3
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
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
hsQ' : (algebraMap R Q.ResidueField) s ≠ 0
hrQ' : φ r = 1
e' : (algebraMap R Q.ResidueField) s * φ x = (algebraMap S Q.ResidueField) t
this : φ x = ((algebraMap R p.ResidueField) s)⁻¹ • (algebraMap S Q.ResidueField) t
⊢ ((algebraMap R p.ResidueField) s)⁻¹ • (algebraMap S Q.ResidueField) t ∈
    (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t]

Tactic:
exact Subalgebra.smul_mem _ (self_mem_adjoin_singleton _ _) _

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✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝² : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this✝¹ : Algebra R[X] S := f.toAlgebra
this✝ : IsScalarTower R R[X] S
this : Module.Finite R[X] S
p : R[X]
hp : (algebraMap R[X] S) p = 0
hp' : ¬p = 0
⊢ (aeval (f X)) p = 0

Tactic:
by rwa [aeval_algHom_apply, aeval_X_left_apply]

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

Goal state before:
pp: case inr.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✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
    [inst_3 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q],
    Unramified R S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H✝ : ¬Unramified R S
s : S
hsQ : s ∉ Q
hs : FormallyUnramified R (Localization.Away s)
hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime
inst : Unramified R (Localization.Away s)
f : S
t : ↥(Submonoid.powers s)
hf : IsLocalization.mk' (Localization.Away s) f t ∉ Ideal.map (algebraMap S (Localization.Away s)) Q
H : HasStandardEtaleSurjectionOn R (IsLocalization.mk' (Localization.Away s) f t)
P : StandardEtalePair R
φ : P.Ring →ₐ[R] Localization.Away ((algebraMap S (Localization.Away s)) f)
hφ : Function.Surjective ⇑φ
⊢ HasStandardEtaleSurjectionOn R (s * f)

Tactic:
exact .mk _ hφ

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
h✝¹ : ↑i ∈ Icc (↑j) (↑j + 0)
h✝ : i = Fin.natAdd 0 j
⊢ f.coeff (↑i - ↑j) = f.coeff 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
h✝¹ : ↑i ∈ Icc (↑j) (↑j + 0)
h✝ : ¬i = Fin.natAdd 0 j
⊢ f.coeff (↑i - ↑j) = 0

pp: case pos
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
h✝¹ : ↑i ∉ Icc (↑j) (↑j + 0)
h✝ : i = Fin.natAdd 0 j
⊢ 0 = f.coeff 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
h✝¹ : ↑i ∉ Icc (↑j) (↑j + 0)
h✝ : ¬i = Fin.natAdd 0 j
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
h✝¹ : ↑i ∈ Icc (↑j) (↑j + 0)
h✝ : i = Fin.natAdd 0 j
⊢ f.coeff (↑i - ↑j) = f.coeff 0

case neg
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
h✝¹ : ↑i ∈ Icc (↑j) (↑j + 0)
h✝ : ¬i = Fin.natAdd 0 j
⊢ f.coeff (↑i - ↑j) = 0

case pos
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
h✝¹ : ↑i ∉ Icc (↑j) (↑j + 0)
h✝ : i = Fin.natAdd 0 j
⊢ 0 = f.coeff 0

case neg
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
h✝¹ : ↑i ∉ Icc (↑j) (↑j + 0)
h✝ : ¬i = Fin.natAdd 0 j
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case left
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m n : ℕ
i : Fin (m + n)
i✝ : Fin m
⊢ f.sylvester g m n i (Fin.castAdd n i✝) =
    (Matrix.reindex (finCongr ⋯) (finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)))
      (g.sylvester f n m) i (Fin.castAdd n i✝)

pp: case right
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m n : ℕ
i : Fin (m + n)
i✝ : Fin n
⊢ f.sylvester g m n i (Fin.natAdd m i✝) =
    (Matrix.reindex (finCongr ⋯) (finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)))
      (g.sylvester f n m) i (Fin.natAdd m i✝)

Tactic:
<;>

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m n : ℕ
i : Fin (m + n)
i✝ : Fin m
⊢ f.sylvester g m n i (Fin.castAdd n i✝) =
    (Matrix.reindex (finCongr ⋯) (finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)))
      (g.sylvester f n m) i (Fin.castAdd n i✝)

case right
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m n : ℕ
i : Fin (m + n)
i✝ : Fin n
⊢ f.sylvester g m n i (Fin.natAdd m i✝) =
    (Matrix.reindex (finCongr ⋯) (finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)))
      (g.sylvester f n m) i (Fin.natAdd m i✝)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case left
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f g : R[X]
m n : ℕ
φ : R →+* S
i : Fin (m + n)
i✝ : Fin m
⊢ (map φ f).sylvester (map φ g) m n i (Fin.castAdd n i✝) = φ.mapMatrix (f.sylvester g m n) i (Fin.castAdd n i✝)

pp: case right
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f g : R[X]
m n : ℕ
φ : R →+* S
i : Fin (m + n)
i✝ : Fin n
⊢ (map φ f).sylvester (map φ g) m n i (Fin.natAdd m i✝) = φ.mapMatrix (f.sylvester g m n) i (Fin.natAdd m i✝)

Tactic:
<;>

Goal state after:
case left
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f g : R[X]
m n : ℕ
φ : R →+* S
i : Fin (m + n)
i✝ : Fin m
⊢ (map φ f).sylvester (map φ g) m n i (Fin.castAdd n i✝) = φ.mapMatrix (f.sylvester g m n) i (Fin.castAdd n i✝)

case right
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f g : R[X]
m n : ℕ
φ : R →+* S
i : Fin (m + n)
i✝ : Fin n
⊢ (map φ f).sylvester (map φ g) m n i (Fin.natAdd m i✝) = φ.mapMatrix (f.sylvester g m n) i (Fin.natAdd m i✝)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case h.zero.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)
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
hm : (C r).natDegree = 0
hfn : (algebraMap R S) ((C r).coeff 0) ∉ p
⊢ ZariskisMainProperty R p

pp: case h.zero.succ
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)
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
hm : (C r).natDegree = 0
n✝ : ℕ
hfn : (algebraMap R S) ((C r).coeff (n✝ + 1)) ∉ p
⊢ ZariskisMainProperty R p

Tactic:
<;>

Goal state after:
case h.zero.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)
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
hm : (C r).natDegree = 0
hfn : (algebraMap R S) ((C r).coeff 0) ∉ p
⊢ ZariskisMainProperty R p

case h.zero.succ
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)
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
hm : (C r).natDegree = 0
n✝ : ℕ
hfn : (algebraMap R S) ((C r).coeff (n✝ + 1)) ∉ p
⊢ ZariskisMainProperty R p
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case h₁
R S : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S), f.Finite → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
inst✝ : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
x✝ : R
⊢ (((aeval (f X)).comp (mapRingHom (algebraMap R ↥(integralClosure R S)))).comp C) x✝ = (f.comp C) x✝

pp: case h₂
R S : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S), f.Finite → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
inst✝ : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := ⋯
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
⊢ ((aeval (f X)).comp (mapRingHom (algebraMap R ↥(integralClosure R S)))) X = f.toRingHom X

Tactic:
<;>

Goal state after:
case h₁
R S : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S), f.Finite → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
inst✝ : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
x✝ : R
⊢ (((aeval (f X)).comp (mapRingHom (algebraMap R ↥(integralClosure R S)))).comp C) x✝ = (f.comp C) x✝

case h₂
R S : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S), f.Finite → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
inst✝ : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := ⋯
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
⊢ ((aeval (f X)).comp (mapRingHom (algebraMap R ↥(integralClosure R S)))) X = f.toRingHom X
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
g : R[X]
m : ℕ
⊢ (-1) ^ (m * 0) * (0 ^ 0 * g.coeff 0 ^ m) = 0 ^ 0 * g.coeff 0 ^ m

pp: case succ
R : Type u_1
inst✝ : CommRing R
g : R[X]
m n✝ : ℕ
⊢ (-1) ^ (m * (n✝ + 1)) * (0 ^ (n✝ + 1) * g.coeff 0 ^ m) = 0 ^ (n✝ + 1) * g.coeff 0 ^ m

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
g : R[X]
m : ℕ
⊢ (-1) ^ (m * 0) * (0 ^ 0 * g.coeff 0 ^ m) = 0 ^ 0 * g.coeff 0 ^ m

case succ
R : Type u_1
inst✝ : CommRing R
g : R[X]
m n✝ : ℕ
⊢ (-1) ^ (m * (n✝ + 1)) * (0 ^ (n✝ + 1) * g.coeff 0 ^ m) = 0 ^ (n✝ + 1) * g.coeff 0 ^ m
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case h₁
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
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
x✝ : R
⊢ ((aeval ((Ideal.Quotient.mk (conductor R (f X)).radical) (f X))).comp C) x✝ =
    (((Ideal.Quotient.mk J).comp f.toRingHom).comp C) x✝

pp: case h₂
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
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := ⋯
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
⊢ (aeval ((Ideal.Quotient.mk (conductor R (f X)).radical) (f X))).toRingHom X =
    ((Ideal.Quotient.mk J).comp f.toRingHom) X

Tactic:
<;>

Goal state after:
case h₁
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
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
x✝ : R
⊢ ((aeval ((Ideal.Quotient.mk (conductor R (f X)).radical) (f X))).comp C) x✝ =
    (((Ideal.Quotient.mk J).comp f.toRingHom).comp C) x✝

case h₂
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
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := ⋯
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
⊢ (aeval ((Ideal.Quotient.mk (conductor R (f X)).radical) (f X))).toRingHom X =
    ((Ideal.Quotient.mk J).comp f.toRingHom) X
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  (pullbackRestrictIsoRestrict f ↑U).inv ≫
      Cover.trans (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        (pullbackRestrictIsoRestrict f ↑V).hom =
    X.homOfLE ⋯
⊢ (f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑V) ↑Γ(X, f ⁻¹ᵁ ↑V)).val ≫ X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V =
    (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫
        Spec.map ((normalizationDiagram f).map ((toOpensFunctor Y).map i).op) ≫
          colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V

Tactic:
rw [← Spec.map_comp_assoc]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  (pullbackRestrictIsoRestrict f ↑U).inv ≫
      Cover.trans (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        (pullbackRestrictIsoRestrict f ↑V).hom =
    X.homOfLE ⋯
⊢ (f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑V) ↑Γ(X, f ⁻¹ᵁ ↑V)).val ≫ X.presheaf.map (homOfLE ⋯).op) ≫
        colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V =
    (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map
          ((normalizationDiagram f).map ((toOpensFunctor Y).map i).op ≫
            CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫
        colimit.ι (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp ⋙ Scheme.Spec) V