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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyQuasiFinite f
y : ↥Y
⊢ IsDiscrete (⇑f ⁻¹' {y})

Tactic:
by
  simpa [Scheme.Hom.range_fiberι] using
    (isDiscrete_univ_iff.mpr inferInstance).image (f.fiberι y).isEmbedding.toIsInducing

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : QuasiCompact f
y : ↥Y
⊢ (⇑f ⁻¹' {y}).Finite

Tactic:
simpa [Scheme.Hom.range_fiberι] using Set.finite_univ.image (f.fiberι y)

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p : K[X]
q✝ : K⟮X⟯
q r : K[X]
x✝ : r ≠ 0
⊢ RatFunc.mk (c • p • q) r = c • p • RatFunc.mk q r

Tactic:
mk_smul,

Goal state after:
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p : K[X]
q✝ : K⟮X⟯
q r : K[X]
x✝ : r ≠ 0
⊢ c • RatFunc.mk (p • q) r = c • p • RatFunc.mk q r
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
⊢ RatFunc.mk (c • p) q = c • ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q)

Tactic:
mk_smul,

Goal state after:
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
⊢ c • RatFunc.mk p q = c • ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ C (q.leadingCoeff / ((C a.leadingCoeff⁻¹).leadingCoeff * (gcd p q).leadingCoeff))⁻¹ *
        (p / (C a.leadingCoeff⁻¹ * gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (p / gcd p q) ∧
    C (q.leadingCoeff / ((C a.leadingCoeff⁻¹).leadingCoeff * (gcd p q).leadingCoeff))⁻¹ *
        (q / (C a.leadingCoeff⁻¹ * gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (q / gcd p q)

Tactic:
Polynomial.leadingCoeff_C,

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ C (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * (p / (C a.leadingCoeff⁻¹ * gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (p / gcd p q) ∧
    C (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * (q / (C a.leadingCoeff⁻¹ * gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (q / gcd p q)
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: 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 : (Ideal.Quotient.mkₐ R I) ((aeval x) P.g * a) = 1
⊢ ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)

Tactic:
← map_one
    (Ideal.Quotient.mkₐ R I),

Goal state after:
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 : (Ideal.Quotient.mkₐ R I) ((aeval x) P.g * a) = (Ideal.Quotient.mkₐ R I) 1
⊢ ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case e'_3.e'_8.h₁
R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
e : P.Fiber S ≃ₐ[P.ResidueField] P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I :=
  fiberEquivQuotient (aeval x) hx' P
a : R
⊢ e ((aeval (1 ⊗ₜ[R] x)) (C ((algebraMap R P.ResidueField) a))) =
    (Ideal.Quotient.mk (Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker ↑(aeval x))))
      (C ((algebraMap R P.ResidueField) a))

Tactic:
aeval_C,

Goal state after:
case e'_3.e'_8.h₁
R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
e : P.Fiber S ≃ₐ[P.ResidueField] P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I :=
  fiberEquivQuotient (aeval x) hx' P
a : R
⊢ e ((algebraMap P.ResidueField (P.ResidueField ⊗[R] S)) ((algebraMap R P.ResidueField) a)) =
    (Ideal.Quotient.mk (Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker ↑(aeval x))))
      (C ((algebraMap R P.ResidueField) a))
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
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝¹ : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this✝ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
have := IsLocalization.integralClosure (S := B) M (Rf := S) (Sf := S ⊗[R] B)

Goal state after:
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
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
⊢ Function.Bijective ⇑(toIntegralClosure R S B)
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
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
convert!
    (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (integralClosure R B) M)
        (S ⊗[R] integralClosure R B) (integralClosure S (S ⊗[R] B))).bijective

Goal state after:
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
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
⊢ ⇑(toIntegralClosure R S B) =
    ⇑(IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) (S ⊗[R] ↥(integralClosure R B))
        ↥(integralClosure S (S ⊗[R] B)))
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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hp : φ p * t ∈ φ.range
⊢ ∃ q, IsIntegral R (t - φ q)

Tactic:
by
  obtain ⟨r, hr : φ r = _⟩ := hp
  obtain rfl | hp1 := eq_or_ne p 1
  · exact ⟨r, by simp_all [isIntegral_zero]⟩
  exact ⟨_, isIntegral_of_isIntegralElem_of_monic_of_natDegree_lt φ (t - φ (r /ₘ p)) p (r %ₘ p)
    (ht.sub _ φ.isIntegralElem_map) hpm (natDegree_modByMonic_lt _ hpm hp1)
    (by simp [mul_sub, ← hr, sub_eq_iff_eq_add, ← map_mul, ← map_add, r.modByMonic_add_div])⟩

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr.h.succ.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : integralClosure R S = ⊥
hφ : φ.Finite
i : ℕ
this✝ : ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.leadingCoeff • t ∈ (conductor R (φ X)).radical
p : R[X]
hp : φ p * t ∈ (conductor R (φ X)).radical
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.natDegree = m → p.coeff i • t ∈ (conductor R (φ X)).radical
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
this : φ p.eraseLead * t ∈ (conductor R (φ X)).radical
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

Tactic:
simpa [eraseLead_coeff, hi'] using
        IH _ ((eraseLead_natDegree_le _).trans_lt (by lia)) _ this rfl

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
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsEtaleAt R Q
⊢ ∃ f ∉ Q, IsStandardEtale R (Localization.Away f)

Tactic:
by
  obtain ⟨f, hfQ, h⟩ := exists_etale_of_isEtaleAt (R := R) Q
  obtain ⟨g, hgQ, hg⟩ := IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn (R := R) Q
  have : Etale R (Localization.Away (f * g)) := by
    rw [← basicOpen_subset_etaleLocus_iff_etale] at h ⊢
    exact .trans (PrimeSpectrum.basicOpen_mul_le_left _ _) h
  exact ⟨f * g, ‹Q.IsPrime›.mul_notMem hfQ hgQ, (hg.of_dvd (by simp)).isStandardEtale⟩

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
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
hg : g₀ ∉ Ideal.map (algebraMap S (Localization.Away f)) p
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
obtain ⟨g, ⟨_, m, rfl⟩, hg₀⟩ := IsLocalization.exists_mk'_eq (.powers f) g₀

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
hg : g₀ ∉ Ideal.map (algebraMap S (Localization.Away f)) p
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ : IsLocalization.mk' (Localization.Away f) g ⟨(fun x ↦ f ^ x) m, ⋯⟩ = g₀
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)
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
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝⁸ : IsDomain S'
this✝⁷ : IsDomain R
this✝⁶ : Algebra.IsIntegral R R'
this✝⁵ : FaithfulSMul R' K
this✝⁴ : FaithfulSMul R R'
this✝³ : FaithfulSMul R' L
this✝² : FaithfulSMul R' S'
this✝¹ : IsIntegrallyClosedIn R' K
this✝ : IsIntegrallyClosed R'
g : R' ⊗[R] S →ₐ[R'] S' := TensorProduct.lift (ofId R' S') f ⋯
hf₃ : Function.Injective ⇑f
hf₄ : f.IsIntegral
H₁ : IsStronglyTranscendental R' (f x)
H₂ : (aeval (f x)).Finite
Q : Ideal S'
isPrime✝ : Q.IsPrime
hQ : PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime✝ } = { asIdeal := P, isPrime := inst✝¹ }
this : WeaklyQuasiFiniteAt R' (Ideal.comap g.toRingHom Q)
⊢ WeaklyQuasiFiniteAt R' Q

Tactic:
exact .of_surjectiveOnStalks (Q.comap g.toRingHom) _ g
    (RingHom.surjectiveOnStalks_of_surjective hf₁) rfl

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]
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, ⋯⟩
⊢ Fin.addCases
        (fun j₁_1 ↦
          if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) + (f * (monomial k) r).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₂) -
      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₂) + (k + m), ⋯⟩ =
    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₂)

