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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
x_in : x ∈ P.ker
property✝ : Cotangent.mk ⟨x, x_in⟩ ∈ P.extendScalars.cotangentComplex.ker
⊢ x ∈
    Ideal.comap (algebraMap P.Ring (Generators.self P.Ring S).toExtension.Ring)
      (Generators.self P.Ring S).toExtension.ker

Tactic:
RingHom.comap_ker,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
x_in : x ∈ P.ker
property✝ : Cotangent.mk ⟨x, x_in⟩ ∈ P.extendScalars.cotangentComplex.ker
⊢ x ∈
    RingHom.ker
      ((algebraMap (Generators.self P.Ring S).toExtension.Ring S).comp
        (algebraMap P.Ring (Generators.self P.Ring S).toExtension.Ring))
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ Function.Injective ⇑H.restrict

Tactic:
rw [injective_iff_map_eq_zero]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ ∀ (a : S ⧸ Q), H.restrict a = 0 → a = 0
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ Ideal.comap φ Q = Q

Tactic:
by
  refine le_antisymm (fun x hx ↦ ?_) H.le_comap
  rwa [← Ideal.Quotient.eq_zero_iff_mem, ← H.restrict_injective.eq_iff, map_zero, restrict_mk,
    Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap]

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ ζ ^ (i * j) - ζ ^ ((q + k) * j) ∈ Q

Tactic:
add_mul,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ ζ ^ (i * j) - ζ ^ (q * j + k * j) ∈ Q
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this✝ : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1 = 0
⊢ φ ζ = ζ ^ q

Tactic:
simp [h₂, pow_mul, hk'] at h₁

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
⊢ (map f) (cos A) = cos A'

Tactic:
by
  ext
  simp [cos, apply_ite f]

Goal state after:
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
aux₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
aux₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
subst_mul aux₁,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
aux₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
aux₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
h : ∀ (x : α), (s x).coeff g = 0
⊢ ∑ᶠ (i : α), (s i).coeff g = 0

Tactic:
finsum_congr h,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
h : ∀ (x : α), (s x).coeff g = 0
⊢ ∑ᶠ (x : α), 0 = 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
h : ∀ (x : α), (s x).coeff g = 0
⊢ ∑ᶠ (x : α), 0 = 0

Tactic:
finsum_zero

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
h : ∀ (x : α), (s x).coeff g = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
⊢ (powerSeriesFamily x ((algebraMap R R⟦X⟧) r)).hsum = (algebraMap R R⟦Γ⟧) r

Tactic:
simp only [algebraMap_eq]
    ext g
    simp only [coeff_hsum, smulFamily_toFun, coeff_C, powers_toFun, ite_smul, zero_smul]
    rw [finsum_eq_single _ 0 fun n hn => by simp [hn]]
    by_cases hg : g = 0 <;> simp [hg, Algebra.algebraMap_eq_smul_one]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ((s.smul t) i).coeff g = ∑ gh ∈ VAddAntidiagonal g ⋯, s.hsum.coeff gh.1 • t.hsum.coeff gh.2

Tactic:
simp only [coeff_hsum_eq_sum, smul_toFun, HahnModule.coeff_smul, Equiv.symm_apply_apply]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ∑ x ∈ VAddAntidiagonal g ⋯, (s i.1).coeff x.1 • (t i.2).coeff x.2 =
    ∑ x ∈ VAddAntidiagonal g ⋯,
      (∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1) • ∑ i ∈ (t.coeff x.2).support, (t i).coeff x.2
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case refine_1
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x✝ : Γ × Γ'
hgh : x✝ ∈ ↑(VAddAntidiagonal g ⋯)
⊢ (fun a ↦ a) x✝ ∈ ↑(VAddAntidiagonal g ⋯)

Tactic:
simp_all only [mem_coe, mem_vaddAntidiagonal, mem_support, ne_eq, Set.mem_iUnion, and_true]

Goal state after:
case refine_1
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x✝ : Γ × Γ'
hgh : ¬s.hsum.coeff x✝.1 = 0 ∧ ¬t.hsum.coeff x✝.2 = 0 ∧ x✝.1 +ᵥ x✝.2 = g
⊢ (∃ i, ¬(s i).coeff x✝.1 = 0) ∧ ∃ i, ¬(t i).coeff x✝.2 = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![f, 0] F.toPowerSeries = PowerSeries.subst f (subst ![PowerSeries.X, 0] F.toPowerSeries)

Tactic:
rw [PowerSeries.subst, subst_comp_subst_apply _ hf.const]
      · congr! 2 with s
        fin_cases s
        · simp [PowerSeries.X, subst]
        · simp [subst, eval₂]
      exact HasSubst.X_zero

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
n : ℕ
x✝ : Γ
⊢ (0 ^ n).coeff x✝ = ((single 0 1) n).coeff x✝

Tactic:
obtain rfl | ha := eq_or_ne n 0 <;> simp [*]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = y + (single x.order) x.leadingCoeff
oinv : Γ
hxo : oinv + x.order = 0
⊢ 1 - (single oinv) r * x = -((single oinv) r * y)

Tactic:
hxy

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = y + (single x.order) x.leadingCoeff
oinv : Γ
hxo : oinv + x.order = 0
⊢ 1 - (single oinv) r * (y + (single x.order) x.leadingCoeff) = -((single oinv) r * y)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * u = 1
h : u = x.leadingCoeff
⊢ IsUnit x

Tactic:
rw [h] at iu

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
⊢ IsUnit x
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case cons
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingUp R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.head.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver q.asIdeal
Q : Ideal S
PQlt : P < Q
hQ : Q.IsPrime
Qlo : Q.LiesOver l.head.asIdeal
⊢ ∃ L,
    L.length = (l.cons q lt).length ∧
      RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = (l.cons q lt).toList

Tactic:
obtain ⟨L, len, head, spec⟩ := ih Q

Goal state after:
case cons
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingUp R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.head.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver q.asIdeal
Q : Ideal S
PQlt : P < Q
hQ : Q.IsPrime
Qlo : Q.LiesOver l.head.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
head : RelSeries.head L = { asIdeal := Q, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ ∃ L,
    L.length = (l.cons q lt).length ∧
      RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = (l.cons q lt).toList
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:
← Ideal.one_eq_top,

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 • 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:
← Ideal.one_eq_top,

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 • 1]
⊢ Polynomial.eval a f ≡ 0 [SMOD I ^ n • 1]
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:
← Ideal.one_eq_top,

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 • 1]
⊢ a - a₀ ∈ I
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
⊢ q.height < ↑1

Tactic:
by rw [this]; exact zero_lt_one

Goal state after:
Module: Mathlib.RingTheory.IdealFilter.Topology

Goal state before:
pp: case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
hs : s ∈ 𝓝 a
t : Set A
ht : t ∈ F.addGroupFilterBasis
hts : (fun y ↦ a + y) '' t ⊆ s
⊢ ∃ I ∈ F, a +ᵥ idealSet I ⊆ s

Tactic:
rcases ht with ⟨I, hI, rfl⟩

Goal state after:
case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
hs : s ∈ 𝓝 a
I : Ideal A
hI : I ∈ F
hts : (fun y ↦ a + y) '' ↑I ⊆ s
⊢ ∃ I ∈ F, a +ᵥ idealSet I ⊆ s
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
⊢ ⨅ i, RingHom.ker (algebraMap R (Localization.AtPrime (↑i).asIdeal)) ≤
    ⨅ p, ⨅ (x : p.IsPrime), ⨅ (_ : I ≤ p), RingHom.ker (algebraMap R (Localization.AtPrime p))

Tactic:
simp only [le_iInf_iff]

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
⊢ ∀ (i : Ideal R) (i_1 : i.IsPrime),
    I ≤ i →
      ⨅ i, RingHom.ker (algebraMap R (Localization.AtPrime (↑i).asIdeal)) ≤
        RingHom.ker (algebraMap R (Localization.AtPrime i))
Module: Mathlib.RingTheory.KrullDimension.LocalRing

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
x✝ : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI✝ : I ≠ ⊥
hI_prime : I.IsPrime
x : R
hI : x ∈ I
hx : x ≠ 0
⊢ I.IsMaximal

Tactic:
have : IsLocalRing.maximalIdeal R ≤ I := le_trans (h x hx)
      ((Ideal.IsRadical.radical_le_iff hI_prime.isRadical).mpr
        ((Ideal.span_singleton_le_iff_mem I).mpr hI))

Goal state after:
case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
x✝ : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
this✝ : ¬ringKrullDim R ≤ 0
I : Ideal R
hI✝ : I ≠ ⊥
hI_prime : I.IsPrime
x : R
hI : x ∈ I
hx : x ≠ 0
this : IsLocalRing.maximalIdeal R ≤ I
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ p.height ≤ Cardinal.toENat (Submodule.spanRank I)

Tactic:
by
  classical
  rw [I.spanRank_toENat_eq_iInf_finset_card, le_iInf_iff]
  rintro ⟨s, (rfl : span s = I)⟩
  induction hn : s.card using Nat.strong_induction_on generalizing R with
  | h n H =>
    replace hn : s.card ≤ n := hn.le
    have := hp.isPrime
    cases n with
    | zero =>
      rw [ENat.natCast_zero, nonpos_iff_eq_zero, height_eq_zero_iff, minimalPrimes]
      simp_all
    | succ n =>
      wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal R
      · rw [← Localization.AtPrime.under_maximalIdeal (I := p)] at hp ⊢
        rw [IsLocalization.height_under p.primeCompl]
        rw [← Set.mem_preimage, ← IsLocalization.minimalPrimes_map p.primeCompl, map_span] at hp
        exact this _ (s.image (algebraMap R (Localization p.primeCompl))) (by simpa using hp)
          inferInstance _ H (Finset.card_image_le.trans hn) ⟨inferInstance, rfl⟩
      obtain ⟨_, rfl⟩ := hR
      simp_rw [height_le_iff_covBy, ENat.natCast_add, ENat.natCast_one, ENat.lt_natCast_add_one_iff]
      intro q hq hpq hq'
      obtain ⟨x, s', hxs', rfl, hxq⟩ : ∃ x s', x ∉ s' ∧ s = insert x s' ∧ x ∉ q := by
        have : ¬(s : Set R) ⊆ q := by
          rw [← span_le]
          exact fun e ↦ lt_irrefl _ ((hp.2 ⟨hq, e⟩ hpq.le).trans_lt hpq)
        obtain ⟨x, hxt, hxq⟩ := Set.not_subset.mp this
        exact ⟨x, _, fun e ↦ (Finset.mem_erase.mp e).1 rfl, (Finset.insert_erase hxt).symm, hxq⟩
      have : maximalIdeal R ≤ (q ⊔ span {x}).radical := by
        rw [radical_eq_sInf, le_sInf_iff]
        exact fun J ⟨hJ, hJ'⟩ ↦ by_contra fun h ↦ hq' J hJ' ((SetLike.lt_iff_le_and_exists.mpr
          ⟨le_sup_left, x, mem_sup_right (mem_span_singleton_self _), hxq⟩).trans_le hJ)
          ((le_maximalIdeal hJ'.ne_top).lt_of_not_ge h)
      have h : (s' : Set R) ⊆ (q ⊔ span {x}).radical := by
        have := hp.le.trans this
        rw [span_le, Finset.coe_insert, Set.insert_subset_iff] at this
        exact this.2
      obtain ⟨t, ht, hspan⟩ := exists_subset_radical_span_sup_of_subset_radical_sup _ _ _ h
      let t := Finset.univ.image t
      suffices hq : q ∈ (span t).minimalPrimes from
        have tcard : t.card ≤ n := Nat.le_of_lt_succ ((Finset.card_image_le.trans_lt <| by
          simpa using Finset.card_lt_card (Finset.ssubset_insert hxs')).trans_le hn)
        (H _ (tcard.trans_lt n.lt_succ_self) q t hq rfl).trans (by norm_cast)
      rw [Finset.coe_insert] at hp
      convert! mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert hpq _ _ hp _ ht ?_
      · simp [t]
      refine hspan.trans <| radical_mono ?_
      rw [← Set.union_singleton, span_union]

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ ¬(IsLocalRing.maximalIdeal R).height = ⊤

Tactic:
exact ((IsLocalRing.maximalIdeal R).finiteHeight_iff.mp
      (IsLocalRing.maximalIdeal R).finiteHeight_of_isNoetherianRing).resolve_left
        Ideal.IsPrime.ne_top'

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
⊢ supportDim R M ≤ supportDim R (QuotSMulTop x M) + 1

Tactic:
nontriviality M

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
a✝ : Nontrivial M
⊢ supportDim R M ≤ supportDim R (QuotSMulTop x M) + 1