mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inl
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Subsingleton R
⊢ φ q / φ q = φ p' / φ q'

Tactic:
Subsingleton.elim p' q,

Goal state after:
case inl
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Subsingleton R
⊢ φ q / φ q = φ q / φ q'
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
⊢ (∀ (U : X.AffineZariskiSite) (f : ↑Γ(X, ↑U)),
      IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
        (F.map (homOfLE ⋯).op)) ↔
    ∀ (U : X.AffineZariskiSite) (f : ↑Γ(X, ↑U)),
      IsLocalization.Away ((ConcreteCategory.hom (α.app (Opposite.op U))) f) ↑(F.obj (Opposite.op (U.basicOpen f)))

Tactic:
refine forall₂_congr fun U f ↦ ?_

Goal state after:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : ↑Γ(X, ↑U)
⊢ IsPushout (X.presheaf.map (homOfLE ⋯).op) (α.app (Opposite.op U)) (α.app (Opposite.op (U.basicOpen f)))
      (F.map (homOfLE ⋯).op) ↔
    IsLocalization.Away ((ConcreteCategory.hom (α.app (Opposite.op U))) f) ↑(F.obj (Opposite.op (U.basicOpen f)))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)).QuasiFinite
algInst✝ : Algebra ↑(X.presheaf.obj (Opposite.op V)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).toAlgebra
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hxV⟩)) (hV.primeIdealOf ⟨x, hxV⟩).asIdeal
e : ↑(X.presheaf.stalk ↑⟨x, hxV⟩) ≃ₐ[↑Γ(X, V)] Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal :=
  IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hxV⟩).asIdeal.primeCompl (↑(X.presheaf.stalk ↑⟨x, hxV⟩))
    (Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal)
⊢ Algebra.QuasiFinite (↑Γ(Y, U)) (Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal)

Tactic:
← RingHom.quasiFinite_algebraMap

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)).QuasiFinite
algInst✝ : Algebra ↑(X.presheaf.obj (Opposite.op V)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).toAlgebra
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hxV⟩)) (hV.primeIdealOf ⟨x, hxV⟩).asIdeal
e : ↑(X.presheaf.stalk ↑⟨x, hxV⟩) ≃ₐ[↑Γ(X, V)] Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal :=
  IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hxV⟩).asIdeal.primeCompl (↑(X.presheaf.stalk ↑⟨x, hxV⟩))
    (Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal)
⊢ (algebraMap (↑Γ(Y, U)) (Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal)).QuasiFinite
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case _pq
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
c : R
p q : K[X]
hq : q ≠ 0
⊢ RatFunc.mk (c • p) q =
    { toFractionRing := (algebraMap K[X] (FractionRing K[X])) ((algebraMap R K[X]) c) } * RatFunc.mk p q

Tactic:
mk_def_of_ne (c • p) hq,

Goal state after:
case _pq
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
c : R
p q : K[X]
hq : q ≠ 0
⊢ { toFractionRing := IsLocalization.mk' (FractionRing K[X]) (c • p) ⟨q, ⋯⟩ } =
    { toFractionRing := (algebraMap K[X] (FractionRing K[X])) ((algebraMap R K[X]) c) } * RatFunc.mk p q
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy : (Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x) = f ((pullback.fst f (Y.affineCover.f i)) x)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
⊢ ⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x} = ⇑(pullback.fst f ι ≫ f) ⁻¹' {f ((pullback.fst f ι) x)}

Tactic:
← Scheme.Hom.comp_apply,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy : (Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x) = f ((pullback.fst f (Y.affineCover.f i)) x)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
⊢ ⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x} = ⇑(pullback.fst f ι ≫ f) ⁻¹' {(pullback.fst f ι ≫ f) x}
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝ : (CommRingCat.Hom.hom φ).FiniteType
algInst✝ : Algebra ↑R ↑S := ⋯
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
this : Algebra (Localization.AtPrime (Ideal.under (↑R) x.asIdeal)) (Localization.AtPrime x.asIdeal) := ⋯
⊢ QuasiFiniteAt (Spec.map φ) x ↔
    Algebra.QuasiFinite (Localization.AtPrime (Ideal.under (↑R) x.asIdeal)) (Localization.AtPrime x.asIdeal)

Tactic:
← RingHom.quasiFinite_algebraMap

Goal state after:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝ : (CommRingCat.Hom.hom φ).FiniteType
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
this : Algebra (Localization.AtPrime (Ideal.under (↑R) x.asIdeal)) (Localization.AtPrime x.asIdeal) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↑R) x.asIdeal) x.asIdeal
⊢ QuasiFiniteAt (Spec.map φ) x ↔
    (algebraMap (Localization.AtPrime (Ideal.under (↑R) x.asIdeal)) (Localization.AtPrime x.asIdeal)).QuasiFinite
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 (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (a * p / (a * (C a.leadingCoeff⁻¹ * gcd p q))) =
      C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∧
    C (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))) =
      C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)

Tactic:
EuclideanDomain.mul_div_mul_cancel ha hdivp,

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 (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (p / (C a.leadingCoeff⁻¹ * gcd p q)) =
      C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∧
    C (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))) =
      C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : StandardEtalePair R
⊢ (aeval P.X) P.g * (Ideal.Quotient.mk (Ideal.span {C P.f, Y * C P.g - 1})) Y = 1

Tactic:
by
  have : aeval (R := R) P.X = (Ideal.Quotient.mkₐ _ _).comp Polynomial.CAlgHom := by
    ext; simp [StandardEtalePair.Ring, StandardEtalePair.X]
  rw [this]
  dsimp [StandardEtalePair.Ring]
  rw [← map_mul, ← map_one (Ideal.Quotient.mk _), ← sub_eq_zero, ← map_sub, mul_comm]
  exact Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span (Set.mem_insert_of_mem _ rfl))

Goal state after:
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]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this✝ : IsScalarTower R R[X] S
x : S
this : φ p * t * x ∈ φ.range
⊢ φ p * (t * x) ∈ φ.range

Tactic:
convert! this using 1

Goal state after:
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]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this✝ : IsScalarTower R R[X] S
x : S
this : φ p * t * x ∈ φ.range
⊢ φ p * (t * x) = φ p * t * x
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case 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
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ (conductor R (φ X)).radical
i : ℕ
this : ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.leadingCoeff • t ∈ (conductor R (φ X)).radical
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

Tactic:
induction hpn : p.natDegree using Nat.strong_induction_on generalizing p with
    | h n IH =>
    cases n with
    | zero =>
      obtain hi' | hi' := lt_or_ge p.natDegree i
      · simp [coeff_eq_zero_of_natDegree_lt hi']
      · simpa [← coeff_natDegree, hpn, show i = 0 by lia] using this _ hp
    | succ n =>
      obtain hi' | hi' := eq_or_ne i p.natDegree
      · simpa [hi'] using this _ hp
      have : φ p.eraseLead * t ∈ (conductor R (φ X)).radical := by
        simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ t]
        exact sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))
      simpa [eraseLead_coeff, hi'] using
        IH _ ((eraseLead_natDegree_le _).trans_lt (by lia)) _ this rfl

Goal state after:
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✝² : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this✝ : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra (↥R') L := adjoin ↥R' ↑(algebraMap S L).range
f : S →ₐ[R] ↥S' := (IsScalarTower.toAlgHom R S L).codRestrict (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
⊢ g.range = ⊤

Tactic:
← (Subalgebra.map_injective (f := S'.val) Subtype.val_injective).eq_iff,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this✝ : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra (↥R') L := adjoin ↥R' ↑(algebraMap S L).range
f : S →ₐ[R] ↥S' := (IsScalarTower.toAlgHom R S L).codRestrict (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
⊢ Subalgebra.map S'.val g.range = Subalgebra.map S'.val ⊤
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
⊢ (normalizationOpenCover f).f ⟨U, hU⟩ ''ᵁ ⊤ = fromNormalization f ⁻¹ᵁ U

Tactic:
simpa using! (f.fromNormalization_preimage ⟨U, hU⟩).symm

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

Goal state before:
pp: case succ.e_a.right
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
⊢ Fin.addCases (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (n + 1) then g.coeff (↑i - ↑j₁) else 0)
      (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (m + 1) then f.coeff (↑i - ↑j₁) else 0)
      ((Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j))) =
    Fin.addCases (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (n + 1) then g.coeff (↑i - ↑j₁) else 0)
      (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + m then f.coeff (↑i - ↑j₁) else 0) (Fin.natAdd m j)

Tactic:
have : ((Fin.last m).castAdd (n + 1)).succAbove ((j.natAdd m).cast (by grind)) =
          j.natAdd _ := by ext; simp [Fin.succAbove, Fin.lt_def, add_right_comm]

Goal state after:
case succ.e_a.right
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
⊢ Fin.addCases (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (n + 1) then g.coeff (↑i - ↑j₁) else 0)
      (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (m + 1) then f.coeff (↑i - ↑j₁) else 0)
      ((Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j))) =
    Fin.addCases (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (n + 1) then g.coeff (↑i - ↑j₁) else 0)
      (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + m then f.coeff (↑i - ↑j₁) else 0) (Fin.natAdd m j)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

Tactic:
resultant_add_left_deg _ _ _ _ _ (by simp),

Goal state after:
R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
r : R
⊢ (-1) ^ (n * m) * g.coeff n ^ m * (C r).resultant g 0 n = (-1) ^ ((0 + m) * n) * g.coeff n ^ (0 + m) * r ^ n
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 :
  (algebraMap K L) ((f %ₘ g).leadingCoeff ^ g.natDegree)⁻¹ *
      (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.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

Tactic:
map_inv₀,

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) ((f %ₘ g).leadingCoeff ^ g.natDegree))⁻¹ *
      (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.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.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
⊢ normalization f ⟶ T

Tactic:
by
  refine colimit.desc _
    { pt := _
      ι.app U := Spec.map (CommRingCat.ofHom ((f₁.appLE _ _ (by simp [H])).hom.codRestrict _
        fun x ↦ ?_)) ≫ (U.2.preimage f₂).fromSpec,
      ι.naturality := ?_ }
  · algebraize [(f.app U.1).hom, (f₂.app U.1).hom,
      (f₁.appLE (f₂ ⁻¹ᵁ U.1) (f ⁻¹ᵁ U.1) (by simp [H])).hom]
    have : IsScalarTower Γ(Y, U.1) Γ(T, f₂ ⁻¹ᵁ U.1) Γ(X, f ⁻¹ᵁ U.1) := .of_algebraMap_eq' <| by
      simp only [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
        Hom.app_eq_appLE, Hom.appLE_comp_appLE, ← H]
    exact .algebraMap (R := Γ(Y, U.1)) (B := Γ(X, f ⁻¹ᵁ U.1)) (f₂.isIntegral_app U.1 U.2 x)
  · intros U V i
    dsimp [normalizationGlueData, relativeGluingData]
    rw [Category.comp_id, ← Spec.map_comp_assoc, ← (V.2.preimage f₂).map_fromSpec (U.2.preimage f₂)
      (homOfLE (f₂.preimage_mono (Scheme.AffineZariskiSite.toOpens_mono i.le))).op,
      ← Spec.map_comp_assoc]
    congr 2
    ext i
    apply Subtype.ext
    dsimp [normalizationDiagram]
    simp only [← CommRingCat.comp_apply, appLE_map, map_appLE]

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

Goal state before:
pp: case refine_2
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
n m k : ℕ
hn✝ hn : n = m + k
a✝¹ : Nontrivial R
a✝ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m) Algebra.TensorProduct.includeLeft) *
        ↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
            Algebra.TensorProduct.includeRight)).natDegree =
    n

Tactic:
dsimp [mapEquivMonic]

Goal state after:
case refine_2
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
n m k : ℕ
hn✝ hn : n = m + k
a✝¹ : Nontrivial R
a✝ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (Polynomial.map (↑Algebra.TensorProduct.includeLeft) (freeMonic R m) *
        Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k)).natDegree =
    n
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
⊢ (pderiv (Sum.inl i)) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X j))) =
    if ↑j < ↑i then 0 else if h : ↑j - ↑i < k then X (Sum.inr ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = k then 1 else 0

Tactic:
by
  trans ∑ x ∈ Finset.antidiagonal ↑j,
    if h : x.2 < k then if x.1 < m ∧ x.1 = ↑i then X (Sum.inr ⟨x.2, h⟩) else 0
    else if x.2 = k ∧ x.1 < m ∧ x.1 = ↑i then 1 else 0
  · simp [universalFactorizationMap, mapEquivMonic, Polynomial.coeff_mul, coeff_freeMonic,
      apply_dite, apply_ite, ← Algebra.TensorProduct.one_def,
      Pi.single_apply, Fin.ext_iff, ← ite_and]
  · obtain h | h := lt_or_ge j.1 i.1
    · rw [Finset.sum_eq_zero, if_pos h]
      simp only [Finset.mem_antidiagonal, Prod.forall]
      intro a b hab
      simp [show a ≠ i by lia]
    rw [Finset.sum_eq_single ⟨i.1, j.1 - i.1⟩, if_neg h.not_gt]
    · simp
    · simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]
      intro a b e h
      simp [show a ≠ i by lia]
    · simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
⊢ (universalFactorizationMapPresentation R n m k hn).jacobian =
    (-1) ^ n *
      (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).resultant
        (Polynomial.map Algebra.TensorProduct.includeRight.toRingHom (freeMonic R k))

Tactic:
by
  cases subsingleton_or_nontrivial R
  · exact Subsingleton.elim _ _
  let := (universalFactorizationMap R n m k hn).toAlgebra
  rw [Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det,
    MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix]
  simp only [AlgHom.toRingHom_eq_coe, Matrix.det_neg, Matrix.det_transpose, Matrix.det_reindex_self,
    Algebra.Generators.algebraMap_apply, ← Polynomial.resultant.eq_def,
    Fintype.card_fin, map_mul, map_pow, map_neg, map_one]
  congr 1
  rw [← (aeval _).coe_toRingHom, ← Polynomial.resultant_map_map,
    Polynomial.map_map, Polynomial.map_map]
  congr 2
  · ext <;> simp [-algebraMap_apply, -AddMonoidAlgebra.coe_algebraMap, ← algebraMap_eq]
  · ext <;> simp [-algebraMap_apply, -AddMonoidAlgebra.coe_algebraMap, ← algebraMap_eq]
  · rw [(monic_freeMonic ..).natDegree_map, natDegree_freeMonic]
  · rw [(monic_freeMonic ..).natDegree_map, natDegree_freeMonic]

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

Goal state before:
pp: case neg.inl
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ (f.scaleRoots 0).resultant (g.scaleRoots 0) f.natDegree g.natDegree = 0 ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
scaleRoots_zero,

Goal state after:
case neg.inl
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ (f.leadingCoeff • X ^ f.natDegree).resultant (g.scaleRoots 0) f.natDegree g.natDegree =
    0 ^ (f.natDegree * g.natDegree) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.inl
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ (f.leadingCoeff • X ^ f.natDegree).resultant (g.scaleRoots 0) f.natDegree g.natDegree =
    0 ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
scaleRoots_zero,

Goal state after:
case neg.inl
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ (f.leadingCoeff • X ^ f.natDegree).resultant (g.leadingCoeff • X ^ g.natDegree) f.natDegree g.natDegree =
    0 ^ (f.natDegree * g.natDegree) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
⊢ (fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) =
    (Algebra.ofId R 𝓡).comp ((MvPolynomial.mapEquivMonic R R n).symm p)

Tactic:
let := (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
  let := ((MvPolynomial.mapEquivMonic R _ n).symm p).toAlgebra
  exact AlgHom.ext fun x ↦ (Algebra.TensorProduct.tmul_one_eq_one_tmul x).symm

Goal state after: