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

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

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
⊢ ZariskisMainProperty R p
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr
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
this :
  ∀ {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 : R[X] →ₐ[R] S), f.Finite → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
⊢ ZariskisMainProperty R p

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 = ⊥
⊢ ZariskisMainProperty R p

Tactic:
·

Goal state after:
case inr
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
this :
  ∀ {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 : R[X] →ₐ[R] S), f.Finite → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
⊢ ZariskisMainProperty R p
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

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

Tactic:
·

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
n m : ℕ
i : Fin (m + 1 + n)
⊢ 0 < m + 1 + n

Tactic:
by lia

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
n m : ℕ
this : ∀ (i : Fin (m + 1 + n)), f.sylvester 0 (m + 1) n i ⟨0, ⋯⟩ = 0
⊢ 0 < m + 1 + n

Tactic:
by lia

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

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

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
⊢ f.resultant (g + f * (monomial k) r) m n = f.resultant g m n

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
n k : ℕ
hk : k + 0 ≤ n
hf : f.natDegree ≤ 0
⊢ f.resultant (g + f * (monomial k) r) 0 n = f.resultant g 0 n
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 ≤ m

Tactic:
by lia

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 < m + n

Tactic:
by lia

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 + k + m < m + n

Tactic:
by lia

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_1
R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : integralClosure R S = ⊥
hf : ¬conductor R (f X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
⊢ ZariskisMainProperty R (Ideal.under (↥f.range) p)

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
⊢ ∃ r ∉ Ideal.under (↥f.range) p, ⊥.saturation (Submonoid.powers ((algebraMap (↥f.range) S) r)) ⋯ = ⊤

Tactic:
·

Goal state after:
case refine_1
R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : integralClosure R S = ⊥
hf : ¬conductor R (f X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
⊢ ZariskisMainProperty R (Ideal.under (↥f.range) p)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.inl
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₁ j₂ : Fin (m + n)
IH : ↑j₂ ≤ m → (M ↑j₂).det = M₂.det
hi : ↑j₂ + 1 ≤ m
⊢ (if ↑j₂ = ↑j₂ then M₁ j₁ ⟨↑j₂, ⋯⟩ - r * f.sylvester g m n j₁ ⟨↑j₂ + (k + m), ⋯⟩
    else if ↑j₂ < ↑j₂ + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if ↑j₂ < ↑j₂ then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂

pp: case succ.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₂
i : ℕ
IH : i ≤ m → (M i).det = M₂.det
hi : i + 1 ≤ m
j₁ j₂ : Fin (m + n)
h : ↑j₂ ≠ i
⊢ (if ↑j₂ = i then M₁ j₁ ⟨i, ⋯⟩ - r * f.sylvester g m n j₁ ⟨i + (k + m), ⋯⟩
    else if ↑j₂ < i + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if ↑j₂ < i then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂

Tactic:
·

Goal state after:
case succ.inl
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₁ j₂ : Fin (m + n)
IH : ↑j₂ ≤ m → (M ↑j₂).det = M₂.det
hi : ↑j₂ + 1 ≤ m
⊢ (if ↑j₂ = ↑j₂ then M₁ j₁ ⟨↑j₂, ⋯⟩ - r * f.sylvester g m n j₁ ⟨↑j₂ + (k + m), ⋯⟩
    else if ↑j₂ < ↑j₂ + 1 then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂) =
    if ↑j₂ < ↑j₂ then M₁ j₁ j₂ else f.sylvester g m n j₁ j₂
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
⊢ ∃ r ∉ Ideal.under (↥f.range) p, ⊥.saturation (Submonoid.powers ((algebraMap (↥f.range) S) r)) ⋯ = ⊤

Tactic:
·

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
⊢ ∃ r ∉ Ideal.under (↥f.range) p, ⊥.saturation (Submonoid.powers ((algebraMap (↥f.range) S) r)) ⋯ = ⊤
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

Tactic:
by lia

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

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

Tactic:
by lia

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
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
⊢ ZariskisMainProperty R p

Tactic:
wlog H : integralClosure R S = ⊥
  · let inst : Algebra (integralClosure R S) (Localization.AtPrime p) :=
      OreLocalization.instAlgebra
    have inst : Algebra.WeaklyQuasiFiniteAt (integralClosure R S) p :=
      .of_restrictScalars R (integralClosure R S) _
    refine .restrictScalars (this p (aeval (f X)) ?_ (integralClosure_idem (R := R)))
    refine RingHom.Finite.of_comp_finite (f := mapRingHom (algebraMap R _)) ?_
    convert! (show f.toRingHom.Finite from hf)
    ext <;> simp [show ∀ x, f (C x) = algebraMap _ _ x from f.commutes]
  replace hf : ¬ conductor R (f X) ≤ p := by
    intro hp
    rw [← ‹p.IsPrime›.isRadical.radical_le_iff] at hp
    set J := (conductor R (f X)).radical
    have inst : (p.map (Ideal.Quotient.mk J)).IsPrime :=
      Ideal.map_isPrime_of_surjective Ideal.Quotient.mk_surjective (by simpa using hp)
    have inst : IsReduced (S ⧸ J) :=
        (Ideal.isRadical_iff_quotient_reduced _).mp (Ideal.radical_isRadical _)
    have inst : WeaklyQuasiFiniteAt R (p.map (Ideal.Quotient.mk J)) := by
      refine .of_surjectiveOnStalks p _ (Ideal.Quotient.mkₐ R _)
        (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective)
        ((Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective p).trans ?_).symm
      simpa [← RingHom.ker_eq_comap_bot]
    refine not_isStronglyTranscendental_of_weaklyQuasiFiniteAt ?_ (p.map (Ideal.Quotient.mk J))
      (isStronglyTranscendental_mk_radical_conductor H (f X) (by convert! hf; ext; simp))
    convert! (RingHom.Finite.of_surjective _ (Ideal.Quotient.mk_surjective (I := J))).comp hf
      using 1
    ext <;> simp [show ∀ x, f (C x) = algebraMap _ _ x from f.commutes, J]
  obtain ⟨x, hx, hxp⟩ := SetLike.not_le_iff_exists.mp hf
  replace hx (a : _) : x * a ∈ f.range := by simpa [← AlgHom.map_adjoin_singleton f] using hx a
  refine ZariskisMainProperty.trans (S := f.range) _ ?_ ?_
  · have : Algebra.WeaklyQuasiFiniteAt R (p.under f.range) := by
      let := Localization.AtPrime.algebraOfLiesOver (p.under f.range) p
      let e : Localization.AtPrime (p.under f.range) ≃ₐ[R] Localization.AtPrime p :=
        .ofBijective (IsScalarTower.toAlgHom _ _ _)
          (Localization.localRingHom_bijective_of_not_conductor_le hf
            (by simp [← AlgHom.map_adjoin_singleton f]) _)
      exact .of_algHom_localization _ _ e.symm.toAlgHom e.symm.surjective
    refine .of_adjoin_eq_top _ ⟨f X, X, rfl⟩ ?_
    simp [← (Subalgebra.map_injective (f := Subalgebra.val _) Subtype.val_injective).eq_iff,
      ← AlgHom.map_adjoin_singleton f, Subalgebra.range_val]
  · refine ⟨⟨x, by simpa using hx 1⟩, hxp, top_le_iff.mp fun s _ ↦ ⟨_, ⟨1, rfl⟩, ?_⟩⟩
    simpa [Algebra.mem_bot] using hx s

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.affineOpens
⊢ ((pullbackRestrictIsoRestrict f ↑U).hom ≫ (f ⁻¹ᵁ ↑U).ι) ≫ toNormalization f =
    (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U ≫ toNormalization f

pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).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 =
    (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U ≫ toNormalization f
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))
⊢ r * f.coeff (↑j₁ - ↑j₂ - k) = 0

pp: case pos
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 = r * f.coeff (↑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))
⊢ r * f.coeff (↑j₁ - ↑j₂ - k) = 0
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
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))
⊢ m < ↑j₁ - ↑j₂ - k

Tactic:
by lia

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

Goal state before:
pp: case pos
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 = r * f.coeff (↑j₁ - ↑j₂ - k)

Tactic:
·

Goal state after:
case pos
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 = r * f.coeff (↑j₁ - ↑j₂ - k)
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) < m + n

Tactic:
by lia

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
⊢ ↑i + (k + m) < n

Tactic:
by lia

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
x : ℕ
hx : x ∈ p.support
⊢ p.natDegree < n - m + 1

Tactic:
by lia

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 : ℕ
hk : p.natDegree + n ≤ m
hg : g.natDegree ≤ n
⊢ (f + g * p).resultant g m n = f.resultant g m n

Tactic:
rw [resultant_comm, resultant_add_mul_right _ _ _ _ _ hk hg, resultant_comm,
    ← mul_assoc, ← pow_add, mul_comm m n, ← two_mul, pow_mul]
  ring

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 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₂
i : ℕ
IH : i ≤ m → (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
⊢ i < m + n

Tactic:
by lia

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 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₂
i : ℕ
IH : i ≤ m → (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
j : Fin (m + n)
⊢ i < m + n

Tactic:
by lia

Goal state after: