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

Goal state before:
pp: P P' : MorphismProperty Scheme
inst✝³ : P'.RespectsIso
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g
X Y Z T : Scheme
inst✝ : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (pullback.fst f g)
⊢ P g

Tactic:
apply H ((T.isoSpec.inv ≫ p) ≫ f)
  · rw [Category.assoc, P'.cancel_left_of_respectsIso]
    exact P'.comp_mem _ _ hp h
  · rw [← pullbackRightPullbackFstIso_inv_fst f g (T.isoSpec.inv ≫ p),
        P.cancel_left_of_respectsIso]
    exact P.pullback_fst _ _ hf

Goal state after:
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).IsStandardOpenImmersion
⊢ (algebraMap S (TensorProduct R S T)).IsStandardOpenImmersion

Tactic:
isStandardOpenImmersion_algebraMap

Goal state after:
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardOpenImmersion R T
⊢ Algebra.IsStandardOpenImmersion S (TensorProduct R S T)
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
⊢ (map (Ideal.Quotient.mk P) p).coeff p.natDegree = (X ^ p.natDegree).coeff p.natDegree

pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i✝ : ℕ
hi✝ : i✝ ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
i : ℕ
hi : p.natDegree < i
⊢ (map (Ideal.Quotient.mk P) p).coeff i = (X ^ p.natDegree).coeff i

Tactic:
· simp [hp]

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i✝ : ℕ
hi✝ : i✝ ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
i : ℕ
hi : p.natDegree < i
⊢ (map (Ideal.Quotient.mk P) p).coeff i = (X ^ p.natDegree).coeff i
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case inr.inl
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
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
h₀ : (algebraMap R[X] S[X]) X = X
this✝¹ : (Polynomial.map (algebraMap R[X] S[X]) ((taylor (X ^ m)) q)).IsRoot (p - X ^ m)
this✝ : X ^ m - p ∣ Polynomial.map (algebraMap R S) (eval (X ^ m) q)
this : IsIntegral R (-(X ^ m - p).coeff i)
hi : i ≤ p.natDegree
⊢ IsIntegral R (p.coeff i)

Tactic:
simpa [show i ≠ m by lia] using this

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : WeaklyQuasiFiniteAt R Q
this : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P).IsPrime
⊢ P = Q

Tactic:
have := QuasiFiniteAt.eq_of_le_of_under_eq (R := R)
    (P := P.map (Ideal.Quotient.mk ((Q.under R).map (algebraMap R S))))
    (Q := Q.map (Ideal.Quotient.mk ((Q.under R).map (algebraMap R S))))
    (Ideal.map_mono h₁) (by
      rw [← Ideal.under_under (B := S), ← Ideal.under_under (A := R) (B := S) (C := S ⧸ _)]
      dsimp [Ideal.under] at h₂ ⊢
      simp [Ideal.map_comap_le]
      simp [Ideal.map_comap_le, ← h₂])

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : WeaklyQuasiFiniteAt R Q
this✝ : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P).IsPrime
this :
  Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P =
    Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) Q
⊢ P = Q
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ @LocallyQuasiFinite = affineLocally fun {R S} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite

Tactic:
by
    ext X Y f
    simp [locallyQuasiFinite_iff, affineLocally_iff_affineOpens_le, affineOpens]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsFinite f
⊢ LocallyQuasiFinite f

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally @IsFinite] at ‹IsFinite f›

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : targetAffineLocally (fun X x f x_1 ↦ IsAffine X ∧ (CommRingCat.Hom.hom (Hom.appTop f)).Finite) f
⊢ LocallyQuasiFinite f
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)}) ⋯
⊢ IsOpen {⟨(pullback.fst f (Y.affineCover.f i)) x, ⋯⟩} ↔ IsOpen {⟨x, ⋯⟩}

Tactic:
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!

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 {⟨x, ⋯⟩}
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H' : ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ (RatFunc.mk p q).liftOn f H = f p q

Tactic:
liftOn_mk _ _ f f0 @H'

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H' : ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ f p q = f p q
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
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
⊢ Function.Bijective (Ideal.Quotient.mkₐ R I).comp

Tactic:
← P.homEquiv.symm.bijective.of_comp_iff,

Goal state after:
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
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
⊢ Function.Bijective ((Ideal.Quotient.mkₐ R I).comp ∘ ⇑P.homEquiv.symm)
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
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
this : ∀ (x : S), P.HasMap ((Ideal.Quotient.mk I) x) → ∃! a, ↑a - x ∈ I
⊢ Function.Bijective (⇑P.homEquiv ∘ (Ideal.Quotient.mkₐ R I).comp ∘ ⇑P.homEquiv.symm)

Tactic:
by
    simpa [Function.bijective_iff_existsUnique, Ideal.Quotient.mk_surjective.forall,
      Subtype.ext_iff, Ideal.Quotient.mk_eq_mk_iff_sub_mem]

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

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
⊢ Function.Surjective ⇑(toIntegralClosure R (MvPolynomial σ R) B)

Tactic:
rintro ⟨x, hx⟩

Goal state after:
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)
⊢ ∃ a, (toIntegralClosure R (MvPolynomial σ R) B) a = ⟨x, hx⟩
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
w : P.ResidueField[X]
hw : (mapRingHom (algebraMap R P.ResidueField)) (minpoly R x) = Polynomial.map (algebraMap R P.ResidueField) p * w
⊢ ¬m ∣ 1 + w * Polynomial.map (algebraMap R P.ResidueField) (minpoly R x) ^ (p.natDegree + 1)

Tactic:
dvd_add_left (dvd_mul_of_dvd_right (dvd_pow (by simp [m, minpoly.dvd_iff]) (by simp)) _),

Goal state after:
case refine_2
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
w : P.ResidueField[X]
hw : (mapRingHom (algebraMap R P.ResidueField)) (minpoly R x) = Polynomial.map (algebraMap R P.ResidueField) p * w
⊢ ¬m ∣ 1
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
⊢ ∃ q n, IsIntegral R (a ^ n • t - φ q)

Tactic:
let R' := Localization.Away a

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]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
⊢ ∃ q n, IsIntegral R (a ^ n • t - φ q)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝²⁸ : CommRing R
inst✝²⁷ : CommRing S
inst✝²⁶ : Algebra R S
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝⁷ : IsDomain S'
this✝⁶ : IsDomain R
this✝⁵ : Algebra.IsIntegral R R'
this✝⁴ : FaithfulSMul R' K
this✝³ : FaithfulSMul R R'
this✝² : FaithfulSMul R' L
this✝¹ : FaithfulSMul R' S'
this✝ : IsIntegrallyClosedIn R' K
this : IsIntegrallyClosed R'
g : R' ⊗[R] S →ₐ[R'] S' := TensorProduct.lift (ofId R' S') f ⋯
hf₃ : Function.Injective ⇑f
hf₄ : f.IsIntegral
⊢ IsStronglyTranscendental R' (f x)

Tactic:
refine .of_map (f := IsScalarTower.toAlgHom R' S' L) (FaithfulSMul.algebraMap_injective S' L) ?_

Goal state after:
R : Type u_1
S : Type u_2
inst✝²⁸ : CommRing R
inst✝²⁷ : CommRing S
inst✝²⁶ : Algebra R S
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝⁷ : IsDomain S'
this✝⁶ : IsDomain R
this✝⁵ : Algebra.IsIntegral R R'
this✝⁴ : FaithfulSMul R' K
this✝³ : FaithfulSMul R R'
this✝² : FaithfulSMul R' L
this✝¹ : FaithfulSMul R' S'
this✝ : IsIntegrallyClosedIn R' K
this : IsIntegrallyClosed R'
g : R' ⊗[R] S →ₐ[R'] S' := TensorProduct.lift (ofId R' S') f ⋯
hf₃ : Function.Injective ⇑f
hf₄ : f.IsIntegral
⊢ IsStronglyTranscendental R' ((IsScalarTower.toAlgHom R' S' L) (f x))
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case pos.refine_2
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
⊢ (aeval x) (f.eraseLead + C a * X ^ m) = 0

pp: case pos.refine_3
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
⊢ (algebraMap R S) ((f.eraseLead + C a * X ^ m).coeff n) ∉ p

Tactic:
· simp [← self_sub_monomial_natDegree_leadingCoeff, hf, hm, pow_succ', ← Algebra.smul_def,
        ← Algebra.smul_mul_assoc, ← ha]

Goal state after:
case pos.refine_3
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
⊢ (algebraMap R S) ((f.eraseLead + C a * X ^ m).coeff n) ∉ p
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
        simpa [Algebra.smul_def] using! ha

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

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

Tactic:
resultant,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ (f.sylvester g m n).det = (-1) ^ (m * n) * g.resultant f n m
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ (f.sylvester g m n).det = (-1) ^ (m * n) * g.resultant f n m

Tactic:
resultant,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ (f.sylvester g m n).det = (-1) ^ (m * n) * (g.sylvester f n m).det
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
n m : ℕ
i : Fin (m + 1 + n)
⊢ f.sylvester 0 (m + 1) n i ⟨0, ⋯⟩ = 0

Tactic:
simp [sylvester, show (0 : Fin (m + 1 + n)) = Fin.castAdd _ 0 from rfl, Fin.addCases_left]

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
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₂
this : ∀ i ≤ m, (M i).det = M₂.det
⊢ f.resultant (g + f * (monomial k) r) m n = f.resultant g m n

Tactic:
resultant,

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₂
this : ∀ i ≤ m, (M i).det = M₂.det
⊢ (f.sylvester (g + f * (monomial k) r) m n).det = f.resultant g m n
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
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₂
this : ∀ i ≤ m, (M i).det = M₂.det
⊢ (f.sylvester (g + f * (monomial k) r) m n).det = f.resultant g m n

Tactic:
resultant,

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₂
this : ∀ i ≤ m, (M i).det = M₂.det
⊢ (f.sylvester (g + f * (monomial k) r) m n).det = (f.sylvester g m n).det
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
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₂
this : ∀ i ≤ m, (M i).det = r ^ i * M₂.det
⊢ f.resultant (C r * g) m n = r ^ m * f.resultant g m n

Tactic:
resultant,

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₂
this : ∀ i ≤ m, (M i).det = r ^ i * M₂.det
⊢ (f.sylvester (C r * g) m n).det = r ^ m * f.resultant g m n