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

Goal state before:
pp: case cons
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
r : R
rs₁ : List R
ih :
  ∀ (M : Type u_3) [inst : AddCommGroup M] [inst_1 : Module R M],
    IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsWeaklyRegular M (r :: rs₁ ++ rs₂) ↔
    IsWeaklyRegular M (r :: rs₁) ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₁) • ⊤) rs₂

Tactic:
let e := quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
    rw [List.cons_append, isWeaklyRegular_cons_iff, isWeaklyRegular_cons_iff,
      ih, ← and_assoc, ← e.isWeaklyRegular_congr rs₂]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.IsSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
⊢ hI.dpow n a - hI.dpow n b ∈ J

Tactic:
have hab' : a - b ∈ I := I.sub_mem ha hb

Goal state after:
case refine_1
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.IsSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ hI.dpow n a - hI.dpow n b ∈ J
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ Coe.ringHom ⟨dpow' p n ↑x, ⋯⟩ = (RatAlgebra.dividedPowers ⊤).dpow n (Coe.ringHom x)

Tactic:
simp [dpow', inverse_eq_inv', Coe.ringHom_apply, RatAlgebra.dpow_apply,
        Submodule.mem_top, ↓reduceIte]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∈ S
⊢ ⊤.carrier ⊓ ⨅ (_ : J ∈ S), J.carrier = I ⊓ ↑(⨅ (_ : J ∈ S), ⟨J.carrier, ⋯⟩)

Tactic:
ciInf_pos hJ,

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∈ S
⊢ ⊤.carrier ⊓ J.carrier = I ⊓ ↑(⨅ (_ : J ∈ S), ⟨J.carrier, ⋯⟩)
Module: Mathlib.RingTheory.Flat.LocallyFree

Goal state before:
pp: case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Nontrivial R
Rₚ : Type u_1 := Localization.AtPrime p
n : ℕ := rankAtStalk M { asIdeal := p, isPrime := ⋯ }
f : (Fin n →₀ R) →ₗ[R] Fin n →₀ Rₚ := Finsupp.mapRange.linearMap (Algebra.linearMap R Rₚ)
g : M →ₗ[R] LocalizedModule.AtPrime p M := mkLinearMap p.primeCompl M
φ : (Fin n →₀ R) →ₗ[R] M
hφps : Function.Surjective ⇑((IsLocalizedModule.map p.primeCompl f g) φ)
a : R
hap : a ∉ p
hφas : Function.Surjective ⇑((map (Submonoid.powers a)) φ)
this : Free (Localization.Away a) (LocalizedModule.Away a (Fin n →₀ R))
⊢ ∃ a ∉ p, Free (Localization.Away a) (LocalizedModule.Away a M)

Tactic:
let φₐ : LocalizedModule.Away a (Fin n →₀ R) →ₗ[Localization.Away a] LocalizedModule.Away a M :=
      LocalizedModule.map (Submonoid.powers a) φ

Goal state after:
case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Nontrivial R
Rₚ : Type u_1 := Localization.AtPrime p
n : ℕ := rankAtStalk M { asIdeal := p, isPrime := ⋯ }
f : (Fin n →₀ R) →ₗ[R] Fin n →₀ Rₚ := Finsupp.mapRange.linearMap (Algebra.linearMap R Rₚ)
g : M →ₗ[R] LocalizedModule.AtPrime p M := mkLinearMap p.primeCompl M
φ : (Fin n →₀ R) →ₗ[R] M
hφps : Function.Surjective ⇑((IsLocalizedModule.map p.primeCompl f g) φ)
a : R
hap : a ∉ p
hφas : Function.Surjective ⇑((map (Submonoid.powers a)) φ)
this : Free (Localization.Away a) (LocalizedModule.Away a (Fin n →₀ R))
φₐ : LocalizedModule.Away a (Fin n →₀ R) →ₗ[Localization.Away a] LocalizedModule.Away a M :=
  (map (Submonoid.powers a)) φ
⊢ ∃ a ∉ p, Free (Localization.Away a) (LocalizedModule.Away a M)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A✝ : Type u_1
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ hI' : DividedPowers I✝
A : Type u_2
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x✝¹ : ℕ
hn : x✝¹ ≠ 0
a : A
x✝ : a ∈ J ⊓ I
haJ : a ∈ ↑J
haI : a ∈ ↑I
ha0 : φ.toRingHom a = 0
⊢ hJ.dpow x✝¹ (φ.toRingHom a) = 0

Tactic:
ha0,

Goal state after:
A✝ : Type u_1
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ hI' : DividedPowers I✝
A : Type u_2
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x✝¹ : ℕ
hn : x✝¹ ≠ 0
a : A
x✝ : a ∈ J ⊓ I
haJ : a ∈ ↑J
haI : a ∈ ↑I
ha0 : φ.toRingHom a = 0
⊢ hJ.dpow x✝¹ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Binomial

Goal state before:
pp: case succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose d) = ↑(Ring.choose (-(↑d + 1)) n)

Tactic:
Ring.choose_neg,

Goal state after:
case succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose d) = ↑((↑n).negOnePow • Ring.choose (↑d + 1 + ↑n - 1) n)
Module: Mathlib.RingTheory.PowerSeries.Binomial

Goal state before:
pp: case succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose n) = ↑(↑(↑n).negOnePow • Ring.choose (↑(d + n)) n)

Tactic:
Ring.choose_natCast

Goal state after:
case succ
A : Type u_2
inst✝ : CommRing A
n d : ℕ
⊢ ↑↑(↑n).negOnePow * ↑((d + n).choose n) = ↑(↑(↑n).negOnePow • ↑((d + n).choose n))
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc : (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ n).coeff g ≠ 0
⊢ ∃ x_1 ∈ Function.support fun a_1 ↦ (((powerSeriesFamily x a).mul (powerSeriesFamily x b)) a_1).coeff g,
    x_1.1 + x_1.2 = n

Tactic:
use c

Goal state after:
case h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc : (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ n).coeff g ≠ 0
⊢ (c ∈ Function.support fun a_1 ↦ (((powerSeriesFamily x a).mul (powerSeriesFamily x b)) a_1).coeff g) ∧ c.1 + c.2 = n
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
hz : n = 0
this : g = 0 ∧ (PowerSeries.constantCoeff a * PowerSeries.constantCoeff b) • 1 ≠ 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))

Tactic:
simp only [coe_image, Set.mem_image]

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
hz : n = 0
this : g = 0 ∧ (PowerSeries.constantCoeff a * PowerSeries.constantCoeff b) • 1 ≠ 0
⊢ ∃ x_1 ∈ ↑(Set.Finite.toFinset ⋯), x_1.1 + x_1.2 = n
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
t : Finset α
h : {a | (s a).coeff g ≠ 0} ⊆ ↑t
⊢ s.hsum.coeff g = ∑ i ∈ t, (s i).coeff g

Tactic:
simp only [coeff_hsum, finsum_eq_sum _ (s.finite_co_support _)]

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
t : Finset α
h : {a | (s a).coeff g ≠ 0} ⊆ ↑t
⊢ ∑ i ∈ Set.Finite.toFinset ⋯, (s i).coeff g = ∑ i ∈ t, (s i).coeff g
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⟦Γ⟧
⊢ (powerSeriesFamily x 1).hsum = 1

Tactic:
by
    simp only [hsum, smulFamily_toFun, coeff_one, powers_toFun, ite_smul, one_smul, zero_smul]
    ext g
    simp only
    rw [finsum_eq_single _ (0 : ℕ) (fun n hn => by simp [hn])]
    simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g g' : Γ
hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g'
hg' : g' ∈ s.hsum.support
⊢ g ≤ g'

Tactic:
rw [mem_support, coeff_hsum_eq_sum] at hg'
  obtain ⟨i, _, hi⟩ := Finset.exists_ne_zero_of_sum_ne_zero hg'
  exact hg i g' hi

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ((powerSeriesFamily x f).coeff 0) 0 = constantCoeff f

pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ∀ (x_1 : ℕ), x_1 ≠ 0 → ((powerSeriesFamily x f).coeff 0) x_1 = 0

Tactic:
← PowerSeries.coeff_zero_eq_constantCoeff_apply

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ((powerSeriesFamily x f).coeff 0) 0 = (coeff 0) f

Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ∀ (x_1 : ℕ), x_1 ≠ 0 → ((powerSeriesFamily x f).coeff 0) x_1 = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ PowerSeries.subst F.zeroX F.zeroX = subst ![0, subst ![0, PowerSeries.X] F.toPowerSeries] F.toPowerSeries

Tactic:
by
      have : PowerSeries.HasSubst (subst ![0, PowerSeries.X (R := R)] F.toPowerSeries) := by
        refine PowerSeries.HasSubst.of_constantCoeff_zero' ?_
        rw [PowerSeries.constantCoeff, PowerSeries.X, constantCoeff_subst_eq_zero HasSubst.zero_X
          (by simp) F.zero_constantCoeff]
      rw [PowerSeries.subst, subst_comp_subst_apply _ this.const]
      · congr! 2 with d
        fin_cases d
        · simp [← PowerSeries.subst_def, ← PowerSeries.coe_substAlgHom this]
        · simp [← PowerSeries.subst_def, PowerSeries.subst_X this]
      · exact HasSubst.zero_X

Goal state after:
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 α
f : α ↪ β
g : Γ
⊢ {a | (if h : a ∈ Set.range ⇑f then s (Classical.choose h) else 0).coeff g ≠ 0} ⊆
    ⇑f '' Function.support fun a ↦ (s a).coeff g

Tactic:
intro b 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 α
f : α ↪ β
g : Γ
b : β
h : b ∈ {a | (if h : a ∈ Set.range ⇑f then s (Classical.choose h) else 0).coeff g ≠ 0}
⊢ b ∈ ⇑f '' Function.support fun a ↦ (s a).coeff g
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
x✝ :
  ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
f : R[X]
hf : f.Monic
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, f.IsRoot 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₁ : f.IsRoot a
ha₂ : (residue R) a = (residue R) a₀
⊢ a - a₀ ∈ maximalIdeal R

Tactic:
← Ideal.Quotient.eq_zero_iff_mem

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
x✝ :
  ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
f : R[X]
hf : f.Monic
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, f.IsRoot 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₁ : f.IsRoot a
ha₂ : (residue R) a = (residue R) a₀
⊢ (Ideal.Quotient.mk (maximalIdeal R)) (a - a₀) = 0
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal R
h₂ : Polynomial.eval a₀ (derivative f) ∈ maximalIdeal R
⊢ ¬IsUnit ((Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f)))

Tactic:
← Ideal.Quotient.eq_zero_iff_mem

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal R
h₂ : (Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f)) = 0
⊢ ¬IsUnit ((Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f)))
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')⁻¹ʳ
n : ℕ
⊢ c n ≡ a₀ [SMOD I]

Tactic:
induction n with
        | zero => rfl
        | succ n ih => ?_

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')⁻¹ʳ
n : ℕ
ih : c n ≡ a₀ [SMOD I]
⊢ c (n + 1) ≡ a₀ [SMOD I]
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsNoetherianRing R
h : ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p
I : Ideal R
hIn : I ≠ ⊥
a✝ : I.IsPrime
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : Ideal R
hpmin : p ∈ (Ideal.span {x}).minimalPrimes
hpl : p ≤ I
this : p.IsPrime
hpn : p ≠ ⊥
hpp : Submodule.IsPrincipal p
⊢ ∃ x ∈ I, Prime x

Tactic:
exact ⟨hpp.generator p, hpl (hpp.generator_mem p), hpp.prime_generator_of_isPrime p hpn⟩

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

Goal state before:
pp: case hIN.refine_2
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 : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : comap f (map f q ^ n) ⊔ I = comap f (map f q ^ n.succ) ⊔ I
y : R
hy : y ∈ comap f (map f q ^ n.succ)
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx : f y + f (z * Submodule.IsPrincipal.generator I) ∈ map (algebraMap R (Localization.AtPrime q)) q ^ n
⊢ z ∈
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n)

Tactic:
f.map_mul,

Goal state after:
case hIN.refine_2
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 : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : comap f (map f q ^ n) ⊔ I = comap f (map f q ^ n.succ) ⊔ I
y : R
hy : y ∈ comap f (map f q ^ n.succ)
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx : f y + f z * f (Submodule.IsPrincipal.generator I) ∈ map (algebraMap R (Localization.AtPrime q)) q ^ n
⊢ z ∈
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
⊢ (span {x}).height ≤ 1

Tactic:
obtain ⟨p, hp⟩ := (span {x}).nonempty_minimalPrimes (by simpa)
  refine le_trans (height_mono hp.1.2) ?_
  exact Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes (span {x}) _ hp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝ : p.IsPrime
this : (map f p).IsPrime
h : (map f p).height ≤ 1
e : map f p ≤ map f q
⊢ p ≤ q

Tactic:
simpa only [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot, f, mk_ker,
        sup_eq_left.mpr hI'q, sup_eq_left.mpr hI'p] using comap_mono (f := f) e

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
⊢ x ∈ RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal))

Tactic:
rw [RingHom.mem_ker]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
⊢ (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal)) x = 0
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
a✝ : IsOpen s
⊢ IsOpen ((fun a ↦ ↑a) ⁻¹' s)

Tactic:
← (Set.biUnion_preimage_singleton QuotientGroup.mk s)

Goal state after:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
a✝ : IsOpen s
⊢ IsOpen (⋃ y ∈ s, QuotientGroup.mk ⁻¹' {y})
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
w✝ : IsLocalRing R
this✝ : (maximalIdeal R).IsPrime
q : Ideal R
hq✝ : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : maximalIdeal R ∈ (span ↑(insert x s')).minimalPrimes
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : ↑s' ⊆ ↑(q ⊔ span {x}).radical
t✝ : ↑↑s' → R
ht : Set.range t✝ ⊆ ↑q
hspan : ↑s' ⊆ ↑(span (Set.range t✝) ⊔ span {x}).radical
t : Finset R := Finset.image t✝ Finset.univ
hq : q ∈ (span ↑t).minimalPrimes
⊢ Finset.univ.card < (insert x s').card

Tactic:
simpa using Finset.card_lt_card (Finset.ssubset_insert hxs')

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ ↑I.height ≤ ↑(Cardinal.toENat (Submodule.spanRank I))

Tactic:
exact_mod_cast I.height_le_spanRank_toENat hI

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
h : p.height ≤ ↑t.card
⊢ ⋯.toFinset.card = Submodule.spanFinrank I

Tactic:
rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
h : p.height ≤ ↑t.card
⊢ (Submodule.generators I).ncard = Submodule.spanFinrank I
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case h₂
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
s : Set R
p : Ideal R
inst✝ : p.IsPrime
hrm : s ⊆ ↑p
⊢ ↑(Submodule.spanFinrank (span s)) ≤ s.encard

Tactic:
exact Submodule.spanFinrank_span_le_encard _

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

Goal state before:
pp: case h₂
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
s : Set R
hs : s ⊆ ↑p
⊢ ↑(Submodule.spanFinrank (span s)) ≤ s.encard

Tactic:
exact Submodule.spanFinrank_span_le_encard _

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

Goal state before:
pp: case h₂
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Set R
hs : s ⊆ ↑(Ring.jacobson R)
⊢ ↑(Submodule.spanFinrank (Ideal.span s)) ≤ s.encard

Tactic:
exact Submodule.spanFinrank_span_le_encard _

Goal state after: