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_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)
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:
simp
-- 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)
⊢ 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:
simp
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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
⊢ IsDomain S

Tactic:
cases hS
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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
⊢ FaithfulSMul R S

Tactic:
cases hS
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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
⊢ IsDomain R

Tactic:
have : IsDomain R := (FaithfulSMul.algebraMap_injective R S).isDomain
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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_1 : S
hx' : RingHom.Finite.{u_1, u_2} (A := R[X]) (B := S) (AlgHom.toRingHom (aeval x_1))
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)
x : S
⊢ Membership.mem (α := L) (γ := Subalgebra R L) (Subalgebra.restrictScalars R S')
    ((IsScalarTower.toAlgHom R S L : (a : S) → L) x : L)

Tactic:
simpa using show algebraMap S L x ∈ S' from Algebra.subset_adjoin ⟨x, rfl⟩

Premises used: Algebra.subset_adjoin, Exists.intro, rfl
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 ⋯
rw : Subalgebra.map S'.val g.range = S'.val.range
⊢ Function.Surjective (α := ↥R' ⊗[R] S) (β := ↥S') (⇑g : (a : ↥R' ⊗[R] S) → ↥S')

Tactic:
rw [← AlgHom.range_eq_top,
      ← (Subalgebra.map_injective (f := S'.val) Subtype.val_injective).eq_iff, Algebra.map_top]

Premises used: Subtype.val_injective, Function.Injective.eq_iff, AlgHom.range_eq_top, Subalgebra.map_injective, Algebra.map_top
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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

Tactic:
le_antisymm (Set.image_subset_range S'.val g.range) ?_

Premises used: Subalgebra.val, Set.image_subset_range, le_antisymm, SetLike.coe, DFunLike.coe, AlgHom.range
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 ⋯
refine : S'.val.range ≤ Subalgebra.map S'.val g.range
⊢ Subalgebra.map S'.val g.range = S'.val.range

Tactic:
refine le_antisymm (Set.image_subset_range S'.val g.range) ?_

Premises used: Subalgebra.val, Set.image_subset_range, le_antisymm, SetLike.coe, DFunLike.coe, AlgHom.range
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 ⋯
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)
⊢ S'.val.range ≤ Subalgebra.map S'.val g.range

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']

Premises used: Set.mem_range, AlgHom.coe_range, Set.mem_image, Subalgebra.range_val, Subalgebra.coe_val, Subalgebra.coe_map, exists_exists_eq_and, Algebra.adjoin_le_iff, Set.range_subset_iff, RingHom.coe_range
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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
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)
⊢ 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)

Tactic:
simp [g, S']
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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) ((↑((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:
rfl
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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),
    ∃ (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:
exact fun y ↦ ⟨1 ⊗ₜ y, by simp [g, S']; rfl⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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')

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⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 ⋯
hf : Function.Surjective (α := ↥R' ⊗[R] S) (β := ↥S') (⇑g : (a : ↥R' ⊗[R] S) → ↥S')
⊢ ¬IsStronglyTranscendental R x

Tactic:
not_isStronglyTranscendental_of_weaklyQuasiFiniteAt_of_isDomain_aux

Premises used: _private.0.Algebra.not_isStronglyTranscendental_of_weaklyQuasiFiniteAt_of_isDomain_aux
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
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 : QuasiFiniteAt R P
⊢ ¬IsStronglyTranscendental R x

Tactic:
not_isStronglyTranscendental_of_weaklyQuasiFiniteAt hx' P

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 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
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
⊢ ZariskisMainProperty R p

Tactic:
wlog H : integralClosure R S = ⊥

Premises used: integralClosure
-- 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
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
⊢ WeaklyQuasiFiniteAt (↥(integralClosure R S)) p

Tactic:
have inst : Algebra.WeaklyQuasiFiniteAt (integralClosure R S) p :=
      .of_restrictScalars R (integralClosure R S) _
-- 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
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

Tactic:
.restrictScalars (this p x ?_ (integralClosure_idem (R := R)))

Premises used: integralClosure_idem, Algebra.ZariskisMainProperty.restrictScalars
-- 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
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
inr : Eq (α := Subalgebra (↥(integralClosure R S)) S) (↥(integralClosure R S))[x] ⊤
⊢ ZariskisMainProperty R p

Tactic:
refine .restrictScalars (this p 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
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
inr :
  LE.le (α := Subalgebra R S) ⊤ (Subalgebra.restrictScalars R (S := ↥(integralClosure R S)) (↥(integralClosure R S))[x])
⊢ Eq (α := Subalgebra (↥(integralClosure R S)) 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)
-- 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
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])

Tactic:
hx.ge.trans ?_

Premises used: Eq.ge, LE.le.trans
-- 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
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
inr :
  LE.le (α := Subalgebra R S) R[x]
    (Subalgebra.restrictScalars R (S := ↥(integralClosure R S)) (↥(integralClosure R S))[x])
⊢ LE.le (α := Subalgebra R S) ⊤ (Subalgebra.restrictScalars R (S := ↥(integralClosure R S)) (↥(integralClosure R S))[x])

Tactic:
refine hx.ge.trans ?_

Premises used: Eq.ge, LE.le.trans