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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U
⊢ ((((ΓSpecIso Γ(Y, U)).inv ≫ (Spec Γ(Y, U)).presheaf.map (eqToHom ⋯).op) ≫
          app (Spec.map ((normalizationDiagramMap f).app (Opposite.op U))) (IsAffineOpen.fromSpec ⋯ ⁻¹ᵁ U)) ≫
        ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom ⋯).op) ≫
      ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom H).op =
    ((CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
          ((ΓSpecIso ((normalizationDiagram f).obj (Opposite.op ((toOpensFunctor Y).obj ⟨U, hU⟩)))).inv ≫
              (appIso ((normalizationOpenCover f).f ⟨U, hU⟩) ⊤).inv) ≫
            (normalization f).presheaf.map (eqToIso ⋯).op.inv) ≫
        app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U)) ≫
      ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom H).op

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U
⊢ ((((ΓSpecIso Γ(Y, U)).inv ≫ (Spec Γ(Y, U)).presheaf.map (eqToHom ⋯).op) ≫
          app (Spec.map ((normalizationDiagramMap f).app (Opposite.op U))) (IsAffineOpen.fromSpec ⋯ ⁻¹ᵁ U)) ≫
        ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom ⋯).op) ≫
      ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom H).op =
    ((CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
          ((ΓSpecIso ((normalizationDiagram f).obj (Opposite.op ((toOpensFunctor Y).obj ⟨U, hU⟩)))).inv ≫
              (appIso ((normalizationOpenCover f).f ⟨U, hU⟩) ⊤).inv) ≫
            (normalization f).presheaf.map (eqToIso ⋯).op.inv) ≫
        app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U)) ≫
      ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom H).op
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
this :
  ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
    f.Monic →
      g.Monic →
        f.Splits →
          g.Splits →
            g.natDegree ≤ f.natDegree → f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
hfg : ¬g.natDegree ≤ f.natDegree
⊢ (-1) ^ (f.natDegree * g.natDegree) * (Multiset.map ((fun ij ↦ ij.1 - ij.2) ∘ Prod.swap) (f.roots ×ˢ g.roots)).prod =
    (Multiset.map (fun ij ↦ -1) (f.roots ×ˢ g.roots)).prod *
      (Multiset.map (fun ij ↦ ij.2 - ij.1) (f.roots ×ˢ g.roots)).prod

Tactic:
]

Goal state after:
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
this :
  ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
    f.Monic →
      g.Monic →
        f.Splits →
          g.Splits →
            g.natDegree ≤ f.natDegree → f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
hfg : ¬g.natDegree ≤ f.natDegree
⊢ (-1) ^ (f.natDegree * g.natDegree) * (Multiset.map ((fun ij ↦ ij.1 - ij.2) ∘ Prod.swap) (f.roots ×ˢ g.roots)).prod =
    (Multiset.map (fun ij ↦ -1) (f.roots ×ˢ g.roots)).prod *
      (Multiset.map (fun ij ↦ ij.2 - ij.1) (f.roots ×ˢ g.roots)).prod
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_1.refine_2
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)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this✝¹ : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
this✝ : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
this : IsScalarTower (MvPolynomial (Fin n) R) (↥R') S
a : S
has : a ∈ s
⊢ IsIntegral (MvPolynomial (Fin n) R) (r ^ (s.sup m - m a) * (r ^ m a * a))

Tactic:
]

Goal state after:
case refine_1.refine_2
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)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this✝¹ : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
this✝ : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
this : IsScalarTower (MvPolynomial (Fin n) R) (↥R') S
a : S
has : a ∈ s
⊢ IsIntegral (MvPolynomial (Fin n) R) (r ^ (s.sup m - m a) * (r ^ m a * a))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
⊢ (g * r + g * -r).resultant g (g * r).natDegree = (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod

pp: n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
⊢ (-r).natDegree + g.natDegree ≤ (g * r).natDegree

Tactic:
]

Goal state after:
case pos
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
⊢ (g * r + g * -r).resultant g (g * r).natDegree = (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod

n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
⊢ (-r).natDegree + g.natDegree ≤ (g * r).natDegree
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
⊢ (normalizationObjIso f hU).hom ≫ CommRingCat.ofHom (integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U)).val.toRingHom =
    (normalizationObjIso f ⋯).hom ≫
      (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑⟨U, hU⟩) ↑Γ(X, f ⁻¹ᵁ ↑⟨U, hU⟩)).val ≫ X.presheaf.map (eqToHom ⋯).op) ≫
        X.presheaf.map (homOfLE ⋯).op

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
⊢ (normalizationObjIso f hU).hom ≫ CommRingCat.ofHom (integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U)).val.toRingHom =
    (normalizationObjIso f ⋯).hom ≫
      (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑⟨U, hU⟩) ↑Γ(X, f ⁻¹ᵁ ↑⟨U, hU⟩)).val ≫ X.presheaf.map (eqToHom ⋯).op) ≫
        X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
⊢ 0 ^ g.natDegree * g.coeff 0 ^ (g * r).natDegree =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod

Tactic:
]

Goal state after:
case pos
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
⊢ 0 ^ g.natDegree * g.coeff 0 ^ (g * r).natDegree =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
e : pullback (toNormalization f) ((normalizationOpenCover f).f U) ≅ ↑(f ⁻¹ᵁ ↑U) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (toNormalization f) ((normalizationOpenCover f).f U)) (f ⁻¹ᵁ ↑U).ι ⋯
⊢ MorphismProperty.isomorphisms Scheme
    ((e ≪≫ ⋯.isoSpec).inv ≫ Cover.pullbackHom (normalizationOpenCover f) (toNormalization f) U)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
e : pullback (toNormalization f) ((normalizationOpenCover f).f U) ≅ ↑(f ⁻¹ᵁ ↑U) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (toNormalization f) ((normalizationOpenCover f).f U)) (f ⁻¹ᵁ ↑U).ι ⋯
⊢ MorphismProperty.isomorphisms Scheme
    ((e ≪≫ ⋯.isoSpec).inv ≫ Cover.pullbackHom (normalizationOpenCover f) (toNormalization f) U)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_2
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)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
⊢ FiniteType R ↥R'

Tactic:
]

Goal state after:
case refine_2
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)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
⊢ FiniteType R ↥R'
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : ∃ x, x ∈ g.roots
⊢ 0 * g.coeff 0 ^ (g * r).natDegree = (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod

Tactic:
]

Goal state after:
case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : ∃ x, x ∈ g.roots
⊢ 0 * g.coeff 0 ^ (g * r).natDegree = (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
x : K
hx : x ∈ g.roots
⊢ 0 = 0

pp: case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
x : K
hx : x ∈ g.roots
⊢ 0 ∈ Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)

Tactic:
]

Goal state after:
case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
x : K
hx : x ∈ g.roots
⊢ 0 ∈ Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case e'_5
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
e : pullback (toNormalization f) ((normalizationOpenCover f).f U) ≅ ↑(f ⁻¹ᵁ ↑U) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (toNormalization f) ((normalizationOpenCover f).f U)) (f ⁻¹ᵁ ↑U).ι ⋯
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
e_3✝ : Spec Γ(X, f ⁻¹ᵁ ↑U) = Spec (CommRingCat.of ↑Γ(X, f ⁻¹ᵁ ↑U))
e_4✝ : (normalizationOpenCover f).X U = Spec (CommRingCat.of ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)))
⊢ ⋯.isoSpec.hom ≫
      ((e ≪≫ ⋯.isoSpec).inv ≫ Cover.pullbackHom (normalizationOpenCover f) (toNormalization f) U) ≫
        (normalizationOpenCover f).f U =
    ⋯.isoSpec.hom ≫
      Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
        (normalizationOpenCover f).f U

Tactic:
]

Goal state after:
case e'_5
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
e : pullback (toNormalization f) ((normalizationOpenCover f).f U) ≅ ↑(f ⁻¹ᵁ ↑U) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (toNormalization f) ((normalizationOpenCover f).f U)) (f ⁻¹ᵁ ↑U).ι ⋯
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
e_3✝ : Spec Γ(X, f ⁻¹ᵁ ↑U) = Spec (CommRingCat.of ↑Γ(X, f ⁻¹ᵁ ↑U))
e_4✝ : (normalizationOpenCover f).X U = Spec (CommRingCat.of ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)))
⊢ ⋯.isoSpec.hom ≫
      ((e ≪≫ ⋯.isoSpec).inv ≫ Cover.pullbackHom (normalizationOpenCover f) (toNormalization f) U) ≫
        (normalizationOpenCover f).f U =
    ⋯.isoSpec.hom ≫
      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: n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
⊢ g.natDegree + r.natDegree ≤ g.natDegree + r.natDegree

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
e : pullback (toNormalization f) ((normalizationOpenCover f).f U) ≅ ↑(f ⁻¹ᵁ ↑U) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (toNormalization f) ((normalizationOpenCover f).f U)) (f ⁻¹ᵁ ↑U).ι ⋯
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ (CommRingCat.Hom.hom (app f ↑U)).IsIntegral

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
e : pullback (toNormalization f) ((normalizationOpenCover f).f U) ≅ ↑(f ⁻¹ᵁ ↑U) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (toNormalization f) ((normalizationOpenCover f).f U)) (f ⁻¹ᵁ ↑U).ι ⋯
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ (CommRingCat.Hom.hom (app f ↑U)).IsIntegral
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
e : pullback (toNormalization f) ((normalizationOpenCover f).f U) ≅ ↑(f ⁻¹ᵁ ↑U) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (toNormalization f) ((normalizationOpenCover f).f U)) (f ⁻¹ᵁ ↑U).ι ⋯
this✝ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this : integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) = ⊤
⊢ IsIso (Spec.map (CommRingCat.ofHom ⊤.val.toRingHom))

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
e : pullback (toNormalization f) ((normalizationOpenCover f).f U) ≅ ↑(f ⁻¹ᵁ ↑U) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (toNormalization f) ((normalizationOpenCover f).f U)) (f ⁻¹ᵁ ↑U).ι ⋯
this✝ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this : integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) = ⊤
⊢ IsIso (Spec.map (CommRingCat.ofHom ⊤.val.toRingHom))