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]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
⊢ 0 < m * q.natDegree

Tactic:
by simpa using ⟨by lia, minpoly.natDegree_pos hp⟩

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: S : Type u_2
inst✝⁴ : CommRing S
q : Ideal S
inst✝³ : q.IsPrime
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ H : WeaklyQuasiFiniteAt K q
⊢ Module.Finite K (Localization.AtPrime q)

Tactic:
Algebra.weaklyQuasiFiniteAt_iff,

Goal state after:
S : Type u_2
inst✝⁴ : CommRing S
q : Ideal S
inst✝³ : q.IsPrime
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : WeaklyQuasiFiniteAt K q
H : QuasiFinite K (Localization.AtPrime q ⧸ Ideal.map (algebraMap K (Localization.AtPrime q)) (Ideal.under K q))
⊢ Module.Finite K (Localization.AtPrime q)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_4
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
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
x : R[X]
⊢ ((AlgHom.restrictScalars R
            ((Ideal.Quotient.liftₐ (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))
                  (aeval (1 ⊗ₜ[R] f X)) ⋯).comp
              (Algebra.TensorProduct.lift
                (Algebra.ofId p.ResidueField
                  (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
                (f.liftOfSurjective hf
                  ((Ideal.Quotient.mkₐ R (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
                    (mapAlgHom (Algebra.ofId R p.ResidueField)))
                  ⋯)
                ⋯))).comp
        Algebra.TensorProduct.includeRight)
      (f x) =
    ((AlgHom.restrictScalars R (AlgHom.id p.ResidueField (p.Fiber S))).comp Algebra.TensorProduct.includeRight) (f x)

Tactic:
simpa using aeval_algHom_apply
      ((Algebra.TensorProduct.includeRight : S →ₐ[_] p.Fiber S).comp f) X x

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

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
P : Ideal ↑R
hP : P.IsPrime
this : LocallyQuasiFinite (Spec.map (CommRingCat.ofHom (algebraMap P.ResidueField (P.Fiber ↑S))))
⊢ Module.Finite P.ResidueField (P.Fiber ↑S)

Tactic:
by
    simp only [HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), CommRingCat.hom_ofHom,
      RingHom.quasiFinite_algebraMap] at this
    exact .of_quasiFinite

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
⊢ LocallyQuasiFinite f

Tactic:
by
  change id _ -- avoid typeclass synthesis from getting stuck on the wlog hypothesis.
  wlog hY : ∃ R, Y = Spec R
  · refine (IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩
    have (x : Y) : IsLocallyArtinian (f.fiber x) :=
      .of_locallyQuasiFinite (f.fiberToSpecResidueField x)
    refine (MorphismProperty.cancel_right_of_respectsIso @LocallyQuasiFinite _
      (Spec.map ((Y.affineCover.f i).residueFieldMap _))).mp ?_
    let g : (pullback.snd f (Y.affineCover.f i)).fiber x ⟶ f.fiber (Y.affineCover.f i x) :=
      pullback.map _ _ _ _ (pullback.fst _ _) (Spec.map ((Y.affineCover.f i).residueFieldMap _))
        (Y.affineCover.f i) (by simp [pullback.condition]) (by simp)
    have : IsClosedImmersion g := .of_isPreimmersion _ (isClosed_discrete _)
    convert! (inferInstance : LocallyQuasiFinite <| g ≫ f.fiberToSpecResidueField _) using 1
    simp [g, Hom.fiberToSpecResidueField]
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S
  · refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦
      this _ _ (fun x ↦ ?_) ⟨_, rfl⟩
    have (x : _) : IsLocallyArtinian (f.fiber x) :=
      .of_locallyQuasiFinite (f.fiberToSpecResidueField x)
    let g : (X.affineCover.f i ≫ f).fiber x ⟶ f.fiber x :=
      pullback.map _ _ _ _ (X.affineCover.f i) (𝟙 _) (𝟙 _) (by simp) (by simp)
    have : IsClosedImmersion g := .of_isPreimmersion _ (isClosed_discrete _)
    convert (inferInstance : LocallyQuasiFinite <| g ≫ f.fiberToSpecResidueField _)
    simp [g, Hom.fiberToSpecResidueField]
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  algebraize [φ.hom]
  simp only [HasRingHomProperty.Spec_iff, id_eq]
  refine ⟨fun P hP ↦ ?_⟩
  suffices LocallyQuasiFinite (Spec.map <|
      CommRingCat.ofHom <| algebraMap P.ResidueField (P.Fiber S)) by
    simp only [HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), CommRingCat.hom_ofHom,
      RingHom.quasiFinite_algebraMap] at this
    exact .of_quasiFinite
  obtain ⟨x, rfl⟩ : ∃ x : Spec R, P = x.asIdeal := ⟨⟨P, hP⟩, rfl⟩
  refine (MorphismProperty.arrow_mk_iso_iff _ (Arrow.isoMk ?_ ?_ ?_)).mp (hf x)
  · refine asIso (pullback.map _ _ _ _ (𝟙 _) (Spec.map (Spec.residueFieldIso _ x).inv) (𝟙 _)
      ?_ ?_) ≪≫ pullbackSymmetry _ _ ≪≫ pullbackSpecIso ..
    · simp; rfl
    · simp [← Spec.map_comp, fromSpecResidueField, Spec.fromSpecStalk_eq]
  · exact asIso (Spec.map (Spec.residueFieldIso _ x).inv)
  · simp [Hom.fiberToSpecResidueField]

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

Goal state before:
pp: L : Type u_2
R : Type u_3
inst✝¹ : Field L
inst✝ : CommRing R
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
x : R[X]
⊢ (liftRingHom φ hφ) { toFractionRing := (algebraMap R[X] (FractionRing R[X])) x } = φ x

Tactic:
← Localization.mk_one_eq_algebraMap,

Goal state after:
L : Type u_2
R : Type u_3
inst✝¹ : Field L
inst✝ : CommRing R
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
x : R[X]
⊢ (liftRingHom φ hφ) { toFractionRing := Localization.mk x 1 } = φ x
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
x : ↥X
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
⊢ QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩}

Tactic:
obtain ⟨i, y, hy⟩ := Y.affineCover.exists_eq (f x)
    obtain ⟨x, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback _ _ hy.symm
    let ι := Y.affineCover.f i
    convert! this (f := pullback.snd f ι) (x := x) ⟨_, rfl⟩ using 1
    · exact (RingHom.QuasiFinite.respectsIso.arrow_mk_iso_iff
        (Scheme.stalkMapIsoOfIsPullback (.of_hasPullback f ι) x))
    have H : pullback.snd f ι ⁻¹' {pullback.snd f ι x} =
        pullback.fst f ι ⁻¹' f ⁻¹' {f (pullback.fst f ι x)} := by
      rw [← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ← Scheme.Hom.comp_apply,
        pullback.condition]
      simp [← Set.image_singleton, Set.preimage_comp, Set.preimage_image_eq _ ι.injective]
    let f' : pullback.snd f ι ⁻¹' {pullback.snd f ι x} → f ⁻¹' {f (pullback.fst f ι x)} :=
      Set.MapsTo.restrict (pullback.fst f ι) _ _ fun a ha ↦ H.le ha
    have : Topology.IsOpenEmbedding f' := by
      convert!
        (f ⁻¹' {f (pullback.fst f ι x)}).restrictPreimage_isOpenEmbedding
          (pullback.fst f ι).isOpenEmbedding using 0
      dsimp [f', Set.restrictPreimage]
      congr!
    rw [this.isOpen_iff_image_isOpen, Set.image_singleton]; rfl

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

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
f : K⟮X⟯
⊢ (map φ hφ) f = (algebraMap R[X] R⟮X⟯) (φ f.num) / (algebraMap R[X] R⟮X⟯) (φ f.denom)

Tactic:
rw [← num_div_denom f, map_apply_div_ne_zero, num_div_denom f]
  exact denom_ne_zero _

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case ha
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
e : MvPolynomial σ R ⊗[R] B ≃ₐ[MvPolynomial σ R] MvPolynomial σ B :=
  let __RingEquiv := e₀.toRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n (e x))
y : MvPolynomial σ R ⊗[R] ↥(integralClosure R B)
hy : (MvPolynomial.map (integralClosure R B).val.toRingHom) (e₁ y) = e x
i✝ : σ
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝
      ((((↑e₀).comp (Algebra.TensorProduct.map (AlgHom.id R (MvPolynomial σ R)) (integralClosure R B).val)).comp
          Algebra.TensorProduct.includeLeft)
        (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝
      ((((MvPolynomial.mapAlgHom (integralClosure R B).val).comp ↑e₁).comp Algebra.TensorProduct.includeLeft)
        (MvPolynomial.X i✝))

Tactic:
simp [e₀, e₁, MvPolynomial.coeff_map, MvPolynomial.coeff_one,
      apply_ite ((↑) : (integralClosure R B) → B)]

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case hb
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
e : MvPolynomial σ R ⊗[R] B ≃ₐ[MvPolynomial σ R] MvPolynomial σ B :=
  let __RingEquiv := e₀.toRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n (e x))
y : MvPolynomial σ R ⊗[R] ↥(integralClosure R B)
hy : (MvPolynomial.map (integralClosure R B).val.toRingHom) (e₁ y) = e x
x✝ : ↥(integralClosure R B)
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (((AlgHom.restrictScalars R
              ((↑e₀).comp (Algebra.TensorProduct.map (AlgHom.id R (MvPolynomial σ R)) (integralClosure R B).val))).comp
          Algebra.TensorProduct.includeRight)
        x✝) =
    MvPolynomial.coeff m✝
      (((AlgHom.restrictScalars R ((MvPolynomial.mapAlgHom (integralClosure R B).val).comp ↑e₁)).comp
          Algebra.TensorProduct.includeRight)
        x✝)

Tactic:
simp [e₀, e₁, MvPolynomial.coeff_map, MvPolynomial.coeff_one,
      apply_ite ((↑) : (integralClosure R B) → B)]

Goal state after:
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}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
a : S'
ham : a ∈ m
⊢ X - C a ∣ Polynomial.map (algebraMap S S') y - C ((aeval a) y)

Tactic:
simp [Polynomial.dvd_iff_isRoot]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case smul
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
n : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x✝ : S
a : R[X]
x : S
hx : x ∈ Submodule.span R[X] ↑s
IH : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
⊢ p.leadingCoeff ^ s.sup n • (t * a • x) ∈ φ.range

Tactic:
rw [mul_smul_comm, smul_comm, Algebra.smul_def]
    exact mul_mem (AlgHom.mem_range_self _ _) IH

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin n
⊢ (basisProd R m n) (Fin.natAdd m i) = (0, (basis R n) i)

Tactic:
rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_natAdd, Basis.prod_apply,
    Sum.elim_inr, LinearMap.coe_inr, Function.comp_apply]

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.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝² : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝¹ : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝ : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)

Tactic:
let : Algebra Γ(X, f ⁻¹ᵁ U.1) Γ(X, X.basicOpen (f.app _ r)) :=
      (X.presheaf.map (homOfLE (X.basicOpen_le _)).op).hom.toAlgebra

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝³ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝² : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝¹ : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (app f ↑U)) r)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
n : ℕ
r : R
hg : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ (X - C r).resultant g 1 n = eval r g

Tactic:
obtain hg | hg := g.natDegree.eq_zero_or_pos

Goal state after:
case inl
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

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
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]), p.Splits → P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
    Function.Injective ⇑φ → ∀ (p : R[X]), P (map φ p) → P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
    Function.Surjective ⇑φ → ∀ (p : S[X]), (∀ (q : R[X]), P q) → P p
R : Type u
inst✝ : CommRing R
p : R[X]
hR✝ : IsDomain R
hR : IsField R
this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]), IsDomain R → IsField R → p.Splits → P p
hp : ¬p.Splits
⊢ P p

pp: P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]), p.Splits → P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
    Function.Injective ⇑φ → ∀ (p : R[X]), P (map φ p) → P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
    Function.Surjective ⇑φ → ∀ (p : S[X]), (∀ (q : R[X]), P q) → P p
R : Type u
inst✝ : CommRing R
p : R[X]
hR✝ : IsDomain R
hR : IsField R
hp : p.Splits
⊢ P p

Tactic:
· let inst := hR.toField
    exact injective _ _ _ (algebraMap R p.SplittingField).injective _
      (this _ inferInstance (Field.toIsField _) (SplittingField.splits _))

Goal state after:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]), p.Splits → P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
    Function.Injective ⇑φ → ∀ (p : R[X]), P (map φ p) → P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
    Function.Surjective ⇑φ → ∀ (p : S[X]), (∀ (q : R[X]), P q) → P p
R : Type u
inst✝ : CommRing R
p : R[X]
hR✝ : IsDomain R
hR : IsField R
hp : p.Splits
⊢ P p
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ iU ≫ toNormalization f ≫ (normalizationCoprodIso f e).inv = toNormalization (iU ≫ f) ≫ coprod.inl

Tactic:
simp [← toNormalization_inl_normalizationCoprodIso_hom_assoc f e]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ toNormalization (pullback.snd f g) ≫ normalizationPullback f g ≫ pullback.fst (fromNormalization f) g =
    pullback.fst f g ≫ toNormalization f

Tactic:
simp [normalizationPullback]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
h : f.natDegree ≠ 0
⊢ f.resultant f = 0

Tactic:
by
  simp [resultant_self, h]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Subsingleton 𝓡'
⊢ IsCoprime 1 ↑(factor₂ m k hn p)

Tactic:
exact isCoprime_one_left

Goal state after:
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
⊢ ∃ s ∉ q,
    ∃ (hs : IsIntegral R s),
      (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
        ∀ (q' : Ideal ↥(integralClosure R S)),
          q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hs⟩ ∈ q'

Tactic:
have hs₃q : s₃.1 ∉ q := fun h ↦ (show ↑s₂ ^ m * (s₁ * ↑s₂ ^ n) ∉ q from q.primeCompl.mul_mem
     (pow_mem hs₂q _) (mul_mem hs₁q (pow_mem hs₂q _))) (hm ▸ Ideal.mul_mem_left _ _ 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
⊢ ∃ s ∉ q,
    ∃ (hs : IsIntegral R s),
      (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
        ∀ (q' : Ideal ↥(integralClosure R S)),
          q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hs⟩ ∈ q'