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

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

Tactic:
simp

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: 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
x : S ⊗[R] B
hx : x ∈ integralClosure S (S ⊗[R] B)
y : B
hy : IsIntegral R y
⊢ (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R B).val).toRingHom (1 ⊗ₜ[R] ⟨y, hy⟩) =
    ↑Algebra.TensorProduct.includeRight y

Tactic:
simp

Goal state after:
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
a : R
ha : (ofId R S).toRingHom a = f.leadingCoeff • x
h✝ : ¬n = m
⊢ (algebraMap R S) 0 ∈ p

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝⁴ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝³ : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝² : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝¹ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this✝ : IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (appLE f (↑U) (f ⁻¹ᵁ Y.basicOpen r) ⋯)).toAlgebra
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))) r)
    ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r))

Tactic:
have : IsScalarTower Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1) Γ(X, f ⁻¹ᵁ Y.basicOpen r) := .of_algebraMap_eq' rfl

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝⁵ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝⁴ : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝³ : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝² : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this✝¹ : IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
this✝ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (appLE f (↑U) (f ⁻¹ᵁ Y.basicOpen r) ⋯)).toAlgebra
this : IsScalarTower ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))) r)
    ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
r : R
m : ℕ
⊢ (C r).resultant g 0 m = r ^ m

Tactic:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
m : ℕ
r : R
⊢ f.resultant (C r) m 0 = r ^ m

Tactic:
simp

Goal state after:
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

Tactic:
simp

Goal state after:
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

Tactic:
simp

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

Goal state before:
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:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

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₂
i : ℕ
IH : i ≤ m → (M i).det = M₂.det
hi : i + 1 ≤ m
⊢ ⟨i, ⋯⟩ ≠ ⟨i + k + m, ⋯⟩

Tactic:
simp

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.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), ⋯⟩ = ↑(Fin.natAdd m ⟨↑j₂ + k, ⋯⟩)

Tactic:
simp

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:
simp

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)
i : Fin n
IH : ↑(Fin.natAdd m i) ≤ m → (M ↑(Fin.natAdd m i)).det = M₂.det
hi : m + ↑i + 1 ≤ m
⊢ ↑⟨m + ↑i + (k + m), ⋯⟩ = ↑(Fin.natAdd m ⟨↑i + (k + m), ⋯⟩)

Tactic:
simp

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)
i : Fin n
IH : ↑(Fin.natAdd m i) ≤ m → (M ↑(Fin.natAdd m i)).det = M₂.det
hi : m + ↑i + 1 ≤ m
⊢ m + ↑i + (k + m) = m + (↑i + (k + m))
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 (app f ↑U) ≫ IsAffineOpen.fromSpec ⋯ = (f ⁻¹ᵁ ↑U).ι ≫ f

Tactic:
simp

Goal state after:
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)
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})
⊢ r ∈ ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})

Tactic:
simp

Goal state after:
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)
⊢ ∀ (i : ℕ), (monomial i) 0 = 0

Tactic:
simp

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

Goal state before:
pp: case succ.inl.left
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) 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 = r ^ ↑(Fin.castAdd n j₂) * M₂.det
hi : ↑(Fin.castAdd n j₂) + 1 ≤ m
⊢ r *
      Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
        (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂) =
    Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then r * g.coeff (↑j₁ - ↑j₁_1) else 0)
      (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂)

Tactic:
simp

Goal state after:
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)
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)
i : Fin n
⊢ f (MvPolynomial.X i.succ) ∈ ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ Fin.castAdd (n + 1) (Fin.last m) ∉ Finset.univ →
    (-1) ^ (↑(Fin.last ((m + 1).add n)) + ↑(Fin.castAdd (n + 1) (Fin.last m))) *
          f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) (Fin.castAdd (n + 1) (Fin.last m)) *
        ((f.sylvester g (m + 1) (n + 1)).submatrix (Fin.last ((m + 1).add n)).succAbove
            (Fin.castAdd (n + 1) (Fin.last m)).succAbove).det =
      0

Tactic:
simp

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

Goal state before:
pp: case succ.e_a.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (-1) ^ (m + 1 + n + m) = (-1) ^ (n + 1)

pp: case succ.e_a.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) (Fin.castAdd (n + 1) (Fin.last m)) = g.coeff (n + 1)

pp: case succ.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (f.sylvester g (m + 1) (n + 1)).submatrix (Fin.castSucc ∘ ⇑(finCongr ⋯))
      ((Fin.castAdd (n + 1) (Fin.last m)).succAbove ∘ ⇑(finCongr ⋯)) =
    f.sylvester g m (n + 1)

Tactic:
· trans (-1) ^ (2 * m + (n + 1))
      · congr 1; lia
      · simp [pow_add]

Goal state after:
case succ.e_a.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) (Fin.castAdd (n + 1) (Fin.last m)) = g.coeff (n + 1)

case succ.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (f.sylvester g (m + 1) (n + 1)).submatrix (Fin.castSucc ∘ ⇑(finCongr ⋯))
      ((Fin.castAdd (n + 1) (Fin.last m)).succAbove ∘ ⇑(finCongr ⋯)) =
    f.sylvester g m (n + 1)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n k : ℕ
hf : f.natDegree ≤ m
⊢ f.resultant g (m + 0) n = (-1) ^ (n * 0) * g.coeff n ^ 0 * f.resultant g m n

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
r : R
⊢ (C r).natDegree ≤ 0

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
r : R
⊢ (C r).natDegree ≤ 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
r : R
⊢ f.coeff m ^ n * f.resultant (C r) m 0 = f.coeff m ^ (0 + n) * r ^ m

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
n : ℕ
r : R
a✝ : Nontrivial R
s : R
hg✝ : (C s).natDegree ≤ n
hg : (C s).natDegree = 0
⊢ (X - C r).resultant (C s) 1 n = eval r (C s)

Tactic:
simp

Goal state after:
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))
⊢ ⊤ = (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑⟨U, hU⟩)) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ U

Tactic:
simp

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
g : R[X]
n : ℕ
r : R
hg✝ : g.natDegree ≤ n
a✝ : Nontrivial R
hg : g.natDegree > 0
⊢ (X - C r).resultant (C (eval r g)) 1 n = eval r g

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
m : ℕ
r : R
hf : f.natDegree ≤ m
⊢ (-1) ^ (m * 1) * eval r f = (-1) ^ m * eval r f

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
m : ℕ
r : R
hf : f.natDegree ≤ m
⊢ f.resultant (X + C r) m 1 = (-1) ^ m * eval (-r) f

Tactic:
rw [← resultant_X_sub_C_right f m (-r) hf, map_neg, sub_neg_eq_add]

Goal state after:
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
⊢ (Multiset.map (fun ij ↦ -1 * (ij.2 - ij.1)) (f.roots ×ˢ g.roots)).prod =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod

Tactic:
simp

Goal state after:
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
r : K[X]
hr' : r ≠ 0
hg : Monic 1
hg' : Splits 1
hf : (1 * r).Monic
hf' : (1 * r).Splits
hfg : natDegree 1 ≤ (1 * r).natDegree
hN : (1 * r).natDegree + natDegree 1 = n
H : natDegree 1 = 0
⊢ 0 ^ natDegree 1 * coeff 1 0 ^ (1 * r).natDegree =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((1 * r).roots ×ˢ roots 1)).prod

Tactic:
simp

Goal state after:
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
x : K
hx : x ∈ g.roots
⊢ x - x = 0

Tactic:
simp

Goal state after:
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
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
⊢ (map (algebraMap K L) g).natDegree + (map (algebraMap K L) r).natDegree < n

Tactic:
simp

Goal state after:
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
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
⊢ g.natDegree + r.natDegree < n
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base)) ↑k) ⋯).I₀
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ (f ⁻¹ᵁ ↑U).toSpecΓ ≫ Spec.map (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) ⋯) ≫ ⋯.fromSpec = (f ⁻¹ᵁ ↑U).ι ≫ f₁

Tactic:
simp

Goal state after: