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

Goal state before:
pp: case neg
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
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
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
⊢ R[x] ≤ (integralClosure R S).saturation (Submonoid.powers ((algebraMap R S) f.leadingCoeff)) ⋯

Tactic:
]

Goal state after:
case neg
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
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
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
⊢ R[x] ≤ (integralClosure R S).saturation (Submonoid.powers ((algebraMap R S) f.leadingCoeff)) ⋯
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ ↑↑(∏ i,
            ∏ j > i,
              if
                  ((finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)).trans
                        (finCongr ⋯).symm)
                      i <
                    ((finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)).trans
                        (finCongr ⋯).symm)
                      j then
                1
              else -1) *
      (g.sylvester f n m).det =
    (-1) ^ (m * n) * (g.sylvester f n m).det

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ ↑↑(∏ i,
            ∏ j > i,
              if
                  ((finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)).trans
                        (finCongr ⋯).symm)
                      i <
                    ((finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)).trans
                        (finCongr ⋯).symm)
                      j then
                1
              else -1) *
      (g.sylvester f n m).det =
    (-1) ^ (m * n) * (g.sylvester f n m).det
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 = ⊥
hp : (conductor R (f X)).radical ≤ 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
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
hp : (conductor R (f X)).radical ≤ p
⊢ False
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: R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
⊢ (-1) ^ (m * n) * (0 ^ n * g.coeff 0 ^ m) = 0 ^ n * g.coeff 0 ^ m

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
⊢ (-1) ^ (m * n) * (0 ^ n * g.coeff 0 ^ m) = 0 ^ n * g.coeff 0 ^ m
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
⊢ ((pullbackRestrictIsoRestrict f ↑U).inv ≫
        Cover.trans (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
          (pullbackRestrictIsoRestrict f ↑V).hom) ≫
      (f ⁻¹ᵁ ↑V).ι =
    X.homOfLE ⋯ ≫ (f ⁻¹ᵁ ↑V).ι

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
⊢ ((pullbackRestrictIsoRestrict f ↑U).inv ≫
        Cover.trans (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
          (pullbackRestrictIsoRestrict f ↑V).hom) ≫
      (f ⁻¹ᵁ ↑V).ι =
    X.homOfLE ⋯ ≫ (f ⁻¹ᵁ ↑V).ι
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ
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
⊢ ((M (i + 1)).updateCol ⟨i, ⋯⟩ fun k_1 ↦ M (i + 1) k_1 ⟨i, ⋯⟩ + -r • M (i + 1) k_1 ⟨i + k + m, ⋯⟩).det = (M i).det

Tactic:
]

Goal state after:
case succ
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
⊢ ((M (i + 1)).updateCol ⟨i, ⋯⟩ fun k_1 ↦ M (i + 1) k_1 ⟨i, ⋯⟩ + -r • M (i + 1) k_1 ⟨i + k + m, ⋯⟩).det = (M i).det
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.toRingHom ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
        (normalizationOpenCover f).f V =
    (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
        (normalizationOpenCover f).f U

Tactic:
]

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.toRingHom ≫
            X.presheaf.map (homOfLE ⋯).op) ≫
        (normalizationOpenCover f).f V =
    (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
        (normalizationOpenCover f).f U
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.ι (normalizationGlueData f).functor V =
    (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫
        (normalizationGlueData f).functor.map i ≫ colimit.ι (normalizationGlueData f).functor V

Tactic:
]

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.ι (normalizationGlueData f).functor V =
    (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫
        (normalizationGlueData f).functor.map i ≫ colimit.ι (normalizationGlueData f).functor V
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
          ((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

Tactic:
]

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
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: 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 : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
⊢ (algebraMap R S).Finite

Tactic:
]

Goal state after:
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 : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
⊢ (algebraMap R S).Finite
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ ((pullbackRestrictIsoRestrict f ↑U).hom ≫ (f ⁻¹ᵁ ↑U).ι) ≫ toNormalization f =
    (pullbackRestrictIsoRestrict f ↑U).hom ≫
      (f ⁻¹ᵁ ↑U).toSpecΓ ≫
        Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
          (normalizationOpenCover f).f U

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ ((pullbackRestrictIsoRestrict f ↑U).hom ≫ (f ⁻¹ᵁ ↑U).ι) ≫ toNormalization f =
    (pullbackRestrictIsoRestrict f ↑U).hom ≫
      (f ⁻¹ᵁ ↑U).toSpecΓ ≫
        Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
          (normalizationOpenCover f).f U
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
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
this : ⟨↑j₂ + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑j₂ + k, ⋯⟩
h₁ : (↑j₂ ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + n) ∧ k ≤ ↑j₁ - ↑j₂
h₂ : ¬(↑j₂ + k ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + (k + m))
⊢ 0 = 0

pp: case neg
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
this : ⟨↑j₂ + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑j₂ + k, ⋯⟩
h₁ : (↑j₂ ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + n) ∧ k ≤ ↑j₁ - ↑j₂
h₂ : ¬(↑j₂ + k ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + (k + m))
⊢ f.natDegree < ↑j₁ - ↑j₂ - k

Tactic:
]

Goal state after:
case neg
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
this : ⟨↑j₂ + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑j₂ + k, ⋯⟩
h₁ : (↑j₂ ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + n) ∧ k ≤ ↑j₁ - ↑j₂
h₂ : ¬(↑j₂ + k ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + (k + m))
⊢ f.natDegree < ↑j₁ - ↑j₂ - k
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap f.base.hom') ↑k) ⋯).I₀
⊢ (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map
          ((normalizationDiagramMap f).app (Opposite.op ↑U) ≫
            CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
        IsAffineOpen.fromSpec ⋯ =
    (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap f.base.hom') ↑k) ⋯).f U ≫ f

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap f.base.hom') ↑k) ⋯).I₀
⊢ (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map
          ((normalizationDiagramMap f).app (Opposite.op ↑U) ≫
            CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
        IsAffineOpen.fromSpec ⋯ =
    (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap f.base.hom') ↑k) ⋯).f U ≫ f
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ ∀ (i : ↑Y.affineOpens), IsIntegralHom (fromNormalization f ∣_ ↑i)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ ∀ (i : ↑Y.affineOpens), IsIntegralHom (fromNormalization f ∣_ ↑i)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: n : ℕ
IH :
  ∀ {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 : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
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 : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝² : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝¹ : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝ : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
⊢ ((↑f).comp (algebraMap R (MvPolynomial (Fin (n + 1)) R))).FiniteType

Tactic:
]

Goal state after:
n : ℕ
IH :
  ∀ {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 : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
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 : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝² : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝¹ : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝ : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
⊢ ((↑f).comp (algebraMap R (MvPolynomial (Fin (n + 1)) R))).FiniteType
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.inl.right
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)
i : Fin n
IH : ↑(Fin.natAdd m i) ≤ m → (M ↑(Fin.natAdd m i)).det = M₂.det
hi : m + ↑i + 1 ≤ m
this : ⟨m + ↑i + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑i + (k + m), ⋯⟩
⊢ 0 = 0

pp: case succ.inl.right.hnc
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)
i : Fin n
IH : ↑(Fin.natAdd m i) ≤ m → (M ↑(Fin.natAdd m i)).det = M₂.det
hi : m + ↑i + 1 ≤ m
this : ⟨m + ↑i + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑i + (k + m), ⋯⟩
⊢ ¬(↑i + (k + m) ≤ ↑j₁ ∧ ↑j₁ ≤ ↑i + (k + m) + m)

Tactic:
]

Goal state after:
case succ.inl.right.hnc
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)
i : Fin n
IH : ↑(Fin.natAdd m i) ≤ m → (M ↑(Fin.natAdd m i)).det = M₂.det
hi : m + ↑i + 1 ≤ m
this : ⟨m + ↑i + (k + m), ⋯⟩ = Fin.natAdd m ⟨↑i + (k + m), ⋯⟩
⊢ ¬(↑i + (k + m) ≤ ↑j₁ ∧ ↑j₁ ≤ ↑i + (k + m) + m)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U :=
  IsOpenImmersion.isoOfRangeEq (fromNormalization f ⁻¹ᵁ ↑U).ι ((normalizationOpenCover f).f U) ⋯
⊢ IsIntegralHom ((e.inv ≫ fromNormalization f ∣_ ↑U) ≫ (IsAffineOpen.isoSpec ⋯).hom)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U :=
  IsOpenImmersion.isoOfRangeEq (fromNormalization f ⁻¹ᵁ ↑U).ι ((normalizationOpenCover f).f U) ⋯
⊢ IsIntegralHom ((e.inv ≫ fromNormalization f ∣_ ↑U) ≫ (IsAffineOpen.isoSpec ⋯).hom)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
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₂
this : ∀ i ≤ m, (M i).det = M₂.det
⊢ (f.sylvester (g + f * (monomial k) r) m n).det = (M m).det

Tactic:
]

Goal state after:
case inr
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₂
this : ∀ i ≤ m, (M i).det = M₂.det
⊢ (f.sylvester (g + f * (monomial k) r) m n).det = (M m).det
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
H : p.support ⊆ Finset.range (n - m + 1)
⊢ f.resultant (g + f * ∑ n ∈ Finset.range (n - m + 1), (monomial n) (p.coeff n)) m n = f.resultant g m n

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
H : p.support ⊆ Finset.range (n - m + 1)
⊢ f.resultant (g + f * ∑ n ∈ Finset.range (n - m + 1), (monomial n) (p.coeff n)) m n = f.resultant g m n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
g : R[X]
H : 0 ≤ n - m + 1
⊢ f.resultant g m n = f.resultant g m n

Tactic:
]

Goal state after: