awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)
a : R
ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x
pos : n = m → Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) a : S)
⊢ Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) (if n = m then a else 0) : S)
have neg : ¬n = m → Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) 0 : S)
Tactic: split_ifs
-- 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) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) f.leadingCoeff : S)
a : R
ha : (AlgHom.toRingHom (ofId R S) : (a : R) → S) a = f.leadingCoeff • x
h : n = m
⊢ Membership.mem (α := S) p ((algebraMap R S : (a : R) → S) a : S)
have h : (algebraMap R S : (a : R) → S) a = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) x
Tactic: convert! p.mul_mem_right x Hfp
-- 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) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) ∉ p
⊢ ZariskisMainProperty R p
have neg : Eq (α := Subalgebra R S)
  (Subalgebra.saturation (integralClosure R S) (Submonoid.powers ((algebraMap R S : (a : R) → S) f.leadingCoeff)) sorry) ⊤
Tactic: refine zariskisMainProperty_iff_exists_saturation_eq_top.mpr ⟨_, Hfp, isIntegral_algebraMap, ?_⟩
-- 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) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) ∉ p
⊢ Eq (α := Subalgebra R S)
    (Subalgebra.saturation (integralClosure R S) (Submonoid.powers ((algebraMap R S : (a : R) → S) f.leadingCoeff)) ⋯) ⊤
have neg : LE.le (α := Subalgebra R S) R[x]
  (Subalgebra.saturation (integralClosure R S) (Submonoid.powers ((algebraMap R S : (a : R) → S) f.leadingCoeff)) sorry)
Tactic: rw [← top_le_iff, ← hx]
-- 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) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]) (hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)) (n : ℕ)
      (hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p) (hm : f.natDegree = m_1), ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) ∉ p
⊢ LE.le (α := Subalgebra R S) R[x]
    (Subalgebra.saturation (integralClosure R S) (Submonoid.powers ((algebraMap R S : (a : R) → S) f.leadingCoeff)) ⋯)
have neg : Membership.mem (γ := Subalgebra R S) (integralClosure R S)
  ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) f.leadingCoeff : S) x) 1 * x)
Tactic: refine Algebra.adjoin_singleton_le ⟨_, ⟨1, rfl⟩, ?_⟩
-- 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) ⊥
H₀ : Function.Surjective (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
f : R[X]
hf : Eq (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
n : ℕ
hfn : ((algebraMap R S : (a : R) → S) (f.coeff n) : S) ∉ p
⊢ ZariskisMainProperty R p
have induction : ∀ (x : ℕ) (hm : f.natDegree = x), ZariskisMainProperty R p
Tactic: induction hm : f.natDegree using Nat.strong_induction_on generalizing f n with | h m IH =>
  obtain (_ | m) := m
  · obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp hm
    cases n <;> aesop
  by_cases Hfp : algebraMap _ _ f.leadingCoeff ∈ p
  · obtain ⟨a, ha⟩ := H.le (isIntegral_leadingCoeff_smul f x hf)
    refine IH _ ?_ (f.eraseLead + C a * X ^ m) (hm := rfl) ?_ n ?_
    · suffices f.eraseLead.natDegree ≤ m by compute_degree!
      exact (eraseLead_natDegree_le ..).trans (by lia)
    · simp [← self_sub_monomial_natDegree_leadingCoeff, hf, hm, pow_succ', ← Algebra.smul_def,
        ← Algebra.smul_mul_assoc, ← ha]
    · suffices algebraMap R S (f.coeff n) + algebraMap R S (if n = m then a else 0) ∉ p by
        simpa [eraseLead_coeff, show n ≠ f.natDegree by rintro rfl; exact hfn (by simpa)]
      rwa [Ideal.add_mem_iff_left]
      split_ifs
      · convert! p.mul_mem_right x Hfp
        simpa [Algebra.smul_def] using ha
      · simp
  · refine zariskisMainProperty_iff_exists_saturation_eq_top.mpr ⟨_, Hfp, isIntegral_algebraMap, ?_⟩
    rw [← top_le_iff, ← hx]
    refine Algebra.adjoin_singleton_le ⟨_, ⟨1, rfl⟩, ?_⟩
    simpa [Algebra.smul_def] using isIntegral_leadingCoeff_smul f x hf
-- 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
f : R[X] →ₐ[R] S
hf : f.Finite
⊢ 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] (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) ⊥), 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
f : R[X] →ₐ[R] S
hf : f.Finite
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] (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) ⊥), 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] (f : R[X] →ₐ[R] S) (hf : f.Finite) (H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥),
  ZariskisMainProperty R p
Tactic: wlog H : integralClosure R S = ⊥
Cleared hypotheses: p, inst_3, inst_4, f, hf
-- 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
f : R[X] →ₐ[R] S
hf : f.Finite
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] (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 : 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
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
⊢ ZariskisMainProperty R p
have 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)
Tactic: refine .restrictScalars (this p (aeval (f 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
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)
have 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))))
Tactic: refine RingHom.Finite.of_comp_finite (f := mapRingHom (algebraMap 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
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
⊢ 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))))
have 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
Tactic: convert! (show f.toRingHom.Finite from hf)
-- 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
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
⊢ 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
have 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)
Tactic: ext
-- 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
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)
⊢ 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
have 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)
Tactic: ext
-- 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
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
⊢ False
have hp₁ : Ideal.radical (conductor R ((f : (a : R[X]) → S) X)) ≤ p
Tactic: rw [← ‹p.IsPrime›.isRadical.radical_le_iff] at hp
Cleared hypotheses: hp
-- 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
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
⊢ False
have inst : 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)
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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)
⊢ False
have inst₁ : IsReduced.{u} (S ⧸ J)
Tactic: have inst : IsReduced (S ⧸ J) :=
        (Ideal.isRadical_iff_quotient_reduced _).mp (Ideal.radical_isRadical _)
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
have refine : p ⊔ Ideal.comap (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
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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)
⊢ False
have inst₁ : 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]
-- 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
f : R[X] →ₐ[R] S
hf : f.Finite
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
⊢ ZariskisMainProperty R p
have hf₁ : ¬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]
Cleared hypotheses: hf
-- 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
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
⊢ ZariskisMainProperty R p
have 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
Tactic: obtain ⟨x, hx, hxp⟩ := SetLike.not_le_iff_exists.mp hf