-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem Polynomial.isNoetherianRing [inst : IsNoetherianRing R] : IsNoetherianRing R[X] :=
  isNoetherianRing_iff.2
    ⟨fun I : Ideal R[X] =>
      let M := inst.wf.min (Set.range I.leadingCoeffNth) ⟨_, ⟨0, rfl⟩⟩
      have hm : M ∈ Set.range I.leadingCoeffNth := WellFounded.min_mem _ _ _
      let ⟨N, HN⟩ := hm
      let ⟨s, hs⟩ := I.is_fg_degreeLE N
      have hm2 : ∀ k, I.leadingCoeffNth k ≤ M := fun k =>
        Or.casesOn (le_or_lt k N) (fun h => HN ▸ I.leadingCoeffNth_mono h) fun h _ hx =>
          Classical.by_contradiction fun hxm =>
            haveI : IsNoetherian R R := inst
            have : ¬M < I.leadingCoeffNth k

Proof state:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
⊢ p.leadingCoeff ∈ I.leadingCoeffNth N

Tactic:
rw [HN]

Result:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
⊢ p.leadingCoeff ∈ M

Proof state:
case h.inr.intro.intro.intro.convert_5
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ q ∈ Ideal.span ↑s

Tactic:
exact hs2 ⟨Polynomial.mem_degreeLE.2 hdq, hq⟩

Result:
no goals

Proof state:
case refl
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
hp : 0 ∈ I
ih : ∀ m < natDegree 0, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
h : N < natDegree 0
⊢ False

Tactic:
exact Nat.not_lt_zero _ h

Result:
no goals

Proof state:
case h.inr.intro.intro.intro
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ p ∈ Ideal.span ↑s

Tactic:
rw [← sub_add_cancel p (q * Polynomial.X ^ (k - q.natDegree))]

Result:
case h.inr.intro.intro.intro
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ p - q * X ^ (k - q.natDegree) + q * X ^ (k - q.natDegree) ∈ Ideal.span ↑s

Proof state:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
⊢ 0 ≠ 1

Tactic:
intro h

Result:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
⊢ False

Proof state:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp : p ∈ I
⊢ p ∈ Ideal.span ↑s

Tactic:
generalize hn : p.natDegree = k

Result:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp : p ∈ I
k : ℕ
hn : p.natDegree = k
⊢ p ∈ Ideal.span ↑s