awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_10 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst : p.IsPrime
⊢ Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)

Tactic:
have inst : (P.map (Ideal.Quotient.mk p)).IsPrime :=
      Ideal.map_isPrime_of_surjective Ideal.Quotient.mk_surjective (by simpa)
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_11 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
suffices : WeaklyQuasiFiniteAt R (S := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ WeaklyQuasiFiniteAt.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p)) (S := S ⧸ p)
    (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)

Tactic:
suffices Algebra.WeaklyQuasiFiniteAt R (P.map (Ideal.Quotient.mk p)) from
        .of_restrictScalars R _ _
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_11 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ WeaklyQuasiFiniteAt R (S := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)

Tactic:
.of_surjectiveOnStalks P _ (Ideal.Quotient.mkₐ _ _)
        (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective) ?_

Premises used: RingHom.surjectiveOnStalks_of_surjective, Ideal.Quotient.mk_surjective, Algebra.WeaklyQuasiFiniteAt.of_surjectiveOnStalks, Ideal.Quotient.mkₐ
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_11 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
refine :
  P = Ideal.comap (F := S →ₐ[R] S ⧸ p) (Ideal.Quotient.mkₐ R p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ WeaklyQuasiFiniteAt R (S := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)

Tactic:
refine .of_surjectiveOnStalks P _ (Ideal.Quotient.mkₐ _ _)
        (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective) ?_
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_11 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ P = Ideal.comap (F := S →ₐ[R] S ⧸ p) (Ideal.Quotient.mkₐ R p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)

Tactic:
.trans ?_ (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm

Premises used: Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_11 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
refine : P = P ⊔ Ideal.comap (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) ⊥
⊢ P = Ideal.comap (F := S →ₐ[R] S ⧸ p) (Ideal.Quotient.mkₐ R p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)

Tactic:
refine .trans ?_ (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_11 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ P = P ⊔ Ideal.comap (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) ⊥

Tactic:
simpa [← RingHom.ker_eq_comap_bot]

Premises used: RingHom.ker_eq_comap_bot
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra R S] [IsReduced S] {x : S}
    (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_11 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ WeaklyQuasiFiniteAt.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p)) (S := S ⧸ p)
    (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)

Tactic:
have inst : WeaklyQuasiFiniteAt (R ⧸ Ideal.under R p) (Ideal.map (Ideal.Quotient.mk p) P) := by
      suffices Algebra.WeaklyQuasiFiniteAt R (P.map (Ideal.Quotient.mk p)) from
        .of_restrictScalars R _ _
      refine .of_surjectiveOnStalks P _ (Ideal.Quotient.mkₐ _ _)
        (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective) ?_
      refine .trans ?_ (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm
      simpa [← RingHom.ker_eq_comap_bot]
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_9 : CommRing S] [inst_10 : Algebra R S] [IsReduced S]
    {x : S} (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_12 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst_8 : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
inst :
  WeaklyQuasiFiniteAt.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p)) (S := S ⧸ p)
    (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ False

Tactic:
this (R := R ⧸ p.under R) ?_ (P.map (Ideal.Quotient.mk p)) ⟨inferInstance, inferInstance⟩
      ((isStronglyTranscendental_mk_of_mem_minimalPrimes hx p hp).of_surjective_left
        Ideal.Quotient.mk_surjective)

Premises used: Ideal.Quotient.mk, inferInstance, Ideal.map, Ideal.Quotient.mk_surjective, IsStronglyTranscendental.of_surjective_left, And.intro, isStronglyTranscendental_mk_of_mem_minimalPrimes
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_9 : CommRing S] [inst_10 : Algebra R S] [IsReduced S]
    {x : S} (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_12 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst_8 : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
inst :
  WeaklyQuasiFiniteAt.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p)) (S := S ⧸ p)
    (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
inr :
  RingHom.Finite.{u_1, u_2} (A := (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))[X]) (B := S ⧸ p)
    (AlgHom.toRingHom (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
      (aeval ((Ideal.Quotient.mk p : (a : S) → S ⧸ p) x)))
⊢ False

Tactic:
refine this (R := R ⧸ p.under R) ?_ (P.map (Ideal.Quotient.mk p)) ⟨inferInstance, inferInstance⟩
      ((isStronglyTranscendental_mk_of_mem_minimalPrimes hx p hp).of_surjective_left
        Ideal.Quotient.mk_surjective)

Premises used: Ideal.Quotient.mk, inferInstance, Ideal.map, Ideal.Quotient.mk_surjective, IsStronglyTranscendental.of_surjective_left, And.intro, isStronglyTranscendental_mk_of_mem_minimalPrimes
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_9 : CommRing S] [inst_10 : Algebra R S] [IsReduced S]
    {x : S} (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_12 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst_8 : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
inst :
  WeaklyQuasiFiniteAt.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p)) (S := S ⧸ p)
    (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ RingHom.Finite.{u_1, u_2} (A := (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))[X]) (B := S ⧸ p)
    (AlgHom.toRingHom (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
      (aeval ((Ideal.Quotient.mk p : (a : S) → S ⧸ p) x)))

Tactic:
RingHom.Finite.of_comp_finite (f := mapRingHom (Ideal.Quotient.mk _)) ?_

Premises used: RingHom.Finite.of_comp_finite
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_9 : CommRing S] [inst_10 : Algebra R S] [IsReduced S]
    {x : S} (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_12 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst_8 : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
inst :
  WeaklyQuasiFiniteAt.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p)) (S := S ⧸ p)
    (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
inr :
  RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S ⧸ p)
    (RingHom.comp (β := (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))[X])
        (AlgHom.toRingHom (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
          (aeval ((Ideal.Quotient.mk p : (a : S) → S ⧸ p) x)))
        (mapRingHom (Ideal.Quotient.mk (Ideal.under R p))) :
      RingHom.{u_1, u_2} R[X] (S ⧸ p))
⊢ RingHom.Finite.{u_1, u_2} (A := (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))[X]) (B := S ⧸ p)
    (AlgHom.toRingHom (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
      (aeval ((Ideal.Quotient.mk p : (a : S) → S ⧸ p) x)))

Tactic:
refine RingHom.Finite.of_comp_finite (f := mapRingHom (Ideal.Quotient.mk _)) ?_

Premises used: RingHom.Finite.of_comp_finite
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_9 : CommRing S] [inst_10 : Algebra R S] [IsReduced S]
    {x : S} (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_12 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst_8 : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
inst :
  WeaklyQuasiFiniteAt.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p)) (S := S ⧸ p)
    (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
⊢ RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S ⧸ p) (RingHom.comp (Ideal.Quotient.mk p) (AlgHom.toRingHom (aeval x)))

Tactic:
(RingHom.Finite.of_surjective _ (Ideal.Quotient.mk_surjective (I := p))).comp hx'

Premises used: RingHom.Finite.comp, RingHom.Finite.of_surjective, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_9 : CommRing S] [inst_10 : Algebra R S] [IsReduced S]
    {x : S} (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_12 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst_8 : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
inst :
  WeaklyQuasiFiniteAt.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p)) (S := S ⧸ p)
    (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
h :
  Eq (α := RingHom.{u_1, u_2} R[X] (S ⧸ p))
    (RingHom.comp (β := (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))[X])
        (AlgHom.toRingHom (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
          (aeval ((Ideal.Quotient.mk p : (a : S) → S ⧸ p) x)))
        (mapRingHom (Ideal.Quotient.mk (Ideal.under R p))) :
      RingHom.{u_1, u_2} R[X] (S ⧸ p))
    (RingHom.comp (Ideal.Quotient.mk p) (AlgHom.toRingHom (aeval x)) : RingHom.{u_1, u_2} R[X] (S ⧸ p))
⊢ RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S ⧸ p)
    (RingHom.comp (β := (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))[X])
        (AlgHom.toRingHom (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
          (aeval ((Ideal.Quotient.mk p : (a : S) → S ⧸ p) x)))
        (mapRingHom (Ideal.Quotient.mk (Ideal.under R p))) :
      RingHom.{u_1, u_2} R[X] (S ⧸ p))

Tactic:
convert! (RingHom.Finite.of_surjective _ (Ideal.Quotient.mk_surjective (I := p))).comp hx'

Premises used: RingHom.Finite.comp, RingHom.Finite.of_surjective, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_5 : P.IsPrime
inst_6 : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_9 : CommRing S] [inst_10 : Algebra R S] [IsReduced S]
    {x : S} (hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))) (P : Ideal S)
    [inst_12 : P.IsPrime] [WeaklyQuasiFiniteAt R P] (hS : IsDomain S ∧ FaithfulSMul R S), ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes ⊥) p
hpP : p ≤ P
inst_7 : p.IsPrime
inst_8 : Ideal.IsPrime (α := S ⧸ p) (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
inst :
  WeaklyQuasiFiniteAt.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p)) (S := S ⧸ p)
    (Ideal.map (F := S →+* S ⧸ p) (Ideal.Quotient.mk p) P)
h :
  ∀ (x_1 : R),
    Eq.{u_2 + 1} (α := S ⧸ p)
      (((RingHom.comp
                (RingHom.comp (β := (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))[X])
                  (AlgHom.toRingHom (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
                    (aeval ((Ideal.Quotient.mk p : (a : S) → S ⧸ p) x)))
                  (mapRingHom (Ideal.Quotient.mk (Ideal.under R p))))
                C :
              RingHom.{u_1, u_2} R (S ⧸ p)) :
            (a : R) → S ⧸ p)
          x_1 :
        S ⧸ p)
      (((@RingHom.comp _ R[X] _ _ (Semiring.toNonAssocSemiring : NonAssocSemiring R[X]) _
                (RingHom.comp (Ideal.Quotient.mk p) (AlgHom.toRingHom (aeval x)) : RingHom.{u_1, u_2} R[X] (S ⧸ p)) C :
              RingHom.{u_1, u_2} R (S ⧸ p)) :
            (a : R) → S ⧸ p)
          x_1 :
        S ⧸ p)
h₁ :
  Eq.{u_2 + 1} (α := S ⧸ p)
    (((RingHom.comp (β := (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))[X])
              (AlgHom.toRingHom (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
                (aeval ((Ideal.Quotient.mk p : (a : S) → S ⧸ p) x)))
              (mapRingHom (Ideal.Quotient.mk (Ideal.under R p))) :
            RingHom.{u_1, u_2} R[X] (S ⧸ p)) :
          (a : R[X]) → S ⧸ p)
        X :
      S ⧸ p)
    (((RingHom.comp (Ideal.Quotient.mk p) (AlgHom.toRingHom (aeval x)) : RingHom.{u_1, u_2} R[X] (S ⧸ p)) :
          (a : R[X]) → S ⧸ p)
        X :
      S ⧸ p)
⊢ Eq (α := RingHom.{u_1, u_2} R[X] (S ⧸ p))
    (RingHom.comp (β := (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))[X])
        (AlgHom.toRingHom (R := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
          (aeval ((Ideal.Quotient.mk p : (a : S) → S ⧸ p) x)))
        (mapRingHom (Ideal.Quotient.mk (Ideal.under R p))) :
      RingHom.{u_1, u_2} R[X] (S ⧸ p))
    (RingHom.comp (Ideal.Quotient.mk p) (AlgHom.toRingHom (aeval x)) : RingHom.{u_1, u_2} R[X] (S ⧸ p))

Tactic:
ext