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 : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
IH :
  ∀ m < 0,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = 0
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have inr : ∀ (hi' : p.natDegree < i),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: obtain hi' | hi' := lt_or_ge p.natDegree i
-- 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
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
IH :
  ∀ m < 0,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = 0
inr :
  ∀ (hi' : p.natDegree < i),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have inr₁ : ∀ (hi' : i ≤ p.natDegree),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: obtain hi' | hi' := lt_or_ge p.natDegree i
-- 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
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = n + 1
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have inr : ∀ (hi' : i = p.natDegree),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: obtain hi' | hi' := eq_or_ne i p.natDegree
-- 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
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = n + 1
inr :
  ∀ (hi' : i = p.natDegree),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have inr₁ : ∀ (hi' : i ≠ p.natDegree),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: obtain hi' | hi' := eq_or_ne i p.natDegree
-- 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
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p.eraseLead : S) t)
have simp : Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
  (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t -
    p.leadingCoeff • t * HPow.hPow (α := S) ((φ : (a : R[X]) → S) X : S) p.natDegree)
Tactic: simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ t]
-- 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
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have this₁ : Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
  (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p.eraseLead : S) t)
Tactic: have : φ p.eraseLead * t ∈ (conductor R (φ X)).radical := by
        simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ t]
        exact sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))
-- 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
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
n : ℕ
IH :
  ∀ m < n,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
hpn : p.natDegree = n
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have inr : ∀
  (IH :
    ∀ m < 0,
      ∀ (p : R[X])
        (hp :
          Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
            (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
        (hpn : p.natDegree = m),
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t))
  (hpn : p.natDegree = 0),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: cases n with
    | zero =>
      obtain hi' | hi' := lt_or_ge p.natDegree i
      · simp [coeff_eq_zero_of_natDegree_lt hi']
      · simpa [← coeff_natDegree, hpn, show i = 0 by lia] using this _ hp
    | succ n =>
      obtain hi' | hi' := eq_or_ne i p.natDegree
      · simpa [hi'] using this _ hp
      have : φ p.eraseLead * t ∈ (conductor R (φ X)).radical := by
        simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ t]
        exact sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))
      simpa [eraseLead_coeff, hi'] using
        IH _ ((eraseLead_natDegree_le _).trans_lt (by lia)) _ this rfl
Cleared hypotheses: n, IH, hpn
-- 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
φ : R[X] →ₐ[R] S
t : S
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
n : ℕ
IH :
  ∀ m < n,
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (hpn : p.natDegree = m),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
hpn : p.natDegree = n
inr :
  ∀
    (IH :
      ∀ m < 0,
        ∀ (p : R[X])
          (hp :
            Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
              (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
          (hpn : p.natDegree = m),
          Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
            (p.coeff i • t))
    (hpn : p.natDegree = 0),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have inr₁ : ∀ (n : ℕ)
  (IH :
    ∀ m < n + 1,
      ∀ (p : R[X])
        (hp :
          Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
            (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
        (hpn : p.natDegree = m),
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t))
  (hpn : p.natDegree = n + 1),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: cases n with
    | zero =>
      obtain hi' | hi' := lt_or_ge p.natDegree i
      · simp [coeff_eq_zero_of_natDegree_lt hi']
      · simpa [← coeff_natDegree, hpn, show i = 0 by lia] using this _ hp
    | succ n =>
      obtain hi' | hi' := eq_or_ne i p.natDegree
      · simpa [hi'] using this _ hp
      have : φ p.eraseLead * t ∈ (conductor R (φ X)).radical := by
        simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ t]
        exact sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))
      simpa [eraseLead_coeff, hi'] using
        IH _ ((eraseLead_natDegree_le _).trans_lt (by lia)) _ this rfl
Cleared hypotheses: n, IH, hpn
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have inr : ∀ (x : ℕ) (hpn : p.natDegree = x),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: induction hpn : p.natDegree using Nat.strong_induction_on generalizing p with
    | h n IH =>
    cases n with
    | zero =>
      obtain hi' | hi' := lt_or_ge p.natDegree i
      · simp [coeff_eq_zero_of_natDegree_lt hi']
      · simpa [← coeff_natDegree, hpn, show i = 0 by lia] using this _ hp
    | succ n =>
      obtain hi' | hi' := eq_or_ne i p.natDegree
      · simpa [hi'] using this _ hp
      have : φ p.eraseLead * t ∈ (conductor R (φ X)).radical := by
        simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ t]
        exact sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))
      simpa [eraseLead_coeff, hi'] using
        IH _ ((eraseLead_natDegree_le _).trans_lt (by lia)) _ this rfl
-- 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
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
i : ℕ
hi : i = p.natDegree
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have obtain : ∀ (n : ℕ)
  (hn :
    Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
      (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: obtain ⟨n, hn⟩ := hp
Cleared hypotheses: hp
-- 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
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have obtain : ∀ (k : ℕ)
  (hk :
    Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p ^ n).leadingCoeff ^ k • t ^ n)),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: obtain ⟨k, hk⟩ := exists_leadingCoeff_pow_smul_mem_conductor φ (t ^ n) (p ^ n) hRS hφ
    (by simpa [mul_pow] using hn)
-- 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
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p ^ n).leadingCoeff ^ k • t ^ n)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have pos : ∀ (hpn : p.leadingCoeff ^ n = 0),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: by_cases hpn : p.leadingCoeff ^ n = 0
-- 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
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p ^ n).leadingCoeff ^ k • t ^ n)
pos :
  ∀ (hpn : p.leadingCoeff ^ n = 0),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have neg : ∀ (hpn : ¬p.leadingCoeff ^ n = 0),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: by_cases hpn : p.leadingCoeff ^ n = 0
-- 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
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p ^ n).leadingCoeff ^ k • t ^ n)
hpn : p.leadingCoeff ^ n = 0
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have h : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p.coeff i • t) ^ n)
Tactic: use n
-- 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
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p ^ n).leadingCoeff ^ k • t ^ n)
hpn : ¬p.leadingCoeff ^ n = 0
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have hk₁ : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ (n * k) • t ^ n)
Tactic: rw [leadingCoeff_pow' hpn, ← pow_mul] at hk
Cleared hypotheses: hk, hpn
-- 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
φ : R[X] →ₐ[R] S
t : S
p_1 : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ^ n)
k : ℕ
hk : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ (n * k) • t ^ n)
hpn : ¬p.leadingCoeff ^ n = 0
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have neg : Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) ((p.coeff i • t) ^ (n * k + n))
Tactic: refine ⟨n * k + n, ?_⟩