mathlib-initiative/mathlib-tactics huggingface dataset:
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
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i✝ : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
H : ∀ {x : S}, x ∈ m → p.IsRoot x
i : ℕ
x : S
hx : x ∈ m
hi : i < Multiset.count (X - C x) (Multiset.map (fun x ↦ X - C x) m)
⊢ ∀ (j : ℕ), IsIntegral R (⟨X - C x, ⟨i, hi⟩⟩.fst.coeff j)

Tactic:
simp [coeff_X, coeff_C, IsIntegral.sub, apply_ite (IsIntegral R),
    isIntegral_one, isIntegral_zero, hpr x (H hx)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hx : x ∈ U
⊢ ∃ U_1 f, (Sieve.coverByImage (toOpensFunctor X) U).arrows f ∧ x ∈ U_1

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open hx U.2

Goal state after:
X : Scheme
U : X.Opens
x : ↥X
hx : x ∈ U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ∃ U_1 f, (Sieve.coverByImage (toOpensFunctor X) U).arrows f ∧ x ∈ U_1
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case refine_3
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ (asIso
            (pullback.map (Spec.map φ) ((Spec R).fromSpecResidueField x)
              (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S)))
              (Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField))) (𝟙 (Spec S))
              (Spec.map (Spec.residueFieldIso R x).inv) (𝟙 (Spec R)) ⋯ ⋯) ≪≫
          pullbackSymmetry (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S)))
              (Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField))) ≪≫
            pullbackSpecIso (↑R) x.asIdeal.ResidueField ↑S).hom ≫
      (Arrow.mk (Spec.map (CommRingCat.ofHom (algebraMap x.asIdeal.ResidueField (x.asIdeal.Fiber ↑S))))).hom =
    (Arrow.mk (Hom.fiberToSpecResidueField (Spec.map φ) x)).hom ≫ (asIso (Spec.map (Spec.residueFieldIso R x).inv)).hom

Tactic:
· simp [Hom.fiberToSpecResidueField]

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

Goal state before:
pp: 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₀⁰
⊢ 1 / 1 = 1

Tactic:
div_one

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

Goal state before:
pp: K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] K⟮X⟯) p) / (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] K⟮X⟯) q) =
    φ p / φ q

Tactic:
by
  rw [← map_div₀, liftMonoidWithZeroHom_apply_div]

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

Goal state before:
pp: case e'_2
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
H : ⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x} = ⇑(pullback.fst f ι) ⁻¹' ⇑f ⁻¹' {f ((pullback.fst f ι) x)}
f' : ↑(⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x}) → ↑(⇑f ⁻¹' {f ((pullback.fst f ι) x)}) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι)) (⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x})
    (⇑f ⁻¹' {f ((pullback.fst f ι) x)}) ⋯
this : Topology.IsOpenEmbedding f'
⊢ IsOpen {⟨(pullback.fst f (Y.affineCover.f i)) x, ⋯⟩} ↔ IsOpen {⟨x, ⋯⟩}

Tactic:
this.isOpen_iff_image_isOpen,

Goal state after:
case e'_2
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
H : ⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x} = ⇑(pullback.fst f ι) ⁻¹' ⇑f ⁻¹' {f ((pullback.fst f ι) x)}
f' : ↑(⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x}) → ↑(⇑f ⁻¹' {f ((pullback.fst f ι) x)}) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι)) (⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x})
    (⇑f ⁻¹' {f ((pullback.fst f ι) x)}) ⋯
this : Topology.IsOpenEmbedding f'
⊢ IsOpen {⟨(pullback.fst f (Y.affineCover.f i)) x, ⋯⟩} ↔ IsOpen (f' '' {⟨x, ⋯⟩})
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).numDenom =
    (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q), C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))

Tactic:
by
  rw [numDenom, liftOn'_div, if_neg hq]
  intro p
  rw [if_pos rfl, if_neg (one_ne_zero' K[X])]
  simp

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

Goal state before:
pp: case inr
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
H : ∃ x, R[x] = ⊤
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
have := (algebraMap R S).domain_nontrivial

Goal state after:
case inr
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
H : ∃ x, R[x] = ⊤
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this : Nontrivial R
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
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
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
⊢ f.natDegree ≠ 0

Tactic:
ne_eq,

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
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
⊢ ¬f.natDegree = 0
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
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
⊢ (aeval ((algebraMap S S') (φ X))).IsIntegralElem ((algebraMap S S') t)

Tactic:
obtain ⟨q, hqm, hq⟩ := ht

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]
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
⊢ (aeval ((algebraMap S S') (φ X))).IsIntegralElem ((algebraMap S S') t)
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
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
⊢ (Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)) ∈
    Algebra.adjoin S ↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B))

Tactic:
have hfg : IsIntegral R (AdjoinRoot.mk 𝓟'.f 𝓟'.g) := by
    have := 𝓟.monic_f.finite_adjoinRoot
    let e : AdjoinRoot 𝓟.f →ₐ[R] AdjoinRoot 𝓟'.f :=
      AdjoinRoot.mapAlgHom (Algebra.ofId _ _) _ _ (dvd_refl _)
    convert! (Algebra.IsIntegral.isIntegral (R := R) (AdjoinRoot.mk 𝓟.f 𝓟.g)).map e
    have : (AdjoinRoot.mk 𝓟'.f).comp (mapRingHom (algebraMap R B)) =
        e.toRingHom.comp (AdjoinRoot.mk _) := by ext <;> simp [e]
    exact congr($this 𝓟.g)

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
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hfg : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
⊢ (Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)) ∈
    Algebra.adjoin S ↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B))
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case h₁
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 = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
x✝ : R
⊢ ((aeval ((Ideal.Quotient.mk (conductor R (f X)).radical) (f X))).comp C) x✝ =
    (((Ideal.Quotient.mk J).comp f.toRingHom).comp C) x✝

Tactic:
simp [show ∀ x, f (C x) = algebraMap _ _ x from f.commutes, J]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case h₂
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 = ⊥
J : Ideal S := ⋯
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
⊢ (aeval ((Ideal.Quotient.mk (conductor R (f X)).radical) (f X))).toRingHom X =
    ((Ideal.Quotient.mk J).comp f.toRingHom) X

Tactic:
simp [show ∀ x, f (C x) = algebraMap _ _ x from f.commutes, J]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap f.base.hom') ↑k) ⋯).I₀
⊢ (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
        (normalizationOpenCover f).f U ≫ fromNormalization f =
    (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap f.base.hom') ↑k) ⋯).f U ≫ f

Tactic:
f.ι_fromNormalization,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap f.base.hom') ↑k) ⋯).I₀
⊢ (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
        Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U)) ≫ IsAffineOpen.fromSpec ⋯ =
    (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap f.base.hom') ↑k) ⋯).f U ≫ f
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
⊢ (C r * f).resultant g m n = r ^ n * f.resultant g m n

Tactic:
by
  rw [resultant_comm, resultant_C_mul_right, resultant_comm, mul_left_comm, ← mul_assoc ((-1) ^ _),
    mul_comm n m, ← mul_pow, neg_one_mul, neg_neg, one_pow, one_mul]

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.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U
⊢ app (fromNormalization f) U ≫ app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U) =
    (CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
        (normalizationObjIso f hU).inv) ≫
      app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U)

Tactic:
← Scheme.Hom.comp_app,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U
⊢ app ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) U =
    (CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
        (normalizationObjIso f hU).inv) ≫
      app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U)
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)
⊢ (Polynomial.map (↑Algebra.TensorProduct.includeLeft) (freeMonic R m) *
        Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k)).natDegree =
    n

Tactic:
((monic_freeMonic R m).map _).natDegree_mul ((monic_freeMonic R k).map _)

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)).natDegree +
      (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k)).natDegree =
    n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

Tactic:
natDegree_C_mul (by simp [hf0]),

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
wlog hR : IsField R
  · let K := FractionRing R
    apply FaithfulSMul.algebraMap_injective R K
    have := this (f.map (algebraMap R K)) (g.map (algebraMap R K)) n (natDegree_map_le.trans hg)
      (hf.map _) (Field.toIsField _)
    simp only [resultant_map_map, natDegree_map_eq_of_injective, leadingCoeff_map_of_injective,
      FaithfulSMul.algebraMap_injective R K, ← hf.natDegree_eq_card_roots,
      ← roots_map_of_injective_of_card_eq_natDegree] at this
    simpa [map_multiset_prod, aeval_algebraMap_apply, Multiset.map_map] using this
  by_cases hf0 : f = 0
  · simp [hf0]
  wlog hfm : f.Monic
  · let inst := hR.toField
    have H : (C f.leadingCoeff⁻¹ * f).Monic := by
      rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hf0]), coeff_C_mul]; simp [hf0]
    have := this (C f.leadingCoeff⁻¹ * f) g n hg (.mul (.C _) hf) hR (by simpa) H
    simpa [hf0, natDegree_C_mul, resultant_C_mul_left, inv_mul_eq_iff_eq_mul₀, roots_C_mul,
      H.leadingCoeff] using this
  simp only [hfm.leadingCoeff, one_pow, one_mul]
  clear hf0
  by_cases hg0 : g = 0
  · subst hg0
    by_cases hf' : f.natDegree = 0
    · obtain ⟨r, rfl⟩ := hfm.natDegree_eq_zero.mp hf'; simp
    simp [← hf.natDegree_eq_card_roots, hf']
  wlog hgm : g.Monic
  · let inst := hR.toField
    have := this f (C g.leadingCoeff⁻¹ * g) n (by simpa [hg0, natDegree_C_mul]) hf hR hfm (by simpa)
      (by rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hg0]), coeff_C_mul]; simp [hg0])
    rw [resultant_C_mul_right, inv_pow, inv_mul_eq_iff_eq_mul₀ (by simp [hg0])] at this
    simpa [← hf.natDegree_eq_card_roots, inv_pow, mul_left_comm (_ ^ g.natDegree), hg0] using this
  let inst := hR.toField
  let L := g.SplittingField
  apply (algebraMap R L).injective
  have := resultant_eq_prod_roots_sub (f.map (algebraMap R L))
    (g.map (algebraMap R L)) (hfm.map _) (hgm.map _) (hf.map _) (SplittingField.splits _)
  simp_rw [natDegree_map] at this
  rw [← resultant_map_map, ← Nat.add_sub_cancel' hg, resultant_add_right_deg _ _ _ _ _ (by simp),
    this, coeff_map, coeff_natDegree, hfm.leadingCoeff, map_one, one_pow, one_mul,
    map_sub_sprod_roots_eq_prod_map_eval _ _ (hgm.map _) (SplittingField.splits _),
    hf.roots_map, map_multiset_prod, Multiset.map_map]
  simp only [eval_map_algebraMap, Function.comp_apply, Multiset.map_map, L]
  congr; ext; simp [aeval_algebraMap_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f₁ f₂ g : R[X]
n : ℕ
hn : g.natDegree ≤ n
⊢ (f₁ * f₂).resultant g (f₁.natDegree + f₂.natDegree) n = f₁.resultant g f₁.natDegree n * f₂.resultant g f₂.natDegree n

Tactic:
rw [resultant_comm, resultant_mul_right _ _ _ n hn, resultant_comm, resultant_comm f₂]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f₁ f₂ g : R[X]
n : ℕ
hn : g.natDegree ≤ n
⊢ (-1) ^ ((f₁.natDegree + f₂.natDegree) * n) *
      ((-1) ^ (n * f₁.natDegree) * f₁.resultant g f₁.natDegree n * g.resultant f₂ n) =
    f₁.resultant g f₁.natDegree n * ((-1) ^ (f₂.natDegree * n) * g.resultant f₂ n)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
H₂ : ∀ (i : Fin k), (universalFactorizationMap R n m k hn).IsIntegralElem (1 ⊗ₜ[R] X i)
⊢ (universalFactorizationMap R n m k hn).IsIntegralElem 0

Tactic:
exact RingHom.isIntegralElem_zero _

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
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:
by
  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: