mathlib-initiative/mathlib-tactics huggingface dataset:
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
H : integralClosure R S = ⊥
hf : ¬conductor R (f X) ≤ p
x : S
hx : x ∈ conductor R (f X)
hxp : x ∉ p
a : S
⊢ x * a ∈ f.range

Tactic:
simpa using

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
H : integralClosure R S = ⊥
hf : ¬conductor R (f X) ≤ p
x : S
hx : x ∈ conductor R (f X)
hxp : x ∉ p
a : S
⊢ ∃ x_1, f x_1 = x * a
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
H : integralClosure R S = ⊥
hf : ¬conductor R (f X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
⊢ x ∈ f.range

Tactic:
simpa using

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
H : integralClosure R S = ⊥
hf : ¬conductor R (f X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
⊢ ∃ x_1, f x_1 = x
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_2
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
s : S
x✝ : s ∈ ⊤
⊢ (fun x_1 ↦ (algebraMap (↥f.range) S) ⟨x, ⋯⟩ ^ x_1) 1 * s ∈ ⊥

Tactic:
simpa using

Goal state after:
case refine_2
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
s : S
x✝ : s ∈ ⊤
⊢ ∃ y, f y = x * s
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ Set.range ⇑(fromNormalization f ⁻¹ᵁ ↑U).ι = Set.range ⇑((normalizationOpenCover f).f U)

Tactic:
simpa using

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ ⇑(fromNormalization f) ⁻¹' ↑↑U = Set.range ⇑((normalizationOpenCover f).f U)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (n + 1)
hb : Fin.natAdd (m + 1) i ≠ Fin.castAdd (n + 1) (Fin.last m)
⊢ f.sylvester g (m + 1) (n + 1) (Fin.last (m + 1 + n)) (Fin.natAdd (m + 1) i) = 0

Tactic:
simpa using

Goal state after:
case right
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (n + 1)
hb : Fin.natAdd (m + 1) i ≠ Fin.castAdd (n + 1) (Fin.last m)
⊢ ↑i ≤ m + 1 + n → m + 1 + n ≤ ↑i + (m + 1) → f.coeff (m + 1 + n - ↑i) = 0
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
⊢ r ≠ 0

Tactic:
simpa using

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
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
⊢ ¬r = 0
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
⊢ r ≠ 0

Tactic:
simpa using

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
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 = 0
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)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
this✝ : ZariskisMainProperty R (Ideal.under (↥R') p)
this : ⊤ ≤ R'.saturation (Submonoid.powers r) ⋯
⊢ ⊥.saturation (Submonoid.powers ((algebraMap (↥R') S) ⟨r, hrR'⟩)) ⋯ = ⊤

Tactic:
simpa using

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)
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✝ : ZariskisMainProperty R (Ideal.under (↥R') p)
this : ⊤ ≤ R'.saturation (Submonoid.powers r) ⋯
⊢ ∀ (x : S), ∃ a, r ^ a * x ∈ R'
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) r).natDegree ≤ (map (algebraMap K L) g).natDegree

Tactic:
simpa using

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
⊢ (f %ₘ g).natDegree ≤ g.natDegree
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegral X
⊢ ⊤ = closure (⇑(toNormalization f) '' Set.univ)

Tactic:
simpa using

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegral X
⊢ Set.univ = closure (Set.range fun a ↦ (toNormalization f) a)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FiniteType R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
this : Small.{u, v} S
r : Shrink.{u, v} S
hr : r ∉ Ideal.comap (Shrink.algEquiv R S).toRingEquiv.toRingHom p
H : ∀ (x : Shrink.{u, v} S), ∃ m, IsIntegral R (r ^ m * x)
x : S
m : ℕ
hm : IsIntegral R (r ^ m * (Shrink.algEquiv R S).symm x)
⊢ IsIntegral R ((Shrink.algEquiv R S) r ^ m * x)

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FiniteType R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
this : Small.{u, v} S
r : Shrink.{u, v} S
hr : r ∉ Ideal.comap (Shrink.algEquiv R S).toRingEquiv.toRingHom p
H : ∀ (x : Shrink.{u, v} S), ∃ m, IsIntegral R (r ^ m * x)
x : S
m : ℕ
hm : IsIntegral R (r ^ m * (Shrink.algEquiv R S).symm x)
⊢ IsIntegral R ((Shrink.algEquiv R S) r ^ m * x)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
this :
  (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))).range ≤
    (Localization.awayMapₐ (adjoin R t).val r').range
x : S
n : ℕ
⊢ ∃ a,
    (Localization.awayMap (adjoin R t).val.toRingHom r') a =
      IsLocalization.mk' (Localization.Away ((adjoin R t).val.toRingHom r')) x
        ⟨(fun x ↦ (adjoin R t).val.toRingHom r' ^ x) n, ⋯⟩

Tactic:
obtain ⟨y, hy : Localization.awayMap _ _ _ = _⟩ := this ⟨x, rfl⟩

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
this :
  (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))).range ≤
    (Localization.awayMapₐ (adjoin R t).val r').range
x : S
n : ℕ
y : Localization.Away r'
hy :
  (Localization.awayMap (adjoin R t).val.toRingHom r') y =
    (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))).toRingHom x
⊢ ∃ a,
    (Localization.awayMap (adjoin R t).val.toRingHom r') a =
      IsLocalization.mk' (Localization.Away ((adjoin R t).val.toRingHom r')) x
        ⟨(fun x ↦ (adjoin R t).val.toRingHom 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✝¹ : FiniteType R S
p : Ideal S
inst✝ : p.IsPrime
H✝ : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrp : ↑r ∉ p
H : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
this✝¹ : Module.Finite R ↥S'
this✝ : QuasiFinite R (Localization.Away r)
this : QuasiFinite R (Localization.Away ↑r)
f : Localization.Away ↑r →ₐ[S] Localization.AtPrime p := IsLocalization.Away.liftAlgHom ↑r ⋯
x s : S
hs : s ∈ p.primeCompl
⊢ IsUnit ((AlgHom.restrictScalars R f) ((algebraMap S (Localization.Away ↑r)) s))

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FiniteType R S
p : Ideal S
inst✝ : p.IsPrime
H✝ : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrp : ↑r ∉ p
H : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
this✝¹ : Module.Finite R ↥S'
this✝ : QuasiFinite R (Localization.Away r)
this : QuasiFinite R (Localization.Away ↑r)
f : Localization.Away ↑r →ₐ[S] Localization.AtPrime p := IsLocalization.Away.liftAlgHom ↑r ⋯
x s : S
hs : s ∈ p.primeCompl
⊢ IsUnit ((algebraMap S (Localization.AtPrime p)) s)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝² : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝¹ : IsAffineHom f₁
this✝ : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₁' : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂ : fromNormalization f ⁻¹ᵁ ↑U = f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂' : fromNormalization f ⁻¹ᵁ ↑U = f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₃ : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
this :
  appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) h₁ =
    (normalization f).presheaf.map (eqToHom h₂).op ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ ↑U) ≫ X.presheaf.map (eqToHom h₃).op
⊢ Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫ (normalizationOpenCover f).f U ≫ f₁ =
    Spec.map (appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) h₁) ≫ ⋯.fromSpec ≫ f₁

Tactic:
rw [this, f.toNormalization_app_preimage U]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝² : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝¹ : IsAffineHom f₁
this✝ : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₁' : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂ : fromNormalization f ⁻¹ᵁ ↑U = f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂' : fromNormalization f ⁻¹ᵁ ↑U = f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₃ : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
this :
  appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) h₁ =
    (normalization f).presheaf.map (eqToHom h₂).op ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ ↑U) ≫ X.presheaf.map (eqToHom h₃).op
⊢ Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫ (normalizationOpenCover f).f U ≫ f₁ =
    Spec.map
        ((normalization f).presheaf.map (eqToHom h₂).op ≫
          ((normalizationObjIso f ⋯).hom ≫
              CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val ≫ X.presheaf.map (eqToHom ⋯).op) ≫
            X.presheaf.map (eqToHom h₃).op) ≫
      ⋯.fromSpec ≫ f₁
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
this✝ :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R → f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
hR : ¬IsField R
K : Type u_1 := FractionRing R
this :
  (algebraMap R K) (f.resultant g f.natDegree n) =
    (algebraMap R K) f.leadingCoeff ^ n *
      (Multiset.map (fun x ↦ eval x (map (algebraMap R K) g)) (Multiset.map (⇑(algebraMap R K)) f.roots)).prod
⊢ (algebraMap R K) (f.resultant g f.natDegree n) =
    (algebraMap R K) (f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod)

Tactic:
simpa using

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
this✝ :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R → f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
hR : ¬IsField R
K : Type u_1 := FractionRing R
this :
  (algebraMap R K) (f.resultant g f.natDegree n) =
    (algebraMap R K) f.leadingCoeff ^ n *
      (Multiset.map (fun x ↦ eval x (map (algebraMap R K) g)) (Multiset.map (⇑(algebraMap R K)) f.roots)).prod
⊢ (algebraMap R K) (f.resultant g f.natDegree n) =
    (algebraMap R K) f.leadingCoeff ^ n * (Multiset.map (fun x ↦ (algebraMap R K) (eval x g)) f.roots).prod
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝² : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝¹ : IsAffineHom f₁
this✝ : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₁' : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂ : fromNormalization f ⁻¹ᵁ ↑U = f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂' : fromNormalization f ⁻¹ᵁ ↑U = f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₃ : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
this :
  appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) ⋯ =
    (normalization f).presheaf.map (eqToHom h₂').op ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ ↑U) ≫ X.presheaf.map (eqToHom h₃).op
⊢ Spec.map (appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) ⋯) ≫ ⋯.fromSpec ≫ f₂ =
    Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫ (normalizationOpenCover f).f U ≫ f₂

Tactic:
rw [this, f.toNormalization_app_preimage U]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝² : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝¹ : IsAffineHom f₁
this✝ : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₁' : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂ : fromNormalization f ⁻¹ᵁ ↑U = f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂' : fromNormalization f ⁻¹ᵁ ↑U = f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₃ : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
this :
  appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) ⋯ =
    (normalization f).presheaf.map (eqToHom h₂').op ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ ↑U) ≫ X.presheaf.map (eqToHom h₃).op
⊢ Spec.map
        ((normalization f).presheaf.map (eqToHom h₂').op ≫
          ((normalizationObjIso f ⋯).hom ≫
              CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val ≫ X.presheaf.map (eqToHom ⋯).op) ≫
            X.presheaf.map (eqToHom h₃).op) ≫
      ⋯.fromSpec ≫ f₂ =
    Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫ (normalizationOpenCover f).f U ≫ f₂
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
this✝ :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          ¬f = 0 →
            f.Monic → f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
hfm : ¬f.Monic
inst : Field R := hR.toField
H : (C f.leadingCoeff⁻¹ * f).Monic
this :
  (C f.leadingCoeff⁻¹ * f).resultant g (C f.leadingCoeff⁻¹ * f).natDegree n =
    (C f.leadingCoeff⁻¹ * f).leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) (C f.leadingCoeff⁻¹ * f).roots).prod
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
simpa using

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
this✝ :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          ¬f = 0 →
            f.Monic → f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
hfm : ¬f.Monic
inst : Field R := hR.toField
H : (C f.leadingCoeff⁻¹ * f).Monic
this :
  (C f.leadingCoeff⁻¹ * f).resultant g (C f.leadingCoeff⁻¹ * f).natDegree n =
    (C f.leadingCoeff⁻¹ * f).leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) (C f.leadingCoeff⁻¹ * f).roots).prod
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod