awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)))
have 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))
Tactic: refine RingHom.Finite.of_comp_finite (f := mapRingHom (Ideal.Quotient.mk _)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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 (β := (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))
have 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))
Tactic: convert! (RingHom.Finite.of_surjective _ (Ideal.Quotient.mk_surjective (I := p))).comp hx'
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_4 : P.IsPrime
inst_5 : WeaklyQuasiFiniteAt R P
hS : IsDomain S ∧ FaithfulSMul R S
⊢ ¬IsStronglyTranscendental R x
have left : IsDomain S
Tactic: cases hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_4 : P.IsPrime
inst_5 : WeaklyQuasiFiniteAt R P
hS : IsDomain S ∧ FaithfulSMul R S
left : IsDomain S
⊢ ¬IsStronglyTranscendental R x
have right : FaithfulSMul R S
Tactic: cases hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_4 : P.IsPrime
inst_5 : WeaklyQuasiFiniteAt R P
left : IsDomain S
right : FaithfulSMul R S
⊢ ¬IsStronglyTranscendental R x
have this : IsDomain R
Tactic: have : IsDomain R := (FaithfulSMul.algebraMap_injective R S).isDomain
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_4 : P.IsPrime
inst_5 : WeaklyQuasiFiniteAt R P
left : IsDomain S
right : FaithfulSMul R S
this_1 : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra.{u_1, u_2} (↥R') L := adjoin ↥R' (↑(RingHom.range (R := S) (algebraMap S L)) : Set L)
f : S →ₐ[R] ↥S' := AlgHom.codRestrict (IsScalarTower.toAlgHom R S L) (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
⊢ Function.Surjective (α := ↥R' ⊗[R] S) (β := ↥S') (⇑g : (a : ↥R' ⊗[R] S) → ↥S')
have rw : Subalgebra.map S'.val g.range = S'.val.range
Tactic: rw [← AlgHom.range_eq_top,
      ← (Subalgebra.map_injective (f := S'.val) Subtype.val_injective).eq_iff, Algebra.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_4 : P.IsPrime
inst_5 : WeaklyQuasiFiniteAt R P
left : IsDomain S
right : FaithfulSMul R S
this_1 : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra.{u_1, u_2} (↥R') L := adjoin ↥R' (↑(RingHom.range (R := S) (algebraMap S L)) : Set L)
f : S →ₐ[R] ↥S' := AlgHom.codRestrict (IsScalarTower.toAlgHom R S L) (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
⊢ Subalgebra.map S'.val g.range = S'.val.range
have refine : S'.val.range ≤ Subalgebra.map S'.val g.range
Tactic: refine le_antisymm (Set.image_subset_range S'.val g.range) ?_
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_4 : P.IsPrime
inst_5 : WeaklyQuasiFiniteAt R P
left : IsDomain S
right : FaithfulSMul R S
this_1 : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra.{u_1, u_2} (↥R') L := adjoin ↥R' (↑(RingHom.range (R := S) (algebraMap S L)) : Set L)
f : S →ₐ[R] ↥S' := AlgHom.codRestrict (IsScalarTower.toAlgHom R S L) (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
⊢ S'.val.range ≤ Subalgebra.map S'.val g.range
have simp : ∀ (y : S),
  ∃ (a : ↥R' ⊗[R] S),
    Eq (α := L) ((↑((g : (a : ↥R' ⊗[R] S) → ↥(adjoin (↥R') (Set.range (⇑(algebraMap S L) : (a : S) → L)))) a) : L) : L)
      (((algebraMap S L : S →+* L) : (a : S) → L) y : L)
Tactic: simp only [RingHom.coe_range, Subalgebra.range_val, Algebra.adjoin_le_iff, Subalgebra.coe_map,
      Subalgebra.coe_val, AlgHom.coe_range, Set.range_subset_iff, Set.mem_image, Set.mem_range,
      exists_exists_eq_and, S']
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_4 : P.IsPrime
inst_5 : WeaklyQuasiFiniteAt R P
left : IsDomain S
right : FaithfulSMul R S
this_1 : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra.{u_1, u_2} (↥R') L := adjoin ↥R' (↑(RingHom.range (R := S) (algebraMap S L)) : Set L)
f : S →ₐ[R] ↥S' := AlgHom.codRestrict (IsScalarTower.toAlgHom R S L) (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
y : S
⊢ Eq (α := L)
    ((↑((g : (a : ↥R' ⊗[R] S) → ↥(adjoin (↥R') (Set.range (⇑(algebraMap S L) : (a : S) → L)))) (1 ⊗ₜ[R] y)) : L) : L)
    (((algebraMap S L : S →+* L) : (a : S) → L) y : L)
have simp : Eq (α := L) ((↑((f : (a : S) → ↥(adjoin (↥R') (Set.range (⇑(algebraMap S L) : (a : S) → L)))) y) : L) : L)
  (((algebraMap S L : S →+* L) : (a : S) → L) y : L)
Tactic: simp [g, S']
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsReduced S
x : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x))
P : Ideal S
inst_4 : P.IsPrime
inst_5 : WeaklyQuasiFiniteAt R P
left : IsDomain S
right : FaithfulSMul R S
this_1 : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra.{u_1, u_2} (↥R') L := adjoin ↥R' (↑(RingHom.range (R := S) (algebraMap S L)) : Set L)
f : S →ₐ[R] ↥S' := AlgHom.codRestrict (IsScalarTower.toAlgHom R S L) (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
⊢ ¬IsStronglyTranscendental R x
have hf : Function.Surjective (α := ↥R' ⊗[R] S) (β := ↥S') (⇑g : (a : ↥R' ⊗[R] S) → ↥S')
Tactic: have hf : Function.Surjective g := by
    rw [← AlgHom.range_eq_top,
      ← (Subalgebra.map_injective (f := S'.val) Subtype.val_injective).eq_iff, Algebra.map_top]
    refine le_antisymm (Set.image_subset_range S'.val g.range) ?_
    simp only [RingHom.coe_range, Subalgebra.range_val, Algebra.adjoin_le_iff, Subalgebra.coe_map,
      Subalgebra.coe_val, AlgHom.coe_range, Set.range_subset_iff, Set.mem_image, Set.mem_range,
      exists_exists_eq_and, S']
    exact fun y ↦ ⟨1 ⊗ₜ y, by simp [g, S']; rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
⊢ ZariskisMainProperty R p
have inr : ∀
  (this :
    ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
      [WeaklyQuasiFiniteAt R p] (x : S) (hx : Eq (α := Subalgebra R S) R[x] ⊤)
      (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥), ZariskisMainProperty R p)
  (H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥), ZariskisMainProperty R p
Tactic: wlog H : integralClosure R S = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
inr :
  ∀
    (this :
      ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S)
        [inst_7 : p.IsPrime] [WeaklyQuasiFiniteAt R p] (x : S) (hx : Eq (α := Subalgebra R S) R[x] ⊤)
        (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥), ZariskisMainProperty R p)
    (H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥), ZariskisMainProperty R p
⊢ ZariskisMainProperty R p
have wlog : ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
  [WeaklyQuasiFiniteAt R p] (x : S) (hx : Eq (α := Subalgebra R S) R[x] ⊤)
  (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥), ZariskisMainProperty R p
Tactic: wlog H : integralClosure R S = ⊥
Cleared hypotheses: p, inst_3, inst_4, x, hx
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] (p : Ideal S) [inst_8 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (x : S) (hx : Eq (α := Subalgebra R S) R[x] ⊤)
    (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥), ZariskisMainProperty R p
H : ¬Eq (α := Subalgebra R S) (integralClosure R S) ⊥
inst : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
⊢ ZariskisMainProperty R p
have inst₁ : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
Tactic: have inst : Algebra.WeaklyQuasiFiniteAt (integralClosure R S) p :=
      .of_restrictScalars R (integralClosure R S) _
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
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] (x : S) (hx : Eq (α := Subalgebra R S) R[x] ⊤)
    (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
⊢ ZariskisMainProperty R p
have inr : Eq (α := Subalgebra (↥(integralClosure R S)) S) (↥(integralClosure R S))[x] ⊤
Tactic: refine .restrictScalars (this p x ?_ (integralClosure_idem (R := R)))
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
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] (x : S) (hx : Eq (α := Subalgebra R S) R[x] ⊤)
    (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 (α := Subalgebra (↥(integralClosure R S)) S) (↥(integralClosure R S))[x] ⊤
have inr : LE.le (α := Subalgebra R S) ⊤ (Subalgebra.restrictScalars R (S := ↥(integralClosure R S)) (↥(integralClosure R S))[x])
Tactic: suffices ⊤ ≤ (Algebra.adjoin (integralClosure R S) {x}).restrictScalars R from
      top_le_iff.mp fun x _ ↦ (Subalgebra.mem_restrictScalars _).mp (this trivial)
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
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] (x : S) (hx : Eq (α := Subalgebra R S) R[x] ⊤)
    (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
⊢ LE.le (α := Subalgebra R S) ⊤ (Subalgebra.restrictScalars R (S := ↥(integralClosure R S)) (↥(integralClosure R S))[x])
have inr : LE.le (α := Subalgebra R S) R[x]
  (Subalgebra.restrictScalars R (S := ↥(integralClosure R S)) (↥(integralClosure R S))[x])
Tactic: refine hx.ge.trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
⊢ Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
have rwa : Eq (α := Subalgebra R S) (AlgHom.range (aeval x)) ⊤
Tactic: rwa [← AlgHom.range_eq_top, ← Algebra.adjoin_singleton_eq_range_aeval]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
⊢ ZariskisMainProperty R p
have H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
Tactic: have H₀ : Function.Surjective (aeval (R := R) x) := by
    rwa [← AlgHom.range_eq_top, ← Algebra.adjoin_singleton_eq_range_aeval]