[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
⊢ IsLocalRingHom (Ideal.Quotient.mk I)
[PROOFSTEP]
constructor
[GOAL]
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
⊢ ∀ (a : R), IsUnit (↑(Ideal.Quotient.mk I) a) → IsUnit a
[PROOFSTEP]
intro a h
[GOAL]
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
⊢ IsUnit a
[PROOFSTEP]
have : IsUnit (Ideal.Quotient.mk (Ideal.jacobson ⊥) a) :=
  by
  rw [isUnit_iff_exists_inv] at *
  obtain ⟨b, hb⟩ := h
  obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective b
  use Ideal.Quotient.mk _ b
  rw [← (Ideal.Quotient.mk _).map_one, ← (Ideal.Quotient.mk _).map_mul, Ideal.Quotient.eq] at hb ⊢
  exact h hb
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
⊢ IsUnit (↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a)
[PROOFSTEP]
rw [isUnit_iff_exists_inv] at *
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : ∃ b, ↑(Ideal.Quotient.mk I) a * b = 1
⊢ ∃ b, ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * b = 1
[PROOFSTEP]
obtain ⟨b, hb⟩ := h
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a : R
b : R ⧸ I
hb : ↑(Ideal.Quotient.mk I) a * b = 1
⊢ ∃ b, ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * b = 1
[PROOFSTEP]
obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective b
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb : ↑(Ideal.Quotient.mk I) a * ↑(Ideal.Quotient.mk I) b = 1
⊢ ∃ b, ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * b = 1
[PROOFSTEP]
use Ideal.Quotient.mk _ b
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb : ↑(Ideal.Quotient.mk I) a * ↑(Ideal.Quotient.mk I) b = 1
⊢ ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) b = 1
[PROOFSTEP]
rw [← (Ideal.Quotient.mk _).map_one, ← (Ideal.Quotient.mk _).map_mul, Ideal.Quotient.eq] at hb ⊢
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb : a * b - 1 ∈ I
⊢ a * b - 1 ∈ Ideal.jacobson ⊥
[PROOFSTEP]
exact h hb
[GOAL]
case map_nonunit
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
this : IsUnit (↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a)
⊢ IsUnit a
[PROOFSTEP]
obtain ⟨⟨x, y, h1, h2⟩, rfl : x = _⟩ := this
[GOAL]
case map_nonunit.intro.mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R ⧸ Ideal.jacobson ⊥
h1 : ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * y = 1
h2 : y * ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a = 1
⊢ IsUnit a
[PROOFSTEP]
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
[GOAL]
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R
h1 : ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a * ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) y = 1
h2 : ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) y * ↑(Ideal.Quotient.mk (Ideal.jacobson ⊥)) a = 1
⊢ IsUnit a
[PROOFSTEP]
rw [← (Ideal.Quotient.mk _).map_mul, ← (Ideal.Quotient.mk _).map_one, Ideal.Quotient.eq, Ideal.mem_jacobson_bot] at h1
  h2 
[GOAL]
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R
h1 : ∀ (y_1 : R), IsUnit ((a * y - 1) * y_1 + 1)
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
⊢ IsUnit a
[PROOFSTEP]
specialize h1 1
[GOAL]
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit ((a * y - 1) * 1 + 1)
⊢ IsUnit a
[PROOFSTEP]
simp at h1 
[GOAL]
case map_nonunit.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (↑(Ideal.Quotient.mk I) a)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit a ∧ IsUnit y
⊢ IsUnit a
[PROOFSTEP]
exact h1.1
[GOAL]
K : Type u_1
inst✝ : Field K
f : K[X]
x✝¹ : Monic f
a₀ : K
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal K
x✝ : IsUnit (Polynomial.eval a₀ (↑derivative f))
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ maximalIdeal K
[PROOFSTEP]
simp only [(maximalIdeal K).eq_bot_of_prime, Ideal.mem_bot] at h₁ ⊢
[GOAL]
K : Type u_1
inst✝ : Field K
f : K[X]
x✝¹ : Monic f
a₀ : K
x✝ : IsUnit (Polynomial.eval a₀ (↑derivative f))
h₁ : Polynomial.eval a₀ f = 0
⊢ ∃ a, IsRoot f a ∧ a - a₀ = 0
[PROOFSTEP]
exact ⟨a₀, h₁, sub_self _⟩
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
⊢ List.TFAE
    [HenselianLocalRing R,
      ∀ (f : R[X]),
        Monic f →
          ∀ (a₀ : ResidueField R),
            ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀,
      ∀ {K : Type u} [inst : Field K] (φ : R →+* K),
        Surjective ↑φ →
          ∀ (f : R[X]),
            Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀]
[PROOFSTEP]
tfae_have _3_2 : 3 → 2
[GOAL]
case _3_2
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
⊢ (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
[PROOFSTEP]
intro H
[GOAL]
case _3_2
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
H :
  ∀ {K : Type u} [inst : Field K] (φ : R →+* K),
    Surjective ↑φ →
      ∀ (f : R[X]),
        Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀
⊢ ∀ (f : R[X]),
    Monic f →
      ∀ (a₀ : ResidueField R),
        ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
[PROOFSTEP]
exact H (residue R) Ideal.Quotient.mk_surjective
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
⊢ List.TFAE
    [HenselianLocalRing R,
      ∀ (f : R[X]),
        Monic f →
          ∀ (a₀ : ResidueField R),
            ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀,
      ∀ {K : Type u} [inst : Field K] (φ : R →+* K),
        Surjective ↑φ →
          ∀ (f : R[X]),
            Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀]
[PROOFSTEP]
tfae_have _2_1 : 2 → 1
[GOAL]
case _2_1
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
⊢ (∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀) →
    HenselianLocalRing R
[PROOFSTEP]
intro H
[GOAL]
case _2_1
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
H :
  ∀ (f : R[X]),
    Monic f →
      ∀ (a₀ : ResidueField R),
        ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
⊢ HenselianLocalRing R
[PROOFSTEP]
constructor
[GOAL]
case _2_1.is_henselian
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
H :
  ∀ (f : R[X]),
    Monic f →
      ∀ (a₀ : ResidueField R),
        ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
⊢ ∀ (f : R[X]),
    Monic f →
      ∀ (a₀ : R),
        Polynomial.eval a₀ f ∈ maximalIdeal R →
          IsUnit (Polynomial.eval a₀ (↑derivative f)) → ∃ a, IsRoot f a ∧ a - a₀ ∈ maximalIdeal R
[PROOFSTEP]
intro f hf a₀ h₁ h₂
[GOAL]
case _2_1.is_henselian
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
H :
  ∀ (f : R[X]),
    Monic f →
      ∀ (a₀ : ResidueField R),
        ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
f : R[X]
hf : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal R
h₂ : IsUnit (Polynomial.eval a₀ (↑derivative f))
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ maximalIdeal R
[PROOFSTEP]
specialize H f hf (residue R a₀)
[GOAL]
case _2_1.is_henselian
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
f : R[X]
hf : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal R
h₂ : IsUnit (Polynomial.eval a₀ (↑derivative f))
H :
  ↑(aeval (↑(residue R) a₀)) f = 0 →
    ↑(aeval (↑(residue R) a₀)) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = ↑(residue R) a₀
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ maximalIdeal R
[PROOFSTEP]
have aux := flip mem_nonunits_iff.mp h₂
[GOAL]
case _2_1.is_henselian
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
f : R[X]
hf : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal R
h₂ : IsUnit (Polynomial.eval a₀ (↑derivative f))
H :
  ↑(aeval (↑(residue R) a₀)) f = 0 →
    ↑(aeval (↑(residue R) a₀)) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = ↑(residue R) a₀
aux : Polynomial.eval a₀ (↑derivative f) ∈ nonunits R → False
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ maximalIdeal R
[PROOFSTEP]
simp only [aeval_def, ResidueField.algebraMap_eq, eval₂_at_apply, ← Ideal.Quotient.eq_zero_iff_mem, ←
  LocalRing.mem_maximalIdeal] at H h₁ aux 
[GOAL]
case _2_1.is_henselian
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
f : R[X]
hf : Monic f
a₀ : R
h₂ : IsUnit (Polynomial.eval a₀ (↑derivative f))
H :
  ↑(residue R) (Polynomial.eval a₀ f) = 0 →
    ↑(residue R) (Polynomial.eval a₀ (↑derivative f)) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = ↑(residue R) a₀
h₁ : ↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ f) = 0
aux : ↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (↑derivative f)) = 0 → False
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ maximalIdeal R
[PROOFSTEP]
obtain ⟨a, ha₁, ha₂⟩ := H h₁ aux
[GOAL]
case _2_1.is_henselian.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
f : R[X]
hf : Monic f
a₀ : R
h₂ : IsUnit (Polynomial.eval a₀ (↑derivative f))
H :
  ↑(residue R) (Polynomial.eval a₀ f) = 0 →
    ↑(residue R) (Polynomial.eval a₀ (↑derivative f)) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = ↑(residue R) a₀
h₁ : ↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ f) = 0
aux : ↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (↑derivative f)) = 0 → False
a : R
ha₁ : IsRoot f a
ha₂ : ↑(residue R) a = ↑(residue R) a₀
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ maximalIdeal R
[PROOFSTEP]
refine' ⟨a, ha₁, _⟩
[GOAL]
case _2_1.is_henselian.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
f : R[X]
hf : Monic f
a₀ : R
h₂ : IsUnit (Polynomial.eval a₀ (↑derivative f))
H :
  ↑(residue R) (Polynomial.eval a₀ f) = 0 →
    ↑(residue R) (Polynomial.eval a₀ (↑derivative f)) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = ↑(residue R) a₀
h₁ : ↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ f) = 0
aux : ↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (↑derivative f)) = 0 → False
a : R
ha₁ : IsRoot f a
ha₂ : ↑(residue R) a = ↑(residue R) a₀
⊢ a - a₀ ∈ maximalIdeal R
[PROOFSTEP]
rw [← Ideal.Quotient.eq_zero_iff_mem]
[GOAL]
case _2_1.is_henselian.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
f : R[X]
hf : Monic f
a₀ : R
h₂ : IsUnit (Polynomial.eval a₀ (↑derivative f))
H :
  ↑(residue R) (Polynomial.eval a₀ f) = 0 →
    ↑(residue R) (Polynomial.eval a₀ (↑derivative f)) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = ↑(residue R) a₀
h₁ : ↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ f) = 0
aux : ↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (↑derivative f)) = 0 → False
a : R
ha₁ : IsRoot f a
ha₂ : ↑(residue R) a = ↑(residue R) a₀
⊢ ↑(Ideal.Quotient.mk (maximalIdeal R)) (a - a₀) = 0
[PROOFSTEP]
rwa [← sub_eq_zero, ← RingHom.map_sub] at ha₂ 
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
_2_1 :
  (∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀) →
    HenselianLocalRing R
⊢ List.TFAE
    [HenselianLocalRing R,
      ∀ (f : R[X]),
        Monic f →
          ∀ (a₀ : ResidueField R),
            ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀,
      ∀ {K : Type u} [inst : Field K] (φ : R →+* K),
        Surjective ↑φ →
          ∀ (f : R[X]),
            Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀]
[PROOFSTEP]
tfae_have _1_3 : 1 → 3
[GOAL]
case _1_3
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
_2_1 :
  (∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀) →
    HenselianLocalRing R
⊢ HenselianLocalRing R →
    ∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀
[PROOFSTEP]
intro hR K _K φ hφ f hf a₀ h₁ h₂
[GOAL]
case _1_3
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
_2_1 :
  (∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ↑φ
f : R[X]
hf : Monic f
a₀ : K
h₁ : eval₂ φ a₀ f = 0
h₂ : eval₂ φ a₀ (↑derivative f) ≠ 0
⊢ ∃ a, IsRoot f a ∧ ↑φ a = a₀
[PROOFSTEP]
obtain ⟨a₀, rfl⟩ := hφ a₀
[GOAL]
case _1_3.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
_2_1 :
  (∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ↑φ
f : R[X]
hf : Monic f
a₀ : R
h₁ : eval₂ φ (↑φ a₀) f = 0
h₂ : eval₂ φ (↑φ a₀) (↑derivative f) ≠ 0
⊢ ∃ a, IsRoot f a ∧ ↑φ a = ↑φ a₀
[PROOFSTEP]
have H := HenselianLocalRing.is_henselian f hf a₀
[GOAL]
case _1_3.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
_2_1 :
  (∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ↑φ
f : R[X]
hf : Monic f
a₀ : R
h₁ : eval₂ φ (↑φ a₀) f = 0
h₂ : eval₂ φ (↑φ a₀) (↑derivative f) ≠ 0
H :
  Polynomial.eval a₀ f ∈ maximalIdeal R →
    IsUnit (Polynomial.eval a₀ (↑derivative f)) → ∃ a, IsRoot f a ∧ a - a₀ ∈ maximalIdeal R
⊢ ∃ a, IsRoot f a ∧ ↑φ a = ↑φ a₀
[PROOFSTEP]
simp only [← ker_eq_maximalIdeal φ hφ, eval₂_at_apply, RingHom.mem_ker φ] at H h₁ h₂ 
[GOAL]
case _1_3.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
_2_1 :
  (∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ↑φ
f : R[X]
hf : Monic f
a₀ : R
H : ↑φ (Polynomial.eval a₀ f) = 0 → IsUnit (Polynomial.eval a₀ (↑derivative f)) → ∃ a, IsRoot f a ∧ ↑φ (a - a₀) = 0
h₁ : ↑φ (Polynomial.eval a₀ f) = 0
h₂ : ↑φ (Polynomial.eval a₀ (↑derivative f)) ≠ 0
⊢ ∃ a, IsRoot f a ∧ ↑φ a = ↑φ a₀
[PROOFSTEP]
obtain ⟨a, ha₁, ha₂⟩ :=
  H h₁
    (by
      contrapose! h₂
      rwa [← mem_nonunits_iff, ← LocalRing.mem_maximalIdeal, ← LocalRing.ker_eq_maximalIdeal φ hφ, RingHom.mem_ker] at
        h₂ )
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
_2_1 :
  (∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ↑φ
f : R[X]
hf : Monic f
a₀ : R
H : ↑φ (Polynomial.eval a₀ f) = 0 → IsUnit (Polynomial.eval a₀ (↑derivative f)) → ∃ a, IsRoot f a ∧ ↑φ (a - a₀) = 0
h₁ : ↑φ (Polynomial.eval a₀ f) = 0
h₂ : ↑φ (Polynomial.eval a₀ (↑derivative f)) ≠ 0
⊢ IsUnit (Polynomial.eval a₀ (↑derivative f))
[PROOFSTEP]
contrapose! h₂
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
_2_1 :
  (∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ↑φ
f : R[X]
hf : Monic f
a₀ : R
H : ↑φ (Polynomial.eval a₀ f) = 0 → IsUnit (Polynomial.eval a₀ (↑derivative f)) → ∃ a, IsRoot f a ∧ ↑φ (a - a₀) = 0
h₁ : ↑φ (Polynomial.eval a₀ f) = 0
h₂ : ¬IsUnit (Polynomial.eval a₀ (↑derivative f))
⊢ ↑φ (Polynomial.eval a₀ (↑derivative f)) = 0
[PROOFSTEP]
rwa [← mem_nonunits_iff, ← LocalRing.mem_maximalIdeal, ← LocalRing.ker_eq_maximalIdeal φ hφ, RingHom.mem_ker] at h₂ 
[GOAL]
case _1_3.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
_2_1 :
  (∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ↑φ
f : R[X]
hf : Monic f
a₀ : R
H : ↑φ (Polynomial.eval a₀ f) = 0 → IsUnit (Polynomial.eval a₀ (↑derivative f)) → ∃ a, IsRoot f a ∧ ↑φ (a - a₀) = 0
h₁ : ↑φ (Polynomial.eval a₀ f) = 0
h₂ : ↑φ (Polynomial.eval a₀ (↑derivative f)) ≠ 0
a : R
ha₁ : IsRoot f a
ha₂ : ↑φ (a - a₀) = 0
⊢ ∃ a, IsRoot f a ∧ ↑φ a = ↑φ a₀
[PROOFSTEP]
refine' ⟨a, ha₁, _⟩
[GOAL]
case _1_3.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
_2_1 :
  (∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ↑φ
f : R[X]
hf : Monic f
a₀ : R
H : ↑φ (Polynomial.eval a₀ f) = 0 → IsUnit (Polynomial.eval a₀ (↑derivative f)) → ∃ a, IsRoot f a ∧ ↑φ (a - a₀) = 0
h₁ : ↑φ (Polynomial.eval a₀ f) = 0
h₂ : ↑φ (Polynomial.eval a₀ (↑derivative f)) ≠ 0
a : R
ha₁ : IsRoot f a
ha₂ : ↑φ (a - a₀) = 0
⊢ ↑φ a = ↑φ a₀
[PROOFSTEP]
rwa [φ.map_sub, sub_eq_zero] at ha₂ 
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : LocalRing R
_3_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀) →
    ∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀
_2_1 :
  (∀ (f : R[X]),
      Monic f →
        ∀ (a₀ : ResidueField R),
          ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀) →
    HenselianLocalRing R
_1_3 :
  HenselianLocalRing R →
    ∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ↑φ →
        ∀ (f : R[X]),
          Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀
⊢ List.TFAE
    [HenselianLocalRing R,
      ∀ (f : R[X]),
        Monic f →
          ∀ (a₀ : ResidueField R),
            ↑(aeval a₀) f = 0 → ↑(aeval a₀) (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑(residue R) a = a₀,
      ∀ {K : Type u} [inst : Field K] (φ : R →+* K),
        Surjective ↑φ →
          ∀ (f : R[X]),
            Monic f → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (↑derivative f) ≠ 0 → ∃ a, IsRoot f a ∧ ↑φ a = a₀]
[PROOFSTEP]
tfae_finish
[GOAL]
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
⊢ maximalIdeal R ≤ Ideal.jacobson ⊥
[PROOFSTEP]
rw [Ideal.jacobson, le_sInf_iff]
[GOAL]
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
⊢ ∀ (b : Ideal R), b ∈ {J | ⊥ ≤ J ∧ Ideal.IsMaximal J} → maximalIdeal R ≤ b
[PROOFSTEP]
rintro I ⟨-, hI⟩
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
I : Ideal R
hI : Ideal.IsMaximal I
⊢ maximalIdeal R ≤ I
[PROOFSTEP]
exact (eq_maximalIdeal hI).ge
[GOAL]
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
⊢ ∀ (f : R[X]),
    Monic f →
      ∀ (a₀ : R),
        Polynomial.eval a₀ f ∈ maximalIdeal R →
          IsUnit (↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (↑derivative f))) →
            ∃ a, IsRoot f a ∧ a - a₀ ∈ maximalIdeal R
[PROOFSTEP]
intro f hf a₀ h₁ h₂
[GOAL]
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal R
h₂ : IsUnit (↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (↑derivative f)))
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ maximalIdeal R
[PROOFSTEP]
refine' HenselianLocalRing.is_henselian f hf a₀ h₁ _
[GOAL]
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal R
h₂ : IsUnit (↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (↑derivative f)))
⊢ IsUnit (Polynomial.eval a₀ (↑derivative f))
[PROOFSTEP]
contrapose! h₂
[GOAL]
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal R
h₂ : ¬IsUnit (Polynomial.eval a₀ (↑derivative f))
⊢ ¬IsUnit (↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (↑derivative f)))
[PROOFSTEP]
rw [← mem_nonunits_iff, ← LocalRing.mem_maximalIdeal, ← Ideal.Quotient.eq_zero_iff_mem] at h₂ 
[GOAL]
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal R
h₂✝ : Polynomial.eval a₀ (↑derivative f) ∈ nonunits R
h₂ : ↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (↑derivative f)) = 0
⊢ ¬IsUnit (↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (↑derivative f)))
[PROOFSTEP]
rw [h₂]
[GOAL]
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal R
h₂✝ : Polynomial.eval a₀ (↑derivative f) ∈ nonunits R
h₂ : ↑(Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (↑derivative f)) = 0
⊢ ¬IsUnit 0
[PROOFSTEP]
exact not_isUnit_zero
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
⊢ ∀ (f : R[X]),
    Monic f →
      ∀ (a₀ : R),
        Polynomial.eval a₀ f ∈ I →
          IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f))) → ∃ a, IsRoot f a ∧ a - a₀ ∈ I
[PROOFSTEP]
intro f _ a₀ h₁ h₂
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ I
[PROOFSTEP]
classical
let f' := derivative f
let c : ℕ → R := fun n => Nat.recOn n a₀ fun _ b => b - f.eval b * Ring.inverse (f'.eval b)
have hc : ∀ n, c (n + 1) = c n - f.eval (c n) * Ring.inverse (f'.eval (c n)) :=
  by
  intro n
  simp only [Nat.rec_add_one]
    -- we now spend some time determining properties of the sequence `c : ℕ → R`
          -- `hc_mod`: for every `n`, we have `c n ≡ a₀ [SMOD I]`
          -- `hf'c`  : for every `n`, `f'.eval (c n)` is a unit
          -- `hfcI`  : for every `n`, `f.eval (c n)` is contained in `I ^ (n+1)`
have hc_mod : ∀ n, c n ≡ a₀ [SMOD I] := by
  intro n
  induction' n with n ih
  · rfl
  rw [Nat.succ_eq_add_one, hc, sub_eq_add_neg, ← add_zero a₀]
  refine' ih.add _
  rw [SModEq.zero, Ideal.neg_mem_iff]
  refine' I.mul_mem_right _ _
  rw [← SModEq.zero] at h₁ ⊢
  exact (ih.eval f).trans h₁
have hf'c : ∀ n, IsUnit (f'.eval (c n)) := by
  intro n
  haveI := isLocalRingHom_of_le_jacobson_bot I (IsAdicComplete.le_jacobson_bot I)
  apply isUnit_of_map_unit (Ideal.Quotient.mk I)
  convert h₂ using 1
  exact SModEq.def.mp ((hc_mod n).eval _)
have hfcI : ∀ n, f.eval (c n) ∈ I ^ (n + 1) := by
  intro n
  induction' n with n ih
  · simpa only [Nat.zero_eq, Nat.rec_zero, zero_add, pow_one] using h₁
  rw [Nat.succ_eq_add_one, ← taylor_eval_sub (c n), hc, sub_eq_add_neg, sub_eq_add_neg, add_neg_cancel_comm]
  rw [eval_eq_sum, sum_over_range' _ _ _ (lt_add_of_pos_right _ zero_lt_two), ←
    Finset.sum_range_add_sum_Ico _ (Nat.le_add_left _ _)]
  swap
  · intro i
    rw [zero_mul]
  refine' Ideal.add_mem _ _ _
  · erw [Finset.sum_range_succ]
    rw [Finset.range_one, Finset.sum_singleton, taylor_coeff_zero, taylor_coeff_one, pow_zero, pow_one, mul_one,
      mul_neg, mul_left_comm, Ring.mul_inverse_cancel _ (hf'c n), mul_one, add_neg_self]
    exact Ideal.zero_mem _
  · refine' Submodule.sum_mem _ _
    simp only [Finset.mem_Ico]
    rintro i ⟨h2i, _⟩
    have aux : n + 2 ≤ i * (n + 1) := by trans 2 * (n + 1) <;> nlinarith only [h2i]
    refine' Ideal.mul_mem_left _ _ (Ideal.pow_le_pow aux _)
    rw [pow_mul']
    refine'
      Ideal.pow_mem_pow ((Ideal.neg_mem_iff _).2 <| Ideal.mul_mem_right _ _ ih)
        _
          -- we are now in the position to show that `c : ℕ → R` is a Cauchy sequence
have aux : ∀ m n, m ≤ n → c m ≡ c n [SMOD (I ^ m • ⊤ : Ideal R)] :=
  by
  intro m n hmn
  rw [← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one]
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  clear hmn
  induction' k with k ih
  · rw [Nat.zero_eq, add_zero]
  rw [Nat.succ_eq_add_one, ← add_assoc, hc, ← add_zero (c m), sub_eq_add_neg]
  refine' ih.add _
  symm
  rw [SModEq.zero, Ideal.neg_mem_iff]
  refine' Ideal.mul_mem_right _ _ (Ideal.pow_le_pow _ (hfcI _))
  rw [add_assoc]
  exact le_self_add
obtain ⟨a, ha⟩ := IsPrecomplete.prec' c (aux _ _)
refine' ⟨a, _, _⟩
· show f.IsRoot a
  suffices ∀ n, f.eval a ≡ 0 [SMOD (I ^ n • ⊤ : Ideal R)] by exact IsHausdorff.haus' _ this
  intro n
  specialize ha n
  rw [← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one] at ha ⊢
  refine' (ha.symm.eval f).trans _
  rw [SModEq.zero]
  exact Ideal.pow_le_pow le_self_add (hfcI _)
· show a - a₀ ∈ I
  specialize ha 1
  rw [hc, pow_one, ← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one, sub_eq_add_neg] at ha 
  rw [← SModEq.sub_mem, ← add_zero a₀]
  refine' ha.symm.trans (SModEq.rfl.add _)
  rw [SModEq.zero, Ideal.neg_mem_iff]
  exact Ideal.mul_mem_right _ _ h₁
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ I
[PROOFSTEP]
let f' := derivative f
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ I
[PROOFSTEP]
let c : ℕ → R := fun n => Nat.recOn n a₀ fun _ b => b - f.eval b * Ring.inverse (f'.eval b)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ I
[PROOFSTEP]
have hc : ∀ n, c (n + 1) = c n - f.eval (c n) * Ring.inverse (f'.eval (c n)) :=
  by
  intro n
  simp only [Nat.rec_add_one]
    -- we now spend some time determining properties of the sequence `c : ℕ → R`
          -- `hc_mod`: for every `n`, we have `c n ≡ a₀ [SMOD I]`
          -- `hf'c`  : for every `n`, `f'.eval (c n)` is a unit
          -- `hfcI`  : for every `n`, `f.eval (c n)` is contained in `I ^ (n+1)`
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
⊢ ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
[PROOFSTEP]
intro n
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
n : ℕ
⊢ c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
[PROOFSTEP]
simp only [Nat.rec_add_one]
  -- we now spend some time determining properties of the sequence `c : ℕ → R`
        -- `hc_mod`: for every `n`, we have `c n ≡ a₀ [SMOD I]`
        -- `hf'c`  : for every `n`, `f'.eval (c n)` is a unit
        -- `hfcI`  : for every `n`, `f.eval (c n)` is contained in `I ^ (n+1)`
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ I
[PROOFSTEP]
have hc_mod : ∀ n, c n ≡ a₀ [SMOD I] := by
  intro n
  induction' n with n ih
  · rfl
  rw [Nat.succ_eq_add_one, hc, sub_eq_add_neg, ← add_zero a₀]
  refine' ih.add _
  rw [SModEq.zero, Ideal.neg_mem_iff]
  refine' I.mul_mem_right _ _
  rw [← SModEq.zero] at h₁ ⊢
  exact (ih.eval f).trans h₁
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
⊢ ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
[PROOFSTEP]
intro n
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
n : ℕ
⊢ c n ≡ a₀ [SMOD I]
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
⊢ c Nat.zero ≡ a₀ [SMOD I]
[PROOFSTEP]
rfl
[GOAL]
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
n : ℕ
ih : c n ≡ a₀ [SMOD I]
⊢ c (Nat.succ n) ≡ a₀ [SMOD I]
[PROOFSTEP]
rw [Nat.succ_eq_add_one, hc, sub_eq_add_neg, ← add_zero a₀]
[GOAL]
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
n : ℕ
ih : c n ≡ a₀ [SMOD I]
⊢ c n + -(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')) ≡ a₀ + 0 [SMOD I]
[PROOFSTEP]
refine' ih.add _
[GOAL]
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
n : ℕ
ih : c n ≡ a₀ [SMOD I]
⊢ -(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')) ≡ 0 [SMOD I]
[PROOFSTEP]
rw [SModEq.zero, Ideal.neg_mem_iff]
[GOAL]
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
n : ℕ
ih : c n ≡ a₀ [SMOD I]
⊢ Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f') ∈ I
[PROOFSTEP]
refine' I.mul_mem_right _ _
[GOAL]
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
n : ℕ
ih : c n ≡ a₀ [SMOD I]
⊢ Polynomial.eval (c n) f ∈ I
[PROOFSTEP]
rw [← SModEq.zero] at h₁ ⊢
[GOAL]
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ≡ 0 [SMOD I]
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : R[X] := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
n : ℕ
ih : c n ≡ a₀ [SMOD I]
⊢ Polynomial.eval (c n) f ≡ 0 [SMOD I]
[PROOFSTEP]
exact (ih.eval f).trans h₁
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ I
[PROOFSTEP]
have hf'c : ∀ n, IsUnit (f'.eval (c n)) := by
  intro n
  haveI := isLocalRingHom_of_le_jacobson_bot I (IsAdicComplete.le_jacobson_bot I)
  apply isUnit_of_map_unit (Ideal.Quotient.mk I)
  convert h₂ using 1
  exact SModEq.def.mp ((hc_mod n).eval _)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
⊢ ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
[PROOFSTEP]
intro n
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
n : ℕ
⊢ IsUnit (Polynomial.eval (c n) f')
[PROOFSTEP]
haveI := isLocalRingHom_of_le_jacobson_bot I (IsAdicComplete.le_jacobson_bot I)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
n : ℕ
this : IsLocalRingHom (Ideal.Quotient.mk I)
⊢ IsUnit (Polynomial.eval (c n) f')
[PROOFSTEP]
apply isUnit_of_map_unit (Ideal.Quotient.mk I)
[GOAL]
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
n : ℕ
this : IsLocalRingHom (Ideal.Quotient.mk I)
⊢ IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval (c n) f'))
[PROOFSTEP]
convert h₂ using 1
[GOAL]
case h.e'_3
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
n : ℕ
this : IsLocalRingHom (Ideal.Quotient.mk I)
⊢ ↑(Ideal.Quotient.mk I) (Polynomial.eval (c n) f') = ↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f))
[PROOFSTEP]
exact SModEq.def.mp ((hc_mod n).eval _)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ I
[PROOFSTEP]
have hfcI : ∀ n, f.eval (c n) ∈ I ^ (n + 1) := by
  intro n
  induction' n with n ih
  · simpa only [Nat.zero_eq, Nat.rec_zero, zero_add, pow_one] using h₁
  rw [Nat.succ_eq_add_one, ← taylor_eval_sub (c n), hc, sub_eq_add_neg, sub_eq_add_neg, add_neg_cancel_comm]
  rw [eval_eq_sum, sum_over_range' _ _ _ (lt_add_of_pos_right _ zero_lt_two), ←
    Finset.sum_range_add_sum_Ico _ (Nat.le_add_left _ _)]
  swap
  · intro i
    rw [zero_mul]
  refine' Ideal.add_mem _ _ _
  · erw [Finset.sum_range_succ]
    rw [Finset.range_one, Finset.sum_singleton, taylor_coeff_zero, taylor_coeff_one, pow_zero, pow_one, mul_one,
      mul_neg, mul_left_comm, Ring.mul_inverse_cancel _ (hf'c n), mul_one, add_neg_self]
    exact Ideal.zero_mem _
  · refine' Submodule.sum_mem _ _
    simp only [Finset.mem_Ico]
    rintro i ⟨h2i, _⟩
    have aux : n + 2 ≤ i * (n + 1) := by trans 2 * (n + 1) <;> nlinarith only [h2i]
    refine' Ideal.mul_mem_left _ _ (Ideal.pow_le_pow aux _)
    rw [pow_mul']
    refine'
      Ideal.pow_mem_pow ((Ideal.neg_mem_iff _).2 <| Ideal.mul_mem_right _ _ ih)
        _
          -- we are now in the position to show that `c : ℕ → R` is a Cauchy sequence
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
⊢ ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
[PROOFSTEP]
intro n
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
⊢ Polynomial.eval (c n) f ∈ I ^ (n + 1)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
⊢ Polynomial.eval (c Nat.zero) f ∈ I ^ (Nat.zero + 1)
[PROOFSTEP]
simpa only [Nat.zero_eq, Nat.rec_zero, zero_add, pow_one] using h₁
[GOAL]
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ Polynomial.eval (c (Nat.succ n)) f ∈ I ^ (Nat.succ n + 1)
[PROOFSTEP]
rw [Nat.succ_eq_add_one, ← taylor_eval_sub (c n), hc, sub_eq_add_neg, sub_eq_add_neg, add_neg_cancel_comm]
[GOAL]
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ Polynomial.eval (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) (↑(taylor (c n)) f) ∈
    I ^ (n + 1 + 1)
[PROOFSTEP]
rw [eval_eq_sum, sum_over_range' _ _ _ (lt_add_of_pos_right _ zero_lt_two), ←
  Finset.sum_range_add_sum_Ico _ (Nat.le_add_left _ _)]
[GOAL]
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ k in Finset.range 2,
        coeff (↑(taylor (c n)) f) k * (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) ^ k +
      ∑ k in Finset.Ico 2 (natDegree (↑(taylor (c n)) f) + 2),
        coeff (↑(taylor (c n)) f) k * (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) ^ k ∈
    I ^ (n + 1 + 1)
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∀ (n_1 : ℕ), 0 * (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) ^ n_1 = 0
[PROOFSTEP]
swap
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∀ (n_1 : ℕ), 0 * (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) ^ n_1 = 0
[PROOFSTEP]
intro i
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
⊢ 0 * (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) ^ i = 0
[PROOFSTEP]
rw [zero_mul]
[GOAL]
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ k in Finset.range 2,
        coeff (↑(taylor (c n)) f) k * (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) ^ k +
      ∑ k in Finset.Ico 2 (natDegree (↑(taylor (c n)) f) + 2),
        coeff (↑(taylor (c n)) f) k * (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) ^ k ∈
    I ^ (n + 1 + 1)
[PROOFSTEP]
refine' Ideal.add_mem _ _ _
[GOAL]
case succ.refine'_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ k in Finset.range 2,
      coeff (↑(taylor (c n)) f) k * (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) ^ k ∈
    I ^ (n + 1 + 1)
[PROOFSTEP]
erw [Finset.sum_range_succ]
[GOAL]
case succ.refine'_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ x in Finset.range 1,
        coeff (↑(taylor (c n)) f) x * (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) ^ x +
      coeff (↑(taylor (c n)) f) 1 * (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) ^ 1 ∈
    I ^ (n + 1 + 1)
[PROOFSTEP]
rw [Finset.range_one, Finset.sum_singleton, taylor_coeff_zero, taylor_coeff_one, pow_zero, pow_one, mul_one, mul_neg,
  mul_left_comm, Ring.mul_inverse_cancel _ (hf'c n), mul_one, add_neg_self]
[GOAL]
case succ.refine'_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ 0 ∈ I ^ (n + 1 + 1)
[PROOFSTEP]
exact Ideal.zero_mem _
[GOAL]
case succ.refine'_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ k in Finset.Ico 2 (natDegree (↑(taylor (c n)) f) + 2),
      coeff (↑(taylor (c n)) f) k * (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) ^ k ∈
    I ^ (n + 1 + 1)
[PROOFSTEP]
refine' Submodule.sum_mem _ _
[GOAL]
case succ.refine'_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∀ (c_1 : ℕ),
    c_1 ∈ Finset.Ico 2 (natDegree (↑(taylor (c n)) f) + 2) →
      coeff (↑(taylor (c n)) f) c_1 * (-(Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f'))) ^ c_1 ∈
        I ^ (n + 1 + 1)
[PROOFSTEP]
simp only [Finset.mem_Ico]
[GOAL]
case succ.refine'_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∀ (c : ℕ),
    2 ≤ c ∧
        c <
          natDegree
              (↑(taylor
                    (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f)))
                      n))
                f) +
            2 →
      coeff
            (↑(taylor
                  (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f)))
                    n))
              f)
            c *
          (-(Polynomial.eval
                  (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n)
                  f *
                Ring.inverse
                  (Polynomial.eval
                    (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f)))
                      n)
                    (↑derivative f)))) ^
            c ∈
        I ^ (n + 1 + 1)
[PROOFSTEP]
rintro i ⟨h2i, _⟩
[GOAL]
case succ.refine'_2.intro
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ :
  i <
    natDegree
        (↑(taylor
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n))
          f) +
      2
⊢ coeff
        (↑(taylor
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n))
          f)
        i *
      (-(Polynomial.eval
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n) f *
            Ring.inverse
              (Polynomial.eval
                (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n)
                (↑derivative f)))) ^
        i ∈
    I ^ (n + 1 + 1)
[PROOFSTEP]
have aux : n + 2 ≤ i * (n + 1) := by trans 2 * (n + 1) <;> nlinarith only [h2i]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ :
  i <
    natDegree
        (↑(taylor
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n))
          f) +
      2
⊢ n + 2 ≤ i * (n + 1)
[PROOFSTEP]
trans 2 * (n + 1)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ :
  i <
    natDegree
        (↑(taylor
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n))
          f) +
      2
⊢ n + 2 ≤ 2 * (n + 1)
[PROOFSTEP]
nlinarith only [h2i]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ :
  i <
    natDegree
        (↑(taylor
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n))
          f) +
      2
⊢ 2 * (n + 1) ≤ i * (n + 1)
[PROOFSTEP]
nlinarith only [h2i]
[GOAL]
case succ.refine'_2.intro
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ :
  i <
    natDegree
        (↑(taylor
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n))
          f) +
      2
aux : n + 2 ≤ i * (n + 1)
⊢ coeff
        (↑(taylor
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n))
          f)
        i *
      (-(Polynomial.eval
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n) f *
            Ring.inverse
              (Polynomial.eval
                (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n)
                (↑derivative f)))) ^
        i ∈
    I ^ (n + 1 + 1)
[PROOFSTEP]
refine' Ideal.mul_mem_left _ _ (Ideal.pow_le_pow aux _)
[GOAL]
case succ.refine'_2.intro
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ :
  i <
    natDegree
        (↑(taylor
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n))
          f) +
      2
aux : n + 2 ≤ i * (n + 1)
⊢ (-(Polynomial.eval
            (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n) f *
          Ring.inverse
            (Polynomial.eval
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n)
              (↑derivative f)))) ^
      i ∈
    I ^ (i * (n + 1))
[PROOFSTEP]
rw [pow_mul']
[GOAL]
case succ.refine'_2.intro
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ :
  i <
    natDegree
        (↑(taylor
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n))
          f) +
      2
aux : n + 2 ≤ i * (n + 1)
⊢ (-(Polynomial.eval
            (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n) f *
          Ring.inverse
            (Polynomial.eval
              (Nat.rec a₀ (fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b (↑derivative f))) n)
              (↑derivative f)))) ^
      i ∈
    (I ^ (n + 1)) ^ i
[PROOFSTEP]
refine'
  Ideal.pow_mem_pow ((Ideal.neg_mem_iff _).2 <| Ideal.mul_mem_right _ _ ih)
    _
      -- we are now in the position to show that `c : ℕ → R` is a Cauchy sequence
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ I
[PROOFSTEP]
have aux : ∀ m n, m ≤ n → c m ≡ c n [SMOD (I ^ m • ⊤ : Ideal R)] :=
  by
  intro m n hmn
  rw [← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one]
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  clear hmn
  induction' k with k ih
  · rw [Nat.zero_eq, add_zero]
  rw [Nat.succ_eq_add_one, ← add_assoc, hc, ← add_zero (c m), sub_eq_add_neg]
  refine' ih.add _
  symm
  rw [SModEq.zero, Ideal.neg_mem_iff]
  refine' Ideal.mul_mem_right _ _ (Ideal.pow_le_pow _ (hfcI _))
  rw [add_assoc]
  exact le_self_add
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
[PROOFSTEP]
intro m n hmn
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m n : ℕ
hmn : m ≤ n
⊢ c m ≡ c n [SMOD I ^ m • ⊤]
[PROOFSTEP]
rw [← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m n : ℕ
hmn : m ≤ n
⊢ c m ≡ c n [SMOD I ^ m]
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
hmn : m ≤ m + k
⊢ c m ≡ c (m + k) [SMOD I ^ m]
[PROOFSTEP]
clear hmn
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
⊢ c m ≡ c (m + k) [SMOD I ^ m]
[PROOFSTEP]
induction' k with k ih
[GOAL]
case intro.zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m : ℕ
⊢ c m ≡ c (m + Nat.zero) [SMOD I ^ m]
[PROOFSTEP]
rw [Nat.zero_eq, add_zero]
[GOAL]
case intro.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ c m ≡ c (m + Nat.succ k) [SMOD I ^ m]
[PROOFSTEP]
rw [Nat.succ_eq_add_one, ← add_assoc, hc, ← add_zero (c m), sub_eq_add_neg]
[GOAL]
case intro.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ c m + 0 ≡ c (m + k) + -(Polynomial.eval (c (m + k)) f * Ring.inverse (Polynomial.eval (c (m + k)) f')) [SMOD I ^ m]
[PROOFSTEP]
refine' ih.add _
[GOAL]
case intro.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ 0 ≡ -(Polynomial.eval (c (m + k)) f * Ring.inverse (Polynomial.eval (c (m + k)) f')) [SMOD I ^ m]
[PROOFSTEP]
symm
[GOAL]
case intro.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ -(Polynomial.eval (c (m + k)) f * Ring.inverse (Polynomial.eval (c (m + k)) f')) ≡ 0 [SMOD I ^ m]
[PROOFSTEP]
rw [SModEq.zero, Ideal.neg_mem_iff]
[GOAL]
case intro.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ Polynomial.eval (c (m + k)) f * Ring.inverse (Polynomial.eval (c (m + k)) f') ∈ I ^ m
[PROOFSTEP]
refine' Ideal.mul_mem_right _ _ (Ideal.pow_le_pow _ (hfcI _))
[GOAL]
case intro.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ m ≤ m + k + 1
[PROOFSTEP]
rw [add_assoc]
[GOAL]
case intro.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ m ≤ m + (k + 1)
[PROOFSTEP]
exact le_self_add
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ I
[PROOFSTEP]
obtain ⟨a, ha⟩ := IsPrecomplete.prec' c (aux _ _)
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : ∀ (n : ℕ), c n ≡ a [SMOD I ^ n • ⊤]
⊢ ∃ a, IsRoot f a ∧ a - a₀ ∈ I
[PROOFSTEP]
refine' ⟨a, _, _⟩
[GOAL]
case intro.refine'_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : ∀ (n : ℕ), c n ≡ a [SMOD I ^ n • ⊤]
⊢ IsRoot f a
[PROOFSTEP]
show f.IsRoot a
[GOAL]
case intro.refine'_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : ∀ (n : ℕ), c n ≡ a [SMOD I ^ n • ⊤]
⊢ IsRoot f a
[PROOFSTEP]
suffices ∀ n, f.eval a ≡ 0 [SMOD (I ^ n • ⊤ : Ideal R)] by exact IsHausdorff.haus' _ this
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : ∀ (n : ℕ), c n ≡ a [SMOD I ^ n • ⊤]
this : ∀ (n : ℕ), Polynomial.eval a f ≡ 0 [SMOD I ^ n • ⊤]
⊢ IsRoot f a
[PROOFSTEP]
exact IsHausdorff.haus' _ this
[GOAL]
case intro.refine'_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : ∀ (n : ℕ), c n ≡ a [SMOD I ^ n • ⊤]
⊢ ∀ (n : ℕ), Polynomial.eval a f ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
intro n
[GOAL]
case intro.refine'_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : ∀ (n : ℕ), c n ≡ a [SMOD I ^ n • ⊤]
n : ℕ
⊢ Polynomial.eval a f ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
specialize ha n
[GOAL]
case intro.refine'_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
n : ℕ
ha : c n ≡ a [SMOD I ^ n • ⊤]
⊢ Polynomial.eval a f ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
rw [← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one] at ha ⊢
[GOAL]
case intro.refine'_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
n : ℕ
ha : c n ≡ a [SMOD I ^ n]
⊢ Polynomial.eval a f ≡ 0 [SMOD I ^ n]
[PROOFSTEP]
refine' (ha.symm.eval f).trans _
[GOAL]
case intro.refine'_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
n : ℕ
ha : c n ≡ a [SMOD I ^ n]
⊢ Polynomial.eval (c n) f ≡ 0 [SMOD I ^ n]
[PROOFSTEP]
rw [SModEq.zero]
[GOAL]
case intro.refine'_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
n : ℕ
ha : c n ≡ a [SMOD I ^ n]
⊢ Polynomial.eval (c n) f ∈ I ^ n
[PROOFSTEP]
exact Ideal.pow_le_pow le_self_add (hfcI _)
[GOAL]
case intro.refine'_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : ∀ (n : ℕ), c n ≡ a [SMOD I ^ n • ⊤]
⊢ a - a₀ ∈ I
[PROOFSTEP]
show a - a₀ ∈ I
[GOAL]
case intro.refine'_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : ∀ (n : ℕ), c n ≡ a [SMOD I ^ n • ⊤]
⊢ a - a₀ ∈ I
[PROOFSTEP]
specialize ha 1
[GOAL]
case intro.refine'_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 1 ≡ a [SMOD I ^ 1 • ⊤]
⊢ a - a₀ ∈ I
[PROOFSTEP]
rw [hc, pow_one, ← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one, sub_eq_add_neg] at ha 
[GOAL]
case intro.refine'_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 0 + -(Polynomial.eval (c 0) f * Ring.inverse (Polynomial.eval (c 0) f')) ≡ a [SMOD I]
⊢ a - a₀ ∈ I
[PROOFSTEP]
rw [← SModEq.sub_mem, ← add_zero a₀]
[GOAL]
case intro.refine'_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 0 + -(Polynomial.eval (c 0) f * Ring.inverse (Polynomial.eval (c 0) f')) ≡ a [SMOD I]
⊢ a ≡ a₀ + 0 [SMOD I]
[PROOFSTEP]
refine' ha.symm.trans (SModEq.rfl.add _)
[GOAL]
case intro.refine'_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 0 + -(Polynomial.eval (c 0) f * Ring.inverse (Polynomial.eval (c 0) f')) ≡ a [SMOD I]
⊢ -(Polynomial.eval (c 0) f * Ring.inverse (Polynomial.eval (c 0) f')) ≡ 0 [SMOD I]
[PROOFSTEP]
rw [SModEq.zero, Ideal.neg_mem_iff]
[GOAL]
case intro.refine'_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : Monic f
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit (↑(Ideal.Quotient.mk I) (Polynomial.eval a₀ (↑derivative f)))
f' : (fun x => R[X]) f := ↑derivative f
c : ℕ → R := fun n => Nat.recOn n a₀ fun x b => b - Polynomial.eval b f * Ring.inverse (Polynomial.eval b f')
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * Ring.inverse (Polynomial.eval (c n) f')
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 0 + -(Polynomial.eval (c 0) f * Ring.inverse (Polynomial.eval (c 0) f')) ≡ a [SMOD I]
⊢ Polynomial.eval (c 0) f * Ring.inverse (Polynomial.eval (c 0) f') ∈ I
[PROOFSTEP]
exact Ideal.mul_mem_right _ _ h₁
