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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V, ∃ (_ : IsAffineOpen V) (hVU : V ≤ f ⁻¹ᵁ U), x ∈ V ∧ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).Smooth

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
  obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open hxU (U.2.preimage f.continuous)
  have := f.finitePresentation_appLE hU hV hVU
  algebraize [(f.appLE U V hVU).hom]
  have : Algebra.IsSmoothAt _ _ := (formallySmooth_stalkMap_iff U hU V hV hVU hxV).mp H
  obtain ⟨r, hrx, hr⟩ := Algebra.IsSmoothAt.exists_notMem_smooth Γ(Y, U)
    (hV.primeIdealOf ⟨x, hxV⟩).asIdeal
  refine ⟨_, hU, _, hV.basicOpen r, (X.basicOpen_le r).trans hVU, ?_, ?_⟩
  · rwa [← PrimeSpectrum.mem_basicOpen, IsAffineOpen.primeIdealOf,
      ← hV.fromSpec_preimage_basicOpen, Scheme.Hom.mem_preimage, ← Scheme.Hom.comp_apply,
      IsAffineOpen.isoSpec_hom, IsAffineOpen.toSpecΓ_fromSpec] at hrx
  · have := hV.isLocalization_basicOpen r
    rw [← RingHom.smooth_algebraMap] at hr
    convert!
      RingHom.Smooth.propertyIsLocal.respectsIso.1 _
        (IsLocalization.algEquiv (.powers r) _ Γ(X, X.basicOpen r)).toRingEquiv hr
    ext
    dsimp
    simp only [IsScalarTower.algebraMap_apply Γ(Y, U) Γ(X, V) (Localization _),
      IsLocalization.map_eq]
    simp only [algebraMap_toAlgebra, RingHomCompTriple.comp_apply, ← ConcreteCategory.comp_apply,
      Scheme.Hom.appLE_map]

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

Goal state before:
pp: X Y U : Scheme
f : U ⟶ X
g : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : LocallyOfFinitePresentation g
x : ↥U
⊢ ((CommRingCat.Hom.hom (stalkMap f x)).comp (CommRingCat.Hom.hom (stalkMap g (f x)))).FormallySmooth ↔
    x ∈ ↑(smoothLocus (f ≫ g))

Tactic:
← CommRingCat.hom_comp,

Goal state after:
X Y U : Scheme
f : U ⟶ X
g : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : LocallyOfFinitePresentation g
x : ↥U
⊢ (CommRingCat.Hom.hom (stalkMap g (f x) ≫ stalkMap f x)).FormallySmooth ↔ x ∈ ↑(smoothLocus (f ≫ g))
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: ⊢ @IsLocalIso = ⨅ P, ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
⊢ @IsLocalIso ≤ ⨅ P, ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P

case refine_2
⊢ ⨅ P, ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P ≤ @IsLocalIso
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
inst✝ : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis k fun i ↦ a ↑i
hn : n ∉ s
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' (insert n s \ {i})))) (a i)

Tactic:
let e₁ : {j : ↥(insert n s) // j ≠ ⟨n, by simp⟩} ≃ ↑s :=
    ⟨fun x ↦ ⟨x, by aesop⟩, fun x ↦ ⟨⟨x, by aesop⟩, by aesop⟩, fun _ ↦ rfl, fun _ ↦ rfl⟩

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
inst✝ : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis k fun i ↦ a ↑i
hn : n ∉ s
e₁ : { j // j ≠ ⟨n, ⋯⟩ } ≃ ↑s :=
  { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' (insert n s \ {i})))) (a i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: case inr
P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
R : CommRingCat
X Y✝ : Scheme
f : X ⟶ Spec R
g : Y✝ ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (pullback.fst f g)
this : ∀ {X : Scheme} (f : X ⟶ Spec R), (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → (∃ T, X = Spec T) → P g
hX : ¬∃ T, X = Spec T
x✝ : CompactSpace ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ P g

Tactic:
refine this (f := (Y.isoSpec.inv ≫ p) ≫ f) ?_ ?_ ⟨_, rfl⟩

Goal state after:
case inr.refine_1
P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
R : CommRingCat
X Y✝ : Scheme
f : X ⟶ Spec R
g : Y✝ ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (pullback.fst f g)
this : ∀ {X : Scheme} (f : X ⟶ Spec R), (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → (∃ T, X = Spec T) → P g
hX : ¬∃ T, X = Spec T
x✝ : CompactSpace ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ (P' ⊓ @QuasiCompact) ((Y.isoSpec.inv ≫ p) ≫ f)

case inr.refine_2
P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
R : CommRingCat
X Y✝ : Scheme
f : X ⟶ Spec R
g : Y✝ ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (pullback.fst f g)
this : ∀ {X : Scheme} (f : X ⟶ Spec R), (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → (∃ T, X = Spec T) → P g
hX : ¬∃ T, X = Spec T
x✝ : CompactSpace ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ P (pullback.fst ((Y.isoSpec.inv ≫ p) ≫ f) g)
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : g.IsStandardOpenImmersion
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.IsStandardOpenImmersion R S
algebraizeInst✝ : Algebra.IsStandardOpenImmersion S T
r : R
hr : IsLocalization.Away r S
⊢ (g.comp f).IsStandardOpenImmersion

Tactic:
obtain ⟨s, hs⟩ := hg

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.IsStandardOpenImmersion R S
algebraizeInst✝ : Algebra.IsStandardOpenImmersion S T
r : R
hr : IsLocalization.Away r S
s : S
hs : IsLocalization.Away s T
⊢ (g.comp f).IsStandardOpenImmersion
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

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 : IsStronglyTranscendental R x
q : Ideal S
hq : q ∈ minimalPrimes S
u : S
p : R[X]
e : (aeval ((Ideal.Quotient.mk q) x)) p * (Ideal.Quotient.mk q) u = 0
⊢ map (algebraMap R (S ⧸ q)) p * C ((Ideal.Quotient.mk q) u) = 0

Tactic:
← Ideal.Quotient.algebraMap_eq,

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 : IsStronglyTranscendental R x
q : Ideal S
hq : q ∈ minimalPrimes S
u : S
p : R[X]
e : (aeval ((algebraMap S (S ⧸ q)) x)) p * (algebraMap S (S ⧸ q)) u = 0
⊢ map (algebraMap R (S ⧸ q)) p * C ((Ideal.Quotient.mk q) u) = 0
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : n = 0
⊢ ∃ a, Valued.v a = n

pp: case neg
K : Type u_1
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ ∃ a, Valued.v a = n

Tactic:
· use 0; simp [hn0]

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ ∃ a, Valued.v a = n
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
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
p✝ : S[X]
hp✝ : IsAlmostIntegral R[X] p✝
i : ℕ
q : S[X]
p : R[X]
hp : p ∈ R[X]⁰
hp' : ∀ (n : ℕ), p • q ^ n ∈ (algebraMap R[X] S[X]).range
n : ℕ
⊢ p.leadingCoeff • q.leadingCoeff ^ n ∈ (algebraMap R S).range

Tactic:
obtain ⟨r, hr⟩ := hp' n

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
p✝ : S[X]
hp✝ : IsAlmostIntegral R[X] p✝
i : ℕ
q : S[X]
p : R[X]
hp : p ∈ R[X]⁰
hp' : ∀ (n : ℕ), p • q ^ n ∈ (algebraMap R[X] S[X]).range
n : ℕ
r : R[X]
hr : (algebraMap R[X] S[X]) r = p • q ^ n
⊢ p.leadingCoeff • q.leadingCoeff ^ n ∈ (algebraMap R S).range
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x : I.ResidueField[X]
⊢ x ∈ I.ResidueField[X]⁰ → x ∈ Submonoid.comap (aeval ((algebraMap R[X] J.ResidueField) X)) J.ResidueField⁰

Tactic:
suffices Function.Injective (aeval (R := I.ResidueField) (algebraMap R[X] J.ResidueField X)) by
      simp [← this.eq_iff]
    rw [injective_iff_map_eq_zero]
    intro x hx
    obtain ⟨r, hr⟩ := map_surjective _ Ideal.Quotient.mk_surjective
      (IsLocalization.integerNormalization (R ⧸ I)⁰ x)
    obtain ⟨s, hs, hr⟩ : ∃ s ∉ I, r.map (algebraMap _ _) = s • x := by
      obtain ⟨b, hb0, hb⟩ := IsLocalization.integerNormalization_spec (R ⧸ I)⁰ x
      obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective b
      refine ⟨s, by simpa [Ideal.Quotient.eq_zero_iff_mem] using! hb0, ?_⟩
      simpa [← hr, map_map, ← Ideal.Quotient.algebraMap_eq] using! hb
    replace hx : r ∈ J := by
      apply_fun aeval (algebraMap R[X] J.ResidueField X) at hr
      simpa [hx, aeval_map_algebraMap, aeval_algebraMap_apply, Algebra.smul_def] using! hr
    refine ((IsUnit.mk0 (algebraMap R I.ResidueField s) (by simpa)).map C).mul_right_injective ?_
    simp only [← algebraMap_eq, ← Algebra.smul_def]
    rw [algebraMap_smul]
    simp only [← hr]
    simpa [Polynomial.ext_iff, Ideal.mem_map_C_iff] using! hJ.le hx

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]
inst✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ ∀ (x y : R⟮X⟯), (↑(map φ hφ)).toFun (x + y) = (↑(map φ hφ)).toFun x + (↑(map φ hφ)).toFun y

Tactic:
by
      rintro ⟨x⟩ ⟨y⟩
      induction x using Localization.induction_on
      induction y using Localization.induction_on
      · simp only [← ofFractionRing_add, Localization.add_mk, map_add, map_mul,
          MonoidHom.toFun_eq_coe, map_apply_ofFractionRing_mk, Submonoid.coe_mul,
          -- We have to specify `S[X]⁰` to `mk_mul_mk`, otherwise it will try to rewrite
          -- the wrong occurrence.
          Submonoid.mk_mul_mk S[X]⁰]

Goal state after:
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)
⊢ algebraMap (↑Γ(Y, U)) (Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal) =
    e.toRingEquiv.toRingHom.comp
      ((CommRingCat.Hom.hom (stalkMap f x)).comp (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)))

Tactic:
← CommRingCat.hom_comp,

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) =
    e.toRingEquiv.toRingHom.comp (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯ ≫ stalkMap f x))
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ (q / gcd p q).leadingCoeff⁻¹ ≠ 0

Tactic:
· simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq

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

Goal state before:
pp: K : Type u
inst✝ : Field K
p : K[X]
⊢ ((algebraMap K[X] K⟮X⟯) p).denom = 1

Tactic:
convert! denom_div p one_ne_zero <;> simp

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

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ (q / gcd p q).leadingCoeff⁻¹ ≠ 0

Tactic:
· simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ IsUnit { toPresentation := P.toPresentation, map := id, map_inj := ⋯ }.jacobian

Tactic:
by simp [P.hasMap.2, P.hasMap.isUnit_derivative_f]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
p : Ideal S
r : S
h : IsIntegral R r
⊢ Submonoid.powers r ≤ (integralClosure R S).toSubmonoid

Tactic:
by simpa [Submonoid.powers_le]

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
hRS : integralClosure R S = ⊥
x : S
hx : (aeval x).Finite
u : S
p : R[X]
e : (aeval ((Ideal.Quotient.mk (conductor R x).radical) x)) p * (Ideal.Quotient.mk (conductor R x).radical) u = 0
⊢ map (algebraMap R (S ⧸ (conductor R x).radical)) p * C ((Ideal.Quotient.mk (conductor R x).radical) u) = 0

Tactic:
← Ideal.Quotient.algebraMap_eq,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
hRS : integralClosure R S = ⊥
x : S
hx : (aeval x).Finite
u : S
p : R[X]
e : (aeval ((algebraMap S (S ⧸ (conductor R x).radical)) x)) p * (algebraMap S (S ⧸ (conductor R x).radical)) u = 0
⊢ map (algebraMap R (S ⧸ (conductor R x).radical)) p * C ((Ideal.Quotient.mk (conductor R x).radical) u) = 0
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
i j : Fin n
hji : id j < id i
⊢ ((taylor r) ↑((degreeLT.basis R n) j)).coeff ↑i = 0

Tactic:
rw [degreeLT.basis_val, coeff_eq_zero_of_degree_lt (by simpa [-taylor_X_pow, -taylor_pow])]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case pos
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
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∈ p
a : R
ha : (ofId R S).toRingHom a = f.leadingCoeff • x
h✝ : n = m
⊢ (algebraMap R S) a ∈ p

Tactic:
convert p.mul_mem_right x Hfp

Goal state after:
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
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∈ p
a : R
ha : (ofId R S).toRingHom a = f.leadingCoeff • x
h✝ : n = m
⊢ (algebraMap R S) a = (algebraMap R S) f.leadingCoeff * x
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case neg
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
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∉ p
⊢ (fun x ↦ (algebraMap R S) f.leadingCoeff ^ x) 1 * x ∈ integralClosure R S

Tactic:
simpa [Algebra.smul_def] using! isIntegral_leadingCoeff_smul f x hf

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

Goal state before:
pp: case inr
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
⊢ f.resultant (g + f * (monomial k) r) m n = f.resultant g m n

Tactic:
let M (i : ℕ) : Matrix (Fin (m + n)) (Fin (m + n)) R :=
    .of fun j₁ j₂ ↦ if j₂.1 < i then M₁ j₁ j₂ else M₂ j₁ j₂

Goal state after:
case inr
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₂
⊢ f.resultant (g + f * (monomial k) r) m n = f.resultant g m n
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
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
⊢ f.resultant (C r * g) m n = r ^ m * f.resultant g m n

Tactic:
let M (i : ℕ) : Matrix (Fin (m + n)) (Fin (m + n)) R :=
    .of fun j₁ j₂ ↦ if j₂.1 < i then M₁ j₁ j₂ else M₂ j₁ j₂

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) 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₂
⊢ f.resultant (C r * g) m n = r ^ m * f.resultant g m n
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
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 : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝³ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝² : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝¹ : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
⊢ Function.Bijective ⇑(IsScalarTower.toAlgHom R (Localization.AtPrime (Ideal.under (↥R') p)) (Localization.AtPrime p))

Tactic:
refine Localization.localRingHom_bijective_of_saturated_inf_eq_top _ ?_ _
          rw [← top_le_iff, ← hs, Algebra.adjoin_le_iff]
          intro x hx
          refine ⟨r ^ (s.sup m), pow_mem (by exact ⟨hrp, hrR'⟩) _, Algebra.subset_adjoin ?_⟩
          simp [Set.smul_mem_smul_set hx, ← smul_eq_mul]

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

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

Tactic:
by
  rw [← zero_add n, resultant_add_right_deg _ _ _ _ _ (by simp)]
  simp

Goal state after: