mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
hx : (aeval ((algebraMap R[X] J.ResidueField) X)) x = 0
r : R[X]
hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
⊢ ∃ s ∉ I, map (algebraMap R I.ResidueField) r = s • x

Tactic:
by
      obtain ⟨b, hb0, hb⟩ := IsLocalization.integerNormalization_spec (R ⧸ I)⁰ x
      obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective b
      refine ⟨s, by simpa [Ideal.Quotient.eq_zero_iff_mem] using! hb0, ?_⟩
      simpa [← hr, map_map, ← Ideal.Quotient.algebraMap_eq] using! hb

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
⊢ ∀ {α : Type w} [Fintype α],
    (∀ {f : MvPolynomial α S},
        (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f →
          ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial (Option α) S},
        (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f →
          ∀ (n : Option α →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
intro α

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
⊢ ∀ [Fintype α],
    (∀ {f : MvPolynomial α S},
        (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f →
          ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial (Option α) S},
        (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f →
          ∀ (n : Option α →₀ ℕ), IsIntegral R (coeff n f)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
⊢ (∀ {f : MvPolynomial α S},
      (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
    ∀ {f : MvPolynomial (Option α) S},
      (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f →
        ∀ (n : Option α →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
IH

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
⊢ ∀ {f : MvPolynomial (Option α) S},
    (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f →
      ∀ (n : Option α →₀ ℕ), IsIntegral R (coeff n f)
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ (aeval (x + (aeval x) P.f * -b)) P.f = 0

Tactic:
rw [Polynomial.aeval_add_of_sq_eq_zero _ _ _ (by grind)]

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ (aeval x) P.f + (aeval x) (derivative P.f) * ((aeval x) P.f * -b) = 0
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (aeval ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X))
      P.f =
    0

Tactic:
rw [aeval_algebraMap_apply, IsScalarTower.algebraMap_apply _ (Localization.Away P.g) (_ ⧸ _),
      Ideal.Quotient.algebraMap_eq, aeval_X_left_apply, Ideal.Quotient.mk_singleton_self]

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePresentation R S
f₁ f₂ : S →ₐ[R] T
h : f₁ P.x = f₂ P.x
⊢ f₁ = f₂

Tactic:
have : f₁.comp P.equivRing.symm.toAlgHom = f₂.comp P.equivRing.symm.toAlgHom :=
    P.P.hom_ext (by simpa)
  ext x
  obtain ⟨x, rfl⟩ := P.equivRing.symm.surjective x
  exact congr($this x)

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝¹ : Nontrivial R
P : Ideal R := Ideal.under R Q
this✝ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
this : ∃ q, q.Monic ∧ (aeval x) q = 0 ∧ (aeval x) (derivative q) ∉ Q
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨q, hq, hqx, hq'x⟩ := this

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
q : R[X]
hq : q.Monic
hqx : (aeval x) q = 0
hq'x : (aeval x) (derivative q) ∉ Q
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤

Tactic:
#adaptation_note /-- Needed after nightly-2023-02-23 -/

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁴ : p.IsPrime
this✝³ : Module p.ResidueField (p.Fiber S) := leftModule
this✝² : SMul p.ResidueField (p.Fiber S) := this✝³.toSMul
this✝¹ : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
hsQ' : (algebraMap R Q.ResidueField) s ≠ 0
hrQ' : φ r = 1
e' : (algebraMap R Q.ResidueField) s * φ x = (algebraMap S Q.ResidueField) t
⊢ t ∉ Q

Tactic:
rw [← Ideal.algebraMap_residueField_eq_zero, ← e']

Goal state after:
case refine_1
R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁴ : p.IsPrime
this✝³ : Module p.ResidueField (p.Fiber S) := leftModule
this✝² : SMul p.ResidueField (p.Fiber S) := this✝³.toSMul
this✝¹ : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
hsQ' : (algebraMap R Q.ResidueField) s ≠ 0
hrQ' : φ r = 1
e' : (algebraMap R Q.ResidueField) s * φ x = (algebraMap S Q.ResidueField) t
⊢ ¬(algebraMap R Q.ResidueField) s * φ x = 0
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
H : Unramified R S
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨S', hS', r, hrQ, hr⟩ := ZariskisMainProperty.of_finiteType (R := R) Q
    |>.exists_fg_and_exists_notMem_and_awayMap_bijective

Goal state after:
R✝ : Type u_1
S✝ : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
H : Unramified R S
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrQ : ↑r ∉ Q
hr : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ ((∏ a₁, (∏ x, if False then -1 else 1) * ∏ a₂, if ↑a₁ < n + ↑a₂ ∧ ¬m + ↑a₁ < ↑a₂ then -1 else 1) *
      ∏ a₂, (∏ a₁, if n + ↑a₂ < ↑a₁ ∧ ¬↑a₂ < m + ↑a₁ then -1 else 1) * ∏ x, if False then -1 else 1) =
    (-1) ^ (m * n)

Tactic:
simp [(Fin.isLt _).trans_le, (Fin.isLt _).le.trans, pow_mul]

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

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

Tactic:
simp only [Finset.range_zero, Finset.sum_empty]

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
g : R[X]
H : 0 ≤ n - m + 1
⊢ f.resultant (g + f * 0) m n = f.resultant g m n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

pp: case succ.hk
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ k + m ≤ n

pp: case succ.hf
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ f.natDegree ≤ m

Tactic:
IH

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ f.resultant g m n = f.resultant g m n

case succ.H
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ k ≤ n - m + 1

case succ.hk
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ k + m ≤ n

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

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

Tactic:
rw [resultant, Matrix.det_succ_row (i := .last _),
      Finset.sum_eq_single (by exact ((Fin.last m).castAdd (n + 1))) _ (by simp)]

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (-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 =
    (-1) ^ (n + 1) * g.coeff (n + 1) * f.resultant g m (n + 1)

R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ ∀ b ∈ Finset.univ,
    b ≠ Fin.castAdd (n + 1) (Fin.last m) →
      (-1) ^ (↑(Fin.last ((m + 1).add n)) + ↑b) * f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) b *
          ((f.sylvester g (m + 1) (n + 1)).submatrix (Fin.last ((m + 1).add n)).succAbove b.succAbove).det =
        0
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 * (ij.2 - ij.1)) (f.roots ×ˢ g.roots)).prod

Tactic:
Multiset.prod_map_mul

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.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
⊢ 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₁) ≫ Spec.map (app f₁ (g ⁻¹ᵁ ↑U)) ≫ ⋯.fromSpec

Tactic:
rw [app_eq_appLE, IsAffineOpen.SpecMap_appLE_fromSpec _ _ ((U.2.preimage _).preimage _)]

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
⊢ 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₁
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case hX
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
n m k : ℕ
hn : n = m + k
i✝ : Fin n
⊢ (Polynomial.map ((↑Algebra.TensorProduct.includeLeft).comp (map (algebraMap R S))) (freeMonic R m) *
          Polynomial.map ((↑Algebra.TensorProduct.includeRight).comp (map (algebraMap R S))) (freeMonic R k)).coeff
      ↑i✝ =
    (Polynomial.map
            ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
                    ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
                    ⋯)).comp
              ↑Algebra.TensorProduct.includeLeft)
            (freeMonic R m) *
          Polynomial.map
            ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
                    ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
                    ⋯)).comp
              ↑Algebra.TensorProduct.includeRight)
            (freeMonic R k)).coeff
      ↑i✝

Tactic:
congr 2 <;> ext <;> simp

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

Goal state before:
pp: case insert
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
f : ι → R[X]
g : R[X]
n : ℕ
hn : g.natDegree ≤ n
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∏ i ∈ s, (f i).leadingCoeff ≠ 0 →
    (∏ i ∈ s, f i).resultant g (∏ i ∈ s, f i).natDegree n = ∏ i ∈ s, (f i).resultant g (f i).natDegree n
hf : ∏ i ∈ insert a s, (f i).leadingCoeff ≠ 0
hf' : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (f a).resultant g (f a).natDegree n * (∏ x ∈ s, f x).resultant g (∏ x ∈ s, f x).natDegree n =
    ∏ i ∈ insert a s, (f i).resultant g (f i).natDegree n

Tactic:
IH hf',

Goal state after:
case insert
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
f : ι → R[X]
g : R[X]
n : ℕ
hn : g.natDegree ≤ n
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∏ i ∈ s, (f i).leadingCoeff ≠ 0 →
    (∏ i ∈ s, f i).resultant g (∏ i ∈ s, f i).natDegree n = ∏ i ∈ s, (f i).resultant g (f i).natDegree n
hf : ∏ i ∈ insert a s, (f i).leadingCoeff ≠ 0
hf' : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (f a).resultant g (f a).natDegree n * ∏ i ∈ s, (f i).resultant g (f i).natDegree n =
    ∏ i ∈ insert a s, (f i).resultant g (f i).natDegree n