mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ.refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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)

Tactic:
]

Goal state after:
case succ.refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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)
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv f.toLinearMap * toConv (f.toLinearMap ∘ₗ antipode R)).ofConv =
    (toConv ((↑f).toLinearMap ∘ₗ (toConv LinearMap.id).ofConv) *
        toConv ((↑f).toLinearMap ∘ₗ (toConv (antipode R)).ofConv)).ofConv

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv f.toLinearMap * toConv (f.toLinearMap ∘ₗ antipode R)).ofConv =
    (toConv ((↑f).toLinearMap ∘ₗ (toConv LinearMap.id).ofConv) *
        toConv ((↑f).toLinearMap ∘ₗ (toConv (antipode R)).ofConv)).ofConv
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingUp R S
inst✝ : HasGoingUp S T
⊢ SpecializingMap (PrimeSpectrum.comap ((algebraMap S T).comp (algebraMap R S)))

Tactic:
]

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingUp R S
inst✝ : HasGoingUp S T
⊢ SpecializingMap (PrimeSpectrum.comap ((algebraMap S T).comp (algebraMap R S)))
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case hf
R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingUp R S
inst✝ : HasGoingUp S T
⊢ HasGoingUp S T

Tactic:
]

Goal state after:
case hf
R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingUp R S
inst✝ : HasGoingUp S T
⊢ HasGoingUp S T
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case hg
R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingUp R S
inst✝ : HasGoingUp S T
⊢ HasGoingUp R S

Tactic:
]

Goal state after:
case hg
R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingUp R S
inst✝ : HasGoingUp S T
⊢ HasGoingUp R S
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 < ((taylor (c n)) f).natDegree + 2
aux : n + 2 ≤ i * (n + 1)
⊢ (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ i ∈ (I ^ (n + 1)) ^ i

Tactic:
]

Goal state after:
case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 < ((taylor (c n)) f).natDegree + 2
aux : n + 2 ≤ i * (n + 1)
⊢ (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ i ∈ (I ^ (n + 1)) ^ i
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 < ((taylor (c n)) f).natDegree + 2
aux : n + 2 ≤ i * (n + 1)
⊢ (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ i ∈ I ^ (i * (n + 1))

Tactic:
rw [pow_mul']

Goal state after:
case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 < ((taylor (c n)) f).natDegree + 2
aux : n + 2 ≤ i * (n + 1)
⊢ (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ i ∈ (I ^ (n + 1)) ^ i
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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]

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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]
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 [SMOD I ^ m]

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 * (Polynomial.eval (c (m + k)) f')⁻¹ʳ) [SMOD I ^ m]

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 * (Polynomial.eval (c (m + k)) f')⁻¹ʳ) [SMOD I ^ m]
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 * (Polynomial.eval (c (m + k)) f')⁻¹ʳ ∈ I ^ m

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 * (Polynomial.eval (c (m + k)) f')⁻¹ʳ ∈ I ^ m
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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)

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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)
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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]

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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]
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ a [SMOD I]
⊢ a - a₀ ∈ I

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ a [SMOD I]
⊢ a - a₀ ∈ I
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ a [SMOD I]
⊢ a ≡ a₀ + 0 [SMOD I]

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ a [SMOD I]
⊢ a ≡ a₀ + 0 [SMOD I]
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ a [SMOD I]
⊢ Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ ∈ I

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ 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 * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (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 * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ a [SMOD I]
⊢ Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ ∈ I
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
hp✝ : maximalIdeal R ∈ I.minimalPrimes
hp : I.IsMinimalPrime (maximalIdeal R)
J : Ideal (R ⧸ I)
prime : J.IsPrime
⊢ Ideal.comap (algebraMap R (R ⧸ I)) J = maximalIdeal R

Tactic:
]

Goal state after:
case e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
hp✝ : maximalIdeal R ∈ I.minimalPrimes
hp : I.IsMinimalPrime (maximalIdeal R)
J : Ideal (R ⧸ I)
prime : J.IsPrime
⊢ Ideal.comap (algebraMap R (R ⧸ I)) J = maximalIdeal R
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : q.height = 0
⊢ 0 < ↑1

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : q.height = 0
⊢ 0 < ↑1
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0
this :
  ∃ b_1,
    (c * (b - a) + Polynomial.eval a (derivative f)) * b_1 = 1 ∧
      b_1 * (c * (b - a) + Polynomial.eval a (derivative f)) = 1
⊢ a = b

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0
this :
  ∃ b_1,
    (c * (b - a) + Polynomial.eval a (derivative f)) * b_1 = 1 ∧
      b_1 * (c * (b - a) + Polynomial.eval a (derivative f)) = 1
⊢ a = b