awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
⊢ ∀ (x : S), ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range

Tactic:
have (x : _) : ∃ n, p.leadingCoeff ^ n • (t * x) ∈ φ.range := by
    have : φ p * t * x ∈ φ.range := by simpa [← AlgHom.map_adjoin_singleton] using hp x
    obtain ⟨q, n, hn⟩ :=
      exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range φ _ p
        (hφ.to_isIntegral (t * x)) (by convert! this using 1; ring)
    obtain ⟨r, hr : algebraMap _ _ r = _⟩ := hRS.le hn
    exact ⟨n, (C r + q), by simp [← Polynomial.algebraMap_eq, - Polynomial.algebraMap_apply, hr]⟩
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this_1 : IsScalarTower R R[X] S
this : ∀ (x : S), ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range
choose :
  ∀ (n : (x : S) → ℕ) (hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range),
    ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)
⊢ ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)

Tactic:
choose n hn using this
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
obtain :
  ∀ (s : Finset S) (hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤),
    ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)
⊢ ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)

Tactic:
obtain ⟨s, hs⟩ := Module.Finite.fg_top (R := R[X]) (M := S)

Premises used: Module.Finite.fg_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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
⊢ ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)

Tactic:
⟨s.sup n, fun x ↦ ?_⟩

Premises used: Exists.intro, Finset.sup
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
refine :
  ∀ (x : S), Membership.mem (γ := Subalgebra R S) R[((φ : (a : R[X]) → S) X : S)] (p.leadingCoeff ^ s.sup n • t * x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)

Tactic:
refine ⟨s.sup n, fun x ↦ ?_⟩
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x : S
rw : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
⊢ Membership.mem (γ := Subalgebra R S) R[((φ : (a : R[X]) → S) X : S)] (p.leadingCoeff ^ s.sup n • t * x)

Tactic:
rw [← AlgHom.map_adjoin_singleton, adjoin_X, Algebra.map_top, Algebra.smul_mul_assoc]

Premises used: Algebra.smul_mul_assoc, Algebra.map_top, AlgHom.map_adjoin_singleton, Polynomial.adjoin_X
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x_1 x : S
h : x ∈ (↑s : Set S)
mem : p.leadingCoeff ^ (s.sup n - n x) • p.leadingCoeff ^ n x • (t * x) ∈ φ.range
⊢ p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range

Tactic:
rw [← Nat.sub_add_cancel (s.le_sup h), pow_add, mul_smul]

Premises used: pow_add, Nat.sub_add_cancel, SemigroupAction.mul_smul, Finset.le_sup
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x_1 x : S
h : x ∈ (↑s : Set S)
⊢ p.leadingCoeff ^ (s.sup n - n x) • p.leadingCoeff ^ n x • (t * x) ∈ φ.range

Tactic:
Subalgebra.smul_mem _ (hn _) _

Premises used: Set.Mem, Subalgebra.smul_mem
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x_1 x : S
h : x ∈ (↑s : Set S)
⊢ p.leadingCoeff ^ (s.sup n - n x) • p.leadingCoeff ^ n x • (t * x) ∈ φ.range

Tactic:
exact Subalgebra.smul_mem _ (hn _) _

Premises used: Subalgebra.smul_mem
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x : S
⊢ p.leadingCoeff ^ s.sup n • (t * 0) ∈ φ.range

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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x_1 x y : S
hx_1 : Membership.mem (γ := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) x
hy_1 : Membership.mem (γ := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) y
hx : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
hy : p.leadingCoeff ^ s.sup n • (t * y) ∈ φ.range
⊢ p.leadingCoeff ^ s.sup n • (t * (x + y)) ∈ φ.range

Tactic:
simpa only [mul_add, smul_add] using add_mem hx hy

Premises used: AddMemClass.add_mem, mul_add, smul_add
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x_1 : S
a : R[X]
x : S
hx : Membership.mem (γ := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) x
IH : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
smul : HMul.hMul (α := S) ((algebraMap R[X] S : (a : R[X]) → S) a : S) (p.leadingCoeff ^ s.sup n • (t * x)) ∈ φ.range
⊢ p.leadingCoeff ^ s.sup n • (t * a • x) ∈ φ.range

Tactic:
rw [mul_smul_comm, smul_comm, Algebra.smul_def]

Premises used: mul_smul_comm, Algebra.smul_def, SMulCommClass.smul_comm
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x_1 : S
a : R[X]
x : S
hx : Membership.mem (γ := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) x
IH : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
⊢ HMul.hMul (α := S) ((algebraMap R[X] S : (a : R[X]) → S) a : S) (p.leadingCoeff ^ s.sup n • (t * x)) ∈ φ.range

Tactic:
mul_mem (AlgHom.mem_range_self _ _) IH

Premises used: AlgHom.mem_range_self, MulMemClass.mul_mem
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x_1 : S
a : R[X]
x : S
hx : Membership.mem (γ := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) x
IH : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
⊢ HMul.hMul (α := S) ((algebraMap R[X] S : (a : R[X]) → S) a : S) (p.leadingCoeff ^ s.sup n • (t * x)) ∈ φ.range

Tactic:
exact mul_mem (AlgHom.mem_range_self _ _) IH

Premises used: AlgHom.mem_range_self, MulMemClass.mul_mem
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x : S
⊢ Membership.mem (γ := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) x

Tactic:
induction hs.ge (Set.mem_univ x) using Submodule.span_induction with
  | mem x h =>
    rw [← Nat.sub_add_cancel (s.le_sup h), pow_add, mul_smul]
    exact Subalgebra.smul_mem _ (hn _) _
  | zero => simp
  | add x y _ _ hx hy => simpa only [mul_add, smul_add] using add_mem hx hy
  | smul a x hx IH =>
    rw [mul_smul_comm, smul_comm, Algebra.smul_def]
    exact mul_mem (AlgHom.mem_range_self _ _) IH

Premises used: Eq.ge, pow_add, Subalgebra.smul_mem, Set.mem_univ, mul_smul_comm, Algebra.smul_def, mul_add, SMulCommClass.smul_comm, SemigroupAction.mul_smul, smul_add
-- 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
φ : 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 : ℕ
inr :
  ∀
    (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))
        (i : ℕ) (hi : i = p.natDegree),
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t))
    (hi : ¬i = p.natDegree),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
wlog :
  ∀ (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)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
wlog hi : i = p.natDegree generalizing p i

Premises used: Polynomial.natDegree
-- 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
φ : 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))
    (i : ℕ) (hi : i = p.natDegree),
    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)),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)

Tactic:
simp only [forall_eq, coeff_natDegree] at this

Premises used: Polynomial.coeff_natDegree, forall_eq
-- 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
φ : 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)
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)

Tactic:
obtain hi' | hi' := lt_or_ge p.natDegree i

Premises used: lt_or_ge, Polynomial.natDegree
-- 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
φ : 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
hi' : p.natDegree < i
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
simp [coeff_eq_zero_of_natDegree_lt hi']

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- 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
φ : 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
hi' : i ≤ p.natDegree
⊢ i = 0

Tactic:
lia
-- 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
φ : 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
hi' : i ≤ p.natDegree
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)

Tactic:
simpa [← coeff_natDegree, hpn, show i = 0 by lia] using this _ hp

Premises used: Polynomial.coeff_natDegree