mathlib-initiative/mathlib-tactics huggingface dataset:
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
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝⁷ : IsDomain S'
this✝⁶ : IsDomain R
this✝⁵ : Algebra.IsIntegral R R'
this✝⁴ : FaithfulSMul R' K
this✝³ : FaithfulSMul R R'
this✝² : FaithfulSMul R' L
this✝¹ : FaithfulSMul R' S'
this✝ : IsIntegrallyClosedIn R' K
this : IsIntegrallyClosed R'
g : R' ⊗[R] S →ₐ[R'] S' := TensorProduct.lift (ofId R' S') f ⋯
hf₃ : Function.Injective ⇑f
x✝ : S
⊢ f x✝ =
    ((AlgHom.restrictScalars R g).comp ((↑(TensorProduct.comm R S R')).comp (IsScalarTower.toAlgHom R S (S ⊗[R] R'))))
      x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝²⁸ : CommRing R
inst✝²⁷ : CommRing S
inst✝²⁶ : Algebra R S
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝⁷ : IsDomain S'
this✝⁶ : IsDomain R
this✝⁵ : Algebra.IsIntegral R R'
this✝⁴ : FaithfulSMul R' K
this✝³ : FaithfulSMul R R'
this✝² : FaithfulSMul R' L
this✝¹ : FaithfulSMul R' S'
this✝ : IsIntegrallyClosedIn R' K
this : IsIntegrallyClosed R'
g : R' ⊗[R] S →ₐ[R'] S' := TensorProduct.lift (ofId R' S') f ⋯
hf₃ : Function.Injective ⇑f
x✝ : S
⊢ f x✝ =
    ((AlgHom.restrictScalars R g).comp ((↑(TensorProduct.comm R S R')).comp (IsScalarTower.toAlgHom R S (S ⊗[R] R'))))
      x✝
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
a✝ : Nontrivial R
⊢ ↑f /ₘ X ^ m = ↑((addLinearEquiv R m n) f).2 ∧ ↑f %ₘ X ^ m = ↑((addLinearEquiv R m n) f).1

Tactic:
;

Goal state after:
m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
a✝ : Nontrivial R
⊢ ↑f /ₘ X ^ m = ↑((addLinearEquiv R m n) f).2 ∧ ↑f %ₘ X ^ m = ↑((addLinearEquiv R m n) f).1
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: case refine_2
m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
a✝ : Nontrivial R
⊢ ↑((addLinearEquiv R m n) f).1 ∈ R[X]_m

Tactic:
;

Goal state after:
case refine_2
m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
a✝ : Nontrivial R
⊢ ↑((addLinearEquiv R m n) f).1 ∈ R[X]_m
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
x✝ : R[X]
⊢ x✝ ∈ Submodule.comap (↑↑(taylorEquiv r)) R[X]_n ↔ x✝ ∈ R[X]_n

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
x✝ : R[X]
⊢ x✝ ∈ Submodule.comap (↑↑(taylorEquiv r)) R[X]_n ↔ x✝ ∈ R[X]_n
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:
;

Goal state after:
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
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f g : R[X]
m n : ℕ
φ : R →+* S
i j : Fin (m + n)
⊢ (map φ f).sylvester (map φ g) m n i j = φ.mapMatrix (f.sylvester g m n) i j
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : f.natDegree = 0
i : ℕ
hi : i < f.natDegree - 1 + f.natDegree
j✝ : Fin (f.natDegree - 1 + f.natDegree)
⊢ f.sylvesterDeriv.updateRow ⟨2 * f.natDegree - 2, ⋯⟩ (f.leadingCoeff • f.sylvesterDeriv ⟨2 * f.natDegree - 2, ⋯⟩)
      ⟨i, hi⟩ j✝ =
    (derivative f).sylvester f (f.natDegree - 1) f.natDegree ⟨i, hi⟩ j✝

Tactic:
;

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : f.natDegree = 0
i : ℕ
hi : i < f.natDegree - 1 + f.natDegree
j✝ : Fin (f.natDegree - 1 + f.natDegree)
⊢ f.sylvesterDeriv.updateRow ⟨2 * f.natDegree - 2, ⋯⟩ (f.leadingCoeff • f.sylvesterDeriv ⟨2 * f.natDegree - 2, ⋯⟩)
      ⟨i, hi⟩ j✝ =
    (derivative f).sylvester f (f.natDegree - 1) f.natDegree ⟨i, hi⟩ j✝
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
hx : x ∈ integralClosure ↑Γ(Y, Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
i : Opposite.op V ⟶ Opposite.op U
algInst✝⁴ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst✝³ : Algebra ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ V) := (CommRingCat.Hom.hom (app f V)).toAlgebra
algInst✝² : Algebra ↑Γ(Y, V) ↑Γ(Y, U) := (CommRingCat.Hom.hom (Y.presheaf.map i)).toAlgebra
algInst✝¹ : Algebra ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯)).toAlgebra
⊢ CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯) =
    CommRingCat.Hom.hom (f.c.app (Opposite.op V) ≫ X.presheaf.map ((TopologicalSpace.Opens.map f.base).map i.unop).op)

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
hx : x ∈ integralClosure ↑Γ(Y, Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
i : Opposite.op V ⟶ Opposite.op U
algInst✝⁴ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst✝³ : Algebra ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ V) := (CommRingCat.Hom.hom (app f V)).toAlgebra
algInst✝² : Algebra ↑Γ(Y, V) ↑Γ(Y, U) := (CommRingCat.Hom.hom (Y.presheaf.map i)).toAlgebra
algInst✝¹ : Algebra ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯)).toAlgebra
⊢ CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯) =
    CommRingCat.Hom.hom (f.c.app (Opposite.op V) ≫ X.presheaf.map ((TopologicalSpace.Opens.map f.base).map i.unop).op)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opensᵒᵖ
⊢ CommRingCat.ofHom
      ((RingHom.id ↑Γ(X, f ⁻¹ᵁ Opposite.unop U)).restrict
        (integralClosure ↑(Y.presheaf.obj U) ↑Γ(X, f ⁻¹ᵁ Opposite.unop U))
        (integralClosure ↑(Y.presheaf.obj U) ↑Γ(X, f ⁻¹ᵁ Opposite.unop U)) ⋯) =
    𝟙 (CommRingCat.of ↥(integralClosure ↑(Y.presheaf.obj U) ↑Γ(X, f ⁻¹ᵁ Opposite.unop U)))

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opensᵒᵖ
⊢ CommRingCat.ofHom
      ((RingHom.id ↑Γ(X, f ⁻¹ᵁ Opposite.unop U)).restrict
        (integralClosure ↑(Y.presheaf.obj U) ↑Γ(X, f ⁻¹ᵁ Opposite.unop U))
        (integralClosure ↑(Y.presheaf.obj U) ↑Γ(X, f ⁻¹ᵁ Opposite.unop U)) ⋯) =
    𝟙 (CommRingCat.of ↥(integralClosure ↑(Y.presheaf.obj U) ↑Γ(X, f ⁻¹ᵁ Opposite.unop U)))
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case h₂
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)
heg :
  ∀ (g : R[X]),
    e (1 ⊗ₜ[R] (aeval 𝓟.x) g) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)))
        ((AdjoinRoot.mk 𝓟'.f) (Polynomial.map (algebraMap R B) g))
k : ℕ
hk : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a)
y : B[X]
hy : (AdjoinRoot.mk 𝓟'.f) (derivative 𝓟'.f) * ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a) = (AdjoinRoot.mk 𝓟'.f) y
hRy : ∀ (i : ℕ), IsIntegral R (y.coeff i)
⊢ 𝓟.x ⊗ₜ[R] 1 = (Algebra.TensorProduct.comm R B S) 𝓟'.x

Tactic:
;

Goal state after:
case h₂
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)
heg :
  ∀ (g : R[X]),
    e (1 ⊗ₜ[R] (aeval 𝓟.x) g) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)))
        ((AdjoinRoot.mk 𝓟'.f) (Polynomial.map (algebraMap R B) g))
k : ℕ
hk : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a)
y : B[X]
hy : (AdjoinRoot.mk 𝓟'.f) (derivative 𝓟'.f) * ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a) = (AdjoinRoot.mk 𝓟'.f) y
hRy : ∀ (i : ℕ), IsIntegral R (y.coeff i)
⊢ 𝓟.x ⊗ₜ[R] 1 = (Algebra.TensorProduct.comm R B S) 𝓟'.x
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: 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)
f : R[X]
hf : (aeval x) f = 0
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∈ p
a : R
ha : (ofId R S).toRingHom a = f.leadingCoeff • x
hfn : (algebraMap R S) (f.coeff f.natDegree) ∉ p
this : (algebraMap R S) (f.coeff f.natDegree) + (algebraMap R S) (if f.natDegree = m then a else 0) ∉ p
⊢ False

Tactic:
;

Goal state after:
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)
f : R[X]
hf : (aeval x) f = 0
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∈ p
a : R
ha : (ofId R S).toRingHom a = f.leadingCoeff • x
hfn : (algebraMap R S) (f.coeff f.natDegree) ∉ p
this : (algebraMap R S) (f.coeff f.natDegree) + (algebraMap R S) (if f.natDegree = m then a else 0) ∉ p
⊢ False
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : (TopologicalSpace.Opens ↥Y)ᵒᵖ
i : U ⟶ V
x : ↑(Y.presheaf.obj U)
⊢ (CommRingCat.Hom.hom
        (Y.presheaf.map i ≫
          CommRingCat.ofHom
            (algebraMap ↑Γ(Y, Opposite.unop V) ↥(integralClosure ↑Γ(Y, Opposite.unop V) ↑Γ(X, f ⁻¹ᵁ Opposite.unop V)))))
      x =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (algebraMap ↑Γ(Y, Opposite.unop U) ↥(integralClosure ↑Γ(Y, Opposite.unop U) ↑Γ(X, f ⁻¹ᵁ Opposite.unop U))) ≫
          (normalizationDiagram f).map i))
      x

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
U V : (TopologicalSpace.Opens ↥Y)ᵒᵖ
i : U ⟶ V
x : ↑(Y.presheaf.obj U)
⊢ (CommRingCat.Hom.hom
        (Y.presheaf.map i ≫
          CommRingCat.ofHom
            (algebraMap ↑Γ(Y, Opposite.unop V) ↥(integralClosure ↑Γ(Y, Opposite.unop V) ↑Γ(X, f ⁻¹ᵁ Opposite.unop V)))))
      x =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (algebraMap ↑Γ(Y, Opposite.unop U) ↥(integralClosure ↑Γ(Y, Opposite.unop U) ↑Γ(X, f ⁻¹ᵁ Opposite.unop U))) ≫
          (normalizationDiagram f).map i))
      x
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
⊢ (-1) ^ (m * 0) * g.resultant f 0 m = g.coeff 0 ^ m
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
f : R[X]
n : ℕ
⊢ f.resultant 0 0 n = 0 ^ 0 * f.coeff 0 ^ n

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

Tactic:
;

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
f : R[X]
n : ℕ
⊢ f.resultant 0 0 n = 0 ^ 0 * f.coeff 0 ^ n

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

Goal state before:
pp: 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)
⊢ aeval (f X) = f

Tactic:
;

Goal state after:
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)
⊢ aeval (f X) = f
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: 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 (f X)) X = f X

Tactic:
;

Goal state after:
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 (f X)) X = f X
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
g : R[X]
r : R
n k : ℕ
hk : k + 0 ≤ n
q : R
hf : (C q).natDegree ≤ 0
⊢ (C q).resultant (g + C q * (monomial k) r) 0 n = (C q).resultant g 0 n

Tactic:
;

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
g : R[X]
r : R
n k : ℕ
hk : k + 0 ≤ n
q : R
hf : (C q).natDegree ≤ 0
⊢ (C q).resultant (g + C q * (monomial k) r) 0 n = (C q).resultant g 0 n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
hi : 0 ≤ m
⊢ (Matrix.of fun j₁ j₂ ↦ M₂ j₁ j₂).det = M₂.det

Tactic:
;

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
hi : 0 ≤ m
⊢ (Matrix.of fun j₁ j₂ ↦ M₂ j₁ j₂).det = M₂.det
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
IH : i ≤ m → (M i).det = M₂.det
hi : i + 1 ≤ m
⊢ ¬i = i + k + m

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
IH : i ≤ m → (M i).det = M₂.det
hi : i + 1 ≤ m
⊢ ¬i = i + k + m
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_1
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
H : integralClosure R S = ⊥
hf : ¬conductor R (f X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
this : WeaklyQuasiFiniteAt R (Ideal.under (↥f.range) p)
⊢ R[⟨f X, ⋯⟩] = ⊤

Tactic:
simp [← (Subalgebra.map_injective (f := Subalgebra.val _) Subtype.val_injective).eq_iff,
      ← AlgHom.map_adjoin_singleton f, Subalgebra.range_val]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑j₂ + 1 ≤ m
⊢ ↑j₂ + (k + m) = m + (↑j₂ + k)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑j₂ + 1 ≤ m
⊢ ↑j₂ + (k + m) = m + (↑j₂ + k)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case e_a
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ (pullbackRestrictIsoRestrict f ↑U).hom ≫ (f ⁻¹ᵁ ↑U).ι = (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U

Tactic:
;

Goal state after:
case e_a
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ (pullbackRestrictIsoRestrict f ↑U).hom ≫ (f ⁻¹ᵁ ↑U).ι = (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U