Tactic:
simp only [Fin.addCases_left, Fin.val_castAdd, this, Fin.addCases_right, mul_ite,
            mul_zero, ← C_mul_X_pow_eq_monomial, ← mul_assoc, coeff_mul_X_pow', ite_add_zero,
            coeff_mul_C, add_assoc, add_eq_left, ← ite_and, ← mul_comm r, tsub_add_eq_tsub_tsub,
            add_sub_assoc, sub_eq_zero]

Goal state after:
case succ.inl.left
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, ⋯⟩
⊢ (if (↑j₂ ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + n) ∧ k ≤ ↑j₁ - ↑j₂ then r * f.coeff (↑j₁ - ↑j₂ - k) else 0) =
    if ↑j₂ + k ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₂ + (k + m) then r * f.coeff (↑j₁ - ↑j₂ - k) else 0
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
⊢ p.support ⊆ Finset.range (n - m + 1)

Tactic:
simp only [Finset.subset_iff, Finset.mem_range]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
⊢ ∀ ⦃x : ℕ⦄, x ∈ p.support → x < n - m + 1
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 g 1 n = eval r g

Tactic:
conv_lhs => rw [← g.modByMonic_add_div (X - C r)]

Goal state after:
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 (g %ₘ (X - C r) + (X - C r) * (g /ₘ (X - C r))) 1 n = eval r g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
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
this :
  (map (algebraMap K L) g).resultant (map (algebraMap K L) r) =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
⊢ f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod

Tactic:
rw [resultant_map_map, natDegree_map, natDegree_map, resultant_C_mul_right,
    map_mul, inv_pow, map_inv₀, inv_mul_eq_iff_eq_mul₀ (by simp [hr₀])] at this

Goal state after:
case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
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
this :
  (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (algebraMap K L) ((f %ₘ g).leadingCoeff ^ g.natDegree) *
      (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
⊢ f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : FiniteType R S
inst✝ : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : ↑s₂ ∉ q
hs₂ : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom s₂)
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  (Localization.awayMap (integralClosure R S).val.toRingHom s₂)
      (IsLocalization.mk' (Localization.Away s₂) s₃ ⟨(fun x ↦ s₂ ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away ((integralClosure R S).val.toRingHom s₂))) s₁
m : ℕ
hm : ↑s₂ ^ m * ↑s₃ = ↑s₂ ^ m * (s₁ * ↑s₂ ^ n)
hm0 : 0 < m
hs₃q : ↑s₃ ∉ q
q' : Ideal ↥(integralClosure R S)
x✝¹ : q'.IsPrime
hq'q : q' ≠ Ideal.under (↥(integralClosure R S)) q
x✝ : q'.LiesOver p
this : Algebra (↥(integralClosure R S)) (Localization.Away ↑s₂) := OreLocalization.instAlgebra
e : Localization.Away s₂ ≃ₐ[↥(integralClosure R S)] Localization.Away ↑s₂ :=
  AlgEquiv.ofBijective (Localization.awayMapₐ (ofId (↥(integralClosure R S)) S) s₂) hs₂
q's : Ideal (Localization.Away s₂) := Ideal.map (algebraMap (↥(integralClosure R S)) (Localization.Away s₂)) q'
H : ¬⟨↑s₂ ^ m * ↑s₃, ⋯⟩ ∈ q'
⊢ s₂ ∉ q'

Tactic:
contrapose H

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : FiniteType R S
inst✝ : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : ↑s₂ ∉ q
hs₂ : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom s₂)
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  (Localization.awayMap (integralClosure R S).val.toRingHom s₂)
      (IsLocalization.mk' (Localization.Away s₂) s₃ ⟨(fun x ↦ s₂ ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away ((integralClosure R S).val.toRingHom s₂))) s₁
m : ℕ
hm : ↑s₂ ^ m * ↑s₃ = ↑s₂ ^ m * (s₁ * ↑s₂ ^ n)
hm0 : 0 < m
hs₃q : ↑s₃ ∉ q
q' : Ideal ↥(integralClosure R S)
x✝¹ : q'.IsPrime
hq'q : q' ≠ Ideal.under (↥(integralClosure R S)) q
x✝ : q'.LiesOver p
this : Algebra (↥(integralClosure R S)) (Localization.Away ↑s₂) := OreLocalization.instAlgebra
e : Localization.Away s₂ ≃ₐ[↥(integralClosure R S)] Localization.Away ↑s₂ :=
  AlgEquiv.ofBijective (Localization.awayMapₐ (ofId (↥(integralClosure R S)) S) s₂) hs₂
q's : Ideal (Localization.Away s₂) := Ideal.map (algebraMap (↥(integralClosure R S)) (Localization.Away s₂)) q'
H : s₂ ∈ q'
⊢ ⟨↑s₂ ^ m * ↑s₃, ⋯⟩ ∈ q'