no goals
R : Type u
S : Type ?u.642876
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inst : IsNoetherianRing R
I : Ideal R[X]
⊢ IsNoetherian R R
infer_instance
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
k : ℕ
h : N < k
x : R
hx : x ∈ Ideal.leadingCoeffNth I k
hxm : ¬x ∈ M
this : IsNoetherian R R
⊢ Ideal.leadingCoeffNth I k ∈ Set.range (Ideal.leadingCoeffNth I)
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
k : ℕ
h : N < k
x : R
hx : x ∈ Ideal.leadingCoeffNth I k
hxm : ¬x ∈ M
this : IsNoetherian R R
⊢ ¬M < Ideal.leadingCoeffNth I k
refine' WellFounded.not_lt_min (wellFounded_submodule_gt R R) _ _ _
no goals
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
k : ℕ
h : N < k
x : R
hx : x ∈ Ideal.leadingCoeffNth I k
hxm : ¬x ∈ M
this : IsNoetherian R R
⊢ Ideal.leadingCoeffNth I k ∈ Set.range (Ideal.leadingCoeffNth I)
exact ⟨k, rfl⟩
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
⊢ I ≤ Submodule.span R[X] ↑s
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
⊢ I ≤ Submodule.span R[X] ↑s
have : Submodule.span R[X] ↑s = Ideal.span ↑s := by rfl
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
⊢ I ≤ Ideal.span ↑s
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
⊢ I ≤ Submodule.span R[X] ↑s
rw [this]
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp : p ∈ I
⊢ p ∈ Ideal.span ↑s
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
⊢ I ≤ Ideal.span ↑s
intro p hp
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp : p ∈ I
k : ℕ
hn : natDegree p = k
⊢ p ∈ Ideal.span ↑s
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp : p ∈ I
⊢ p ∈ Ideal.span ↑s
generalize hn : p.natDegree = k
case h
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
⊢ p ∈ Ideal.span ↑s
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp : p ∈ I
k : ℕ
hn : natDegree p = k
⊢ p ∈ Ideal.span ↑s
induction' k using Nat.strong_induction_on with k ih generalizing p
case h.inl
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : k ≤ N
⊢ p ∈ Ideal.span ↑s

case h.inr
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
⊢ p ∈ Ideal.span ↑s
case h
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
⊢ p ∈ Ideal.span ↑s
cases' le_or_lt k N with h h
no goals
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
⊢ Submodule.span R[X] ↑s = Ideal.span ↑s
rfl
case h.inl
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k : ℕ
hn : natDegree p✝ = k
p : R[X]
hp : p ∈ I
ih : ∀ (m : ℕ), m < natDegree p → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
h : natDegree p ≤ N
⊢ p ∈ Ideal.span ↑s
case h.inl
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : k ≤ N
⊢ p ∈ Ideal.span ↑s
subst k
no goals
case h.inl
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k : ℕ
hn : natDegree p✝ = k
p : R[X]
hp : p ∈ I
ih : ∀ (m : ℕ), m < natDegree p → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
h : natDegree p ≤ N
⊢ p ∈ Ideal.span ↑s
refine' hs2 ⟨Polynomial.mem_degreeLE.2
  (le_trans Polynomial.degree_le_natDegree <| WithBot.coe_le_coe.2 h), hp⟩
case h.inr
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
⊢ p ∈ Ideal.span ↑s
case h.inr
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
⊢ p ∈ Ideal.span ↑s
have hp0 : p ≠ 0 := by
  rintro rfl
  cases hn
  exact Nat.not_lt_zero _ h
case h.inr
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this : 0 ≠ 1
⊢ p ∈ Ideal.span ↑s
case h.inr
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
⊢ p ∈ Ideal.span ↑s
have : (0 : R) ≠ 1 := by
  intro h
  apply hp0
  ext i
  refine' (mul_one _).symm.trans _
  rw [← h, MulZeroClass.mul_zero]
  rfl
case h.inr
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
⊢ p ∈ Ideal.span ↑s
case h.inr
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this : 0 ≠ 1
⊢ p ∈ Ideal.span ↑s
haveI : Nontrivial R := ⟨⟨0, 1, this⟩⟩
case h.inr
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
this : leadingCoeff p ∈ Ideal.leadingCoeffNth I N
⊢ p ∈ Ideal.span ↑s
case h.inr
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
⊢ p ∈ Ideal.span ↑s
have : p.leadingCoeff ∈ I.leadingCoeffNth N := by
  rw [HN]
  exact hm2 k ((I.mem_leadingCoeffNth _ _).2
    ⟨_, hp, hn ▸ Polynomial.degree_le_natDegree, rfl⟩)
case h.inr
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
this : ∃ p_1, p_1 ∈ I ∧ degree p_1 ≤ ↑N ∧ leadingCoeff p_1 = leadingCoeff p
⊢ p ∈ Ideal.span ↑s
case h.inr
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
this : leadingCoeff p ∈ Ideal.leadingCoeffNth I N
⊢ p ∈ Ideal.span ↑s
rw [I.mem_leadingCoeffNth] at this
case h.inr.intro.intro.intro
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
⊢ p ∈ Ideal.span ↑s
case h.inr
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
this : ∃ p_1, p_1 ∈ I ∧ degree p_1 ≤ ↑N ∧ leadingCoeff p_1 = leadingCoeff p
⊢ p ∈ Ideal.span ↑s
rcases this with ⟨q, hq, hdq, hlqp⟩
case h.inr.intro.intro.intro
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ p ∈ Ideal.span ↑s
case h.inr.intro.intro.intro
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
⊢ p ∈ Ideal.span ↑s
have hq0 : q ≠ 0 := by
  intro H
  rw [← Polynomial.leadingCoeff_eq_zero] at H
  rw [hlqp, Polynomial.leadingCoeff_eq_zero] at H
  exact hp0 H
case h.inr.intro.intro.intro
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
⊢ p ∈ Ideal.span ↑s
case h.inr.intro.intro.intro
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
⊢ p ∈ Ideal.span ↑s
have h2 : p.leadingCoeff = (q * Polynomial.X ^ (k - q.natDegree)).leadingCoeff := by
  rw [← hlqp, Polynomial.leadingCoeff_mul_X_pow]
case h.inr.intro.intro.intro
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < degree p
⊢ p ∈ Ideal.span ↑s
case h.inr.intro.intro.intro
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
⊢ p ∈ Ideal.span ↑s
have := Polynomial.degree_sub_lt h1 hp0 h2
case h.inr.intro.intro.intro
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
⊢ p ∈ Ideal.span ↑s
case h.inr.intro.intro.intro
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < degree p
⊢ p ∈ Ideal.span ↑s
rw [Polynomial.degree_eq_natDegree hp0] at this
case h.inr.intro.intro.intro
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
⊢ p - q * X ^ (k - natDegree q) + q * X ^ (k - natDegree q) ∈ Ideal.span ↑s
case h.inr.intro.intro.intro
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
⊢ p ∈ Ideal.span ↑s
rw [← sub_add_cancel p (q * Polynomial.X ^ (k - q.natDegree))]
case h.inr.intro.intro.intro.refine'_1
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
⊢ p - q * X ^ (k - natDegree q) ∈ Ideal.span ↑s

case h.inr.intro.intro.intro.refine'_2
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
⊢ q ∈ Ideal.span ↑s
case h.inr.intro.intro.intro
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
⊢ p - q * X ^ (k - natDegree q) + q * X ^ (k - natDegree q) ∈ Ideal.span ↑s
refine' (Ideal.span ↑s).add_mem _ ((Ideal.span ↑s).mul_mem_right _ _)
no goals
case h.inr.intro.intro.intro.refine'_2
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
⊢ q ∈ Ideal.span ↑s
exact hs2 ⟨Polynomial.mem_degreeLE.2 hdq, hq⟩
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp✝ : p ∈ I
k✝ : ℕ
hn✝ : natDegree p = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
h : N < k
hp : 0 ∈ I
hn : natDegree 0 = k
⊢ False
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
⊢ p ≠ 0
rintro rfl
case refl
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp✝ : p ∈ I
k : ℕ
hn : natDegree p = k
hp : 0 ∈ I
ih : ∀ (m : ℕ), m < natDegree 0 → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
h : N < natDegree 0
⊢ False
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp✝ : p ∈ I
k✝ : ℕ
hn✝ : natDegree p = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
h : N < k
hp : 0 ∈ I
hn : natDegree 0 = k
⊢ False
cases hn
no goals
case refl
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp✝ : p ∈ I
k : ℕ
hn : natDegree p = k
hp : 0 ∈ I
ih : ∀ (m : ℕ), m < natDegree 0 → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
h : N < natDegree 0
⊢ False
exact Nat.not_lt_zero _ h
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
⊢ False
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
⊢ 0 ≠ 1
intro h
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
⊢ p = 0
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
⊢ False
apply hp0
case a
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
i : ℕ
⊢ coeff p i = coeff 0 i
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
⊢ p = 0
ext i
case a
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
i : ℕ
⊢ coeff p i * 1 = coeff 0 i
case a
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
i : ℕ
⊢ coeff p i = coeff 0 i
refine' (mul_one _).symm.trans _
case a
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
i : ℕ
⊢ 0 = coeff 0 i
case a
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
i : ℕ
⊢ coeff p i * 1 = coeff 0 i
rw [← h, MulZeroClass.mul_zero]
no goals
case a
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
i : ℕ
⊢ 0 = coeff 0 i
rfl
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
⊢ leadingCoeff p ∈ M
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
⊢ leadingCoeff p ∈ Ideal.leadingCoeffNth I N
rw [HN]
no goals
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
⊢ leadingCoeff p ∈ M
exact hm2 k ((I.mem_leadingCoeffNth _ _).2
  ⟨_, hp, hn ▸ Polynomial.degree_le_natDegree, rfl⟩)
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
H : q = 0
⊢ False
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
⊢ q ≠ 0
intro H
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
H : leadingCoeff q = 0
⊢ False
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
H : q = 0
⊢ False
rw [← Polynomial.leadingCoeff_eq_zero] at H
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
H : p = 0
⊢ False
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
H : leadingCoeff q = 0
⊢ False
rw [hlqp, Polynomial.leadingCoeff_eq_zero] at H
no goals
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
H : p = 0
⊢ False
exact hp0 H
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ degree p = degree q + ↑(k - natDegree q)

R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ leadingCoeff q * leadingCoeff (X ^ (k - natDegree q)) ≠ 0
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ degree p = degree (q * X ^ (k - natDegree q))
rw [Polynomial.degree_mul', Polynomial.degree_X_pow]
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ ↑(natDegree p) = ↑(natDegree q) + ↑(k - natDegree q)

R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ leadingCoeff q * leadingCoeff (X ^ (k - natDegree q)) ≠ 0
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ degree p = degree q + ↑(k - natDegree q)

R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ leadingCoeff q * leadingCoeff (X ^ (k - natDegree q)) ≠ 0
rw [Polynomial.degree_eq_natDegree hp0, Polynomial.degree_eq_natDegree hq0]
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ natDegree q ≤ k

R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ leadingCoeff q * leadingCoeff (X ^ (k - natDegree q)) ≠ 0
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ ↑(natDegree p) = ↑(natDegree q) + ↑(k - natDegree q)

R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ leadingCoeff q * leadingCoeff (X ^ (k - natDegree q)) ≠ 0
rw [Nat.cast_withBot, Nat.cast_withBot, Nat.cast_withBot, ← WithBot.coe_add,
  add_tsub_cancel_of_le, hn]
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ leadingCoeff q ≠ 0
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ leadingCoeff q * leadingCoeff (X ^ (k - natDegree q)) ≠ 0
rw [Polynomial.leadingCoeff_X_pow, mul_one]
no goals
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ leadingCoeff q ≠ 0
exact mt Polynomial.leadingCoeff_eq_zero.1 hq0
no goals
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
⊢ natDegree q ≤ k
refine' le_trans (Polynomial.natDegree_le_of_degree_le hdq) (le_of_lt h)
no goals
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
⊢ leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
rw [← hlqp, Polynomial.leadingCoeff_mul_X_pow]
case pos
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
hpq : p - q * X ^ (k - natDegree q) = 0
⊢ p - q * X ^ (k - natDegree q) ∈ Ideal.span ↑s

case neg
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
hpq : ¬p - q * X ^ (k - natDegree q) = 0
⊢ p - q * X ^ (k - natDegree q) ∈ Ideal.span ↑s
case h.inr.intro.intro.intro.refine'_1
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
⊢ p - q * X ^ (k - natDegree q) ∈ Ideal.span ↑s
by_cases hpq : p - q * Polynomial.X ^ (k - q.natDegree) = 0
case neg
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
hpq : ¬p - q * X ^ (k - natDegree q) = 0
⊢ natDegree (p - q * X ^ (k - natDegree q)) < k
case neg
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
hpq : ¬p - q * X ^ (k - natDegree q) = 0
⊢ p - q * X ^ (k - natDegree q) ∈ Ideal.span ↑s
refine' ih _ _ (I.sub_mem hp (I.mul_mem_right _ hq)) rfl
no goals
case neg
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
hpq : ¬p - q * X ^ (k - natDegree q) = 0
⊢ natDegree (p - q * X ^ (k - natDegree q)) < k
rwa [Polynomial.degree_eq_natDegree hpq, Nat.cast_withBot, Nat.cast_withBot,
  WithBot.coe_lt_coe, hn] at this
case pos
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
hpq : p - q * X ^ (k - natDegree q) = 0
⊢ 0 ∈ Ideal.span ↑s
case pos
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
hpq : p - q * X ^ (k - natDegree q) = 0
⊢ p - q * X ^ (k - natDegree q) ∈ Ideal.span ↑s
rw [hpq]
no goals
case pos
R : Type u
S : Type ?u.642876
σ : Type v
M✝ : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M✝
inst✝ : Module R M✝
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R :=
  WellFounded.min (_ : WellFounded fun x x_1 => x > x_1) (Set.range (Ideal.leadingCoeffNth I))
    (_ : ∃ x, x ∈ Set.range (Ideal.leadingCoeffNth I))
hm : M ∈ Set.range (Ideal.leadingCoeffNth I)
N : ℕ
HN : Ideal.leadingCoeffNth I N = M
s : Finset R[X]
hs : Submodule.span R ↑s = Ideal.degreeLE I ↑N
hm2 : ∀ (k : ℕ), Ideal.leadingCoeffNth I k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ Ideal.degreeLE I ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
p✝ : R[X]
hp✝ : p✝ ∈ I
k✝ : ℕ
hn✝ : natDegree p✝ = k✝
k : ℕ
ih : ∀ (m : ℕ), m < k → ∀ ⦃p : R[X]⦄, p ∈ I → natDegree p = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : natDegree p = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : degree q ≤ ↑N
hlqp : leadingCoeff q = leadingCoeff p
hq0 : q ≠ 0
h1 : degree p = degree (q * X ^ (k - natDegree q))
h2 : leadingCoeff p = leadingCoeff (q * X ^ (k - natDegree q))
this : degree (p - q * X ^ (k - natDegree q)) < ↑(natDegree p)
hpq : p - q * X ^ (k - natDegree q) = 0
⊢ 0 ∈ Ideal.span ↑s
exact Ideal.zero_mem _