awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] (p : Ideal S) [inst_9 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S) (hf : f.Finite) (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥),
    ZariskisMainProperty R p
H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥
inst_6 : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
inr :
  AlgHom.Finite (R := ↥(integralClosure R S)) (A := (↥(integralClosure R S))[X]) (B := S)
    (aeval ((f : (a : R[X]) → S) X) : (↥(integralClosure R S))[X] →ₐ[↥(integralClosure R S)] S)
⊢ ZariskisMainProperty R p

Tactic:
refine .restrictScalars (this p (aeval (f X)) ?_ (integralClosure_idem (R := R)))
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] (p : Ideal S) [inst_9 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S) (hf : f.Finite) (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥),
    ZariskisMainProperty R p
H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥
inst_6 : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
⊢ AlgHom.Finite (R := ↥(integralClosure R S)) (A := (↥(integralClosure R S))[X]) (B := S)
    (aeval ((f : (a : R[X]) → S) X) : (↥(integralClosure R S))[X] →ₐ[↥(integralClosure R S)] S)

Tactic:
RingHom.Finite.of_comp_finite (f := mapRingHom (algebraMap R _)) ?_

Premises used: AlgHom.Finite, RingHom.Finite.of_comp_finite
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] (p : Ideal S) [inst_9 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S) (hf : f.Finite) (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥),
    ZariskisMainProperty R p
H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥
inst_6 : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
inr :
  RingHom.Finite.{u, u} (A := R[X]) (B := S)
    (RingHom.comp (β := (↥(integralClosure R S))[X])
      (AlgHom.toRingHom (R := ↥(integralClosure R S)) (aeval ((f : (a : R[X]) → S) X)))
      (mapRingHom (algebraMap R ↥(integralClosure R S))))
⊢ AlgHom.Finite (R := ↥(integralClosure R S)) (A := (↥(integralClosure R S))[X]) (B := S)
    (aeval ((f : (a : R[X]) → S) X) : (↥(integralClosure R S))[X] →ₐ[↥(integralClosure R S)] S)

Tactic:
refine RingHom.Finite.of_comp_finite (f := mapRingHom (algebraMap R _)) ?_

Premises used: RingHom.Finite.of_comp_finite
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] (p : Ideal S) [inst_9 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S) (hf : f.Finite) (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥),
    ZariskisMainProperty R p
H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥
inst_6 : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
⊢ f.Finite

Tactic:
(show f.toRingHom.Finite from hf)
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] (p : Ideal S) [inst_9 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S) (hf : f.Finite) (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥),
    ZariskisMainProperty R p
H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥
inst_6 : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
h :
  RingHom.comp (β := (↥(integralClosure R S))[X])
      (AlgHom.toRingHom (R := ↥(integralClosure R S)) (aeval ((f : (a : R[X]) → S) X)))
      (mapRingHom (algebraMap R ↥(integralClosure R S))) =
    f.toRingHom
⊢ RingHom.Finite.{u, u} (A := R[X]) (B := S)
    (RingHom.comp (β := (↥(integralClosure R S))[X])
      (AlgHom.toRingHom (R := ↥(integralClosure R S)) (aeval ((f : (a : R[X]) → S) X)))
      (mapRingHom (algebraMap R ↥(integralClosure R S))))

Tactic:
convert! (show f.toRingHom.Finite from hf)
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] (p : Ideal S) [inst_9 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S) (hf : f.Finite) (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥),
    ZariskisMainProperty R p
H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥
inst_6 : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
h :
  ∀ (x : R),
    Eq (α := S)
      (((RingHom.comp
                (RingHom.comp (β := (↥(integralClosure R S))[X])
                  (AlgHom.toRingHom (R := ↥(integralClosure R S)) (aeval ((f : (a : R[X]) → S) X)))
                  (mapRingHom (algebraMap R ↥(integralClosure R S))))
                C :
              R →+* S) :
            (a : R) → S)
          x :
        S)
      ((f.comp C : (a : R) → S) x : S)
h₁ :
  Eq (α := S)
    (((RingHom.comp (β := (↥(integralClosure R S))[X])
              (AlgHom.toRingHom (R := ↥(integralClosure R S)) (aeval ((f : (a : R[X]) → S) X)))
              (mapRingHom (algebraMap R ↥(integralClosure R S))) :
            R[X] →+* S) :
          (a : R[X]) → S)
        X :
      S)
    ((f.toRingHom : (a : R[X]) → S) X : S)
⊢ RingHom.comp (β := (↥(integralClosure R S))[X])
      (AlgHom.toRingHom (R := ↥(integralClosure R S)) (aeval ((f : (a : R[X]) → S) X)))
      (mapRingHom (algebraMap R ↥(integralClosure R S))) =
    f.toRingHom

Tactic:
ext
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] (p : Ideal S) [inst_9 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S) (hf : f.Finite) (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥),
    ZariskisMainProperty R p
H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥
inst_6 : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
x : R
⊢ Eq (α := S)
    (((RingHom.comp
              (RingHom.comp (β := (↥(integralClosure R S))[X])
                (AlgHom.toRingHom (R := ↥(integralClosure R S)) (aeval ((f : (a : R[X]) → S) X)))
                (mapRingHom (algebraMap R ↥(integralClosure R S))))
              C :
            R →+* S) :
          (a : R) → S)
        x :
      S)
    ((f.comp C : (a : R) → S) x : S)

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

Premises used: AlgHom.commutes
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal S
inst_4 : p.IsPrime
inst_5 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] (p : Ideal S) [inst_9 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S) (hf : f.Finite) (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥),
    ZariskisMainProperty R p
H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥
inst_6 : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
⊢ Eq (α := S)
    (((RingHom.comp (β := (↥(integralClosure R S))[X])
              (AlgHom.toRingHom (R := ↥(integralClosure R S)) (aeval ((f : (a : R[X]) → S) X)))
              (mapRingHom (algebraMap R ↥(integralClosure R S))) :
            R[X] →+* S) :
          (a : R[X]) → S)
        X :
      S)
    ((f.toRingHom : (a : R[X]) → S) X : S)

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

Premises used: AlgHom.commutes
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hp : conductor R ((f : (a : R[X]) → S) X) ≤ p
⊢ Ideal.radical (conductor R ((f : (a : R[X]) → S) X)) ≤ p

Tactic:
rw [← ‹p.IsPrime›.isRadical.radical_le_iff] at hp

Premises used: Ideal.IsRadical.radical_le_iff, Ideal.IsPrime.isRadical
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hp : Ideal.radical (conductor R ((f : (a : R[X]) → S) X)) ≤ p
⊢ let J : Ideal S := Ideal.radical (conductor R ((f : (a : R[X]) → S) X));
  J ≤ p

Tactic:
set J := (conductor R (f X)).radical

Premises used: conductor, Polynomial.X, DFunLike.coe, Ideal.radical
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
J : Ideal S := Ideal.radical (conductor R ((f : (a : R[X]) → S) X))
hp : J ≤ p
⊢ RingHom.ker (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) ≤ p

Tactic:
simpa using hp
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
J : Ideal S := Ideal.radical (conductor R ((f : (a : R[X]) → S) X))
hp : J ≤ p
⊢ Ideal.IsPrime (α := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)

Tactic:
have inst : (p.map (Ideal.Quotient.mk J)).IsPrime :=
      Ideal.map_isPrime_of_surjective Ideal.Quotient.mk_surjective (by simpa using hp)
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst_1 : CommRing R_1
inst_2 : CommRing S_1
inst_3 : Algebra R_1 S_1
R S : Type u
inst_4 : CommRing R
inst_5 : CommRing S
inst_6 : Algebra R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
J : Ideal S := Ideal.radical (conductor R ((f : (a : R[X]) → S) X))
hp : J ≤ p
inst : Ideal.IsPrime (α := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)
⊢ IsReduced.{u} (S ⧸ J)

Tactic:
have inst : IsReduced (S ⧸ J) :=
        (Ideal.isRadical_iff_quotient_reduced _).mp (Ideal.radical_isRadical _)
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst_1 : CommRing R_1
inst_2 : CommRing S_1
inst_3 : Algebra R_1 S_1
R S : Type u
inst_4 : CommRing R
inst_5 : CommRing S
inst_6 : Algebra R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
J : Ideal S := Ideal.radical (conductor R ((f : (a : R[X]) → S) X))
hp : J ≤ p
inst_9 : Ideal.IsPrime (α := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)
inst : IsReduced.{u} (S ⧸ J)
⊢ WeaklyQuasiFiniteAt R (S := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)

Tactic:
.of_surjectiveOnStalks p _ (Ideal.Quotient.mkₐ R _)
        (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective)
        ((Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective p).trans ?_).symm

Premises used: RingHom.surjectiveOnStalks_of_surjective, Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective, Algebra.WeaklyQuasiFiniteAt.of_surjectiveOnStalks, Eq.symm, Ideal.Quotient.mkₐ, Eq.trans
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst_1 : CommRing R_1
inst_2 : CommRing S_1
inst_3 : Algebra R_1 S_1
R S : Type u
inst_4 : CommRing R
inst_5 : CommRing S
inst_6 : Algebra R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
J : Ideal S := Ideal.radical (conductor R ((f : (a : R[X]) → S) X))
hp : J ≤ p
inst_9 : Ideal.IsPrime (α := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)
inst : IsReduced.{u} (S ⧸ J)
refine : p ⊔ Ideal.comap (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) ⊥ = p
⊢ WeaklyQuasiFiniteAt R (S := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)

Tactic:
refine .of_surjectiveOnStalks p _ (Ideal.Quotient.mkₐ R _)
        (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective)
        ((Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective p).trans ?_).symm
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst_1 : CommRing R_1
inst_2 : CommRing S_1
inst_3 : Algebra R_1 S_1
R S : Type u
inst_4 : CommRing R
inst_5 : CommRing S
inst_6 : Algebra R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
J : Ideal S := Ideal.radical (conductor R ((f : (a : R[X]) → S) X))
hp : J ≤ p
inst_9 : Ideal.IsPrime (α := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)
inst : IsReduced.{u} (S ⧸ J)
⊢ p ⊔ Ideal.comap (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) ⊥ = p

Tactic:
simpa [← RingHom.ker_eq_comap_bot]

Premises used: RingHom.ker_eq_comap_bot
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst_1 : CommRing R_1
inst_2 : CommRing S_1
inst_3 : Algebra R_1 S_1
R S : Type u
inst_4 : CommRing R
inst_5 : CommRing S
inst_6 : Algebra R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
J : Ideal S := Ideal.radical (conductor R ((f : (a : R[X]) → S) X))
hp : J ≤ p
inst_9 : Ideal.IsPrime (α := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)
inst : IsReduced.{u} (S ⧸ J)
⊢ WeaklyQuasiFiniteAt R (S := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)

Tactic:
have inst : WeaklyQuasiFiniteAt R (p.map (Ideal.Quotient.mk J)) := by
      refine .of_surjectiveOnStalks p _ (Ideal.Quotient.mkₐ R _)
        (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective)
        ((Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective p).trans ?_).symm
      simpa [← RingHom.ker_eq_comap_bot]
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst_1 : CommRing R_1
inst_2 : CommRing S_1
inst_3 : Algebra R_1 S_1
R S : Type u
inst_4 : CommRing R
inst_5 : CommRing S
inst_6 : Algebra R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
J : Ideal S := Ideal.radical (conductor R ((f : (a : R[X]) → S) X))
hp : J ≤ p
inst_9 : Ideal.IsPrime (α := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)
inst_10 : IsReduced.{u} (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (S := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)
⊢ False

Tactic:
not_isStronglyTranscendental_of_weaklyQuasiFiniteAt ?_ (p.map (Ideal.Quotient.mk J))
      (isStronglyTranscendental_mk_radical_conductor H (f X) (by convert! hf; ext; simp))

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst_1 : CommRing R_1
inst_2 : CommRing S_1
inst_3 : Algebra R_1 S_1
R S : Type u
inst_4 : CommRing R
inst_5 : CommRing S
inst_6 : Algebra R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
J : Ideal S := Ideal.radical (conductor R ((f : (a : R[X]) → S) X))
hp : J ≤ p
inst_9 : Ideal.IsPrime (α := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)
inst_10 : IsReduced.{u} (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (S := S ⧸ J) (Ideal.map (F := S →+* S ⧸ J) (Ideal.Quotient.mk J) p)
⊢ False

Tactic:
refine not_isStronglyTranscendental_of_weaklyQuasiFiniteAt ?_ (p.map (Ideal.Quotient.mk J))
      (isStronglyTranscendental_mk_radical_conductor H (f X) (by convert! hf; ext; simp))
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
⊢ ¬conductor R ((f : (a : R[X]) → S) X) ≤ p

Tactic:
replace hf : ¬ conductor R (f X) ≤ p := by
    intro hp
    rw [← ‹p.IsPrime›.isRadical.radical_le_iff] at hp
    set J := (conductor R (f X)).radical
    have inst : (p.map (Ideal.Quotient.mk J)).IsPrime :=
      Ideal.map_isPrime_of_surjective Ideal.Quotient.mk_surjective (by simpa using hp)
    have inst : IsReduced (S ⧸ J) :=
        (Ideal.isRadical_iff_quotient_reduced _).mp (Ideal.radical_isRadical _)
    have inst : WeaklyQuasiFiniteAt R (p.map (Ideal.Quotient.mk J)) := by
      refine .of_surjectiveOnStalks p _ (Ideal.Quotient.mkₐ R _)
        (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective)
        ((Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective p).trans ?_).symm
      simpa [← RingHom.ker_eq_comap_bot]
    refine not_isStronglyTranscendental_of_weaklyQuasiFiniteAt ?_ (p.map (Ideal.Quotient.mk J))
      (isStronglyTranscendental_mk_radical_conductor H (f X) (by convert! hf; ext; simp))
    convert! (RingHom.Finite.of_surjective _ (Ideal.Quotient.mk_surjective (I := J))).comp hf
      using 1
    ext <;> simp [show ∀ x, f (C x) = algebraMap _ _ x from f.commutes, J]
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
obtain :
  ∀ (x : S) (hx : Membership.mem (γ := Ideal S) (conductor R ((f : (a : R[X]) → S) X) : Ideal S) x) (hxp : x ∉ p),
    ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
obtain ⟨x, hx, hxp⟩ := SetLike.not_le_iff_exists.mp hf

Premises used: Iff.mp, SetLike.not_le_iff_exists
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hx : Membership.mem (γ := Ideal S) (conductor R ((f : (a : R[X]) → S) X) : Ideal S) x
hxp : x ∉ p
a : S
⊢ x * a ∈ f.range

Tactic:
simpa [← AlgHom.map_adjoin_singleton f] using hx a

Premises used: AlgHom.map_adjoin_singleton
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hx : Membership.mem (γ := Ideal S) (conductor R ((f : (a : R[X]) → S) X) : Ideal S) x
hxp : x ∉ p
⊢ ∀ (a : S), x * a ∈ f.range

Tactic:
replace hx (a : _) : x * a ∈ f.range := by simpa [← AlgHom.map_adjoin_singleton f] using hx a
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
⊢ ZariskisMainProperty R p

Tactic:
ZariskisMainProperty.trans (S := f.range) _ ?_ ?_

Premises used: Algebra.ZariskisMainProperty.trans
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
refine_1 : ZariskisMainProperty R (S := ↥f.range) (Ideal.under (↥f.range) p)
refine_2 :
  ∃ r ∉ Ideal.under (↥f.range) p,
    Eq (α := Subalgebra (↥f.range) S)
      (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap (↥f.range) S : (a : ↥f.range) → S) r)) ⋯ :
        Subalgebra (↥f.range) S)
      (⊤ : Subalgebra (↥f.range) S)
⊢ ZariskisMainProperty R p

Tactic:
refine ZariskisMainProperty.trans (S := f.range) _ ?_ ?_

Premises used: Algebra.ZariskisMainProperty.trans
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
this : Algebra (Localization.AtPrime (R := ↥f.range) (Ideal.under (↥f.range) p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥f.range) p) p
⊢ f.range = R[((f : (a : R[X]) → S) X : S)]

Tactic:
simp [← AlgHom.map_adjoin_singleton f]

Premises used: AlgHom.map_adjoin_singleton