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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset 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
hn : s.card ≤ n + 1
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
this : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
⊢ q < maximalIdeal R → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R) → q.height ≤ ↑n

Tactic:
hpq

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset 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
hn : s.card ≤ n + 1
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
this : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
⊢ (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R) → q.height ≤ ↑n
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
⊢ ringKrullDim R = 1

Tactic:
have : ¬ ringKrullDim R ≤ 0 := fun h ↦ by
      have : Ring.KrullDimLE 0 R := Ring.krullDimLE_iff.mpr h
      exact hn Ring.KrullDimLE.isField_of_isDomain
    suffices h : Ring.KrullDimLE 1 R by
      rw [Ring.krullDimLE_iff] at h
      exact le_antisymm h (Order.succ_le_of_lt (lt_of_not_ge this))
    refine Ring.krullDimLE_one_iff_of_noZeroDivisors.mpr fun I hI hI_prime ↦ ?_
    obtain ⟨x, hI, hx⟩ : ∃ (x : R), x ∈ I ∧ x ≠ 0 := by
      apply by_contradiction fun h ↦ (hI (le_antisymm (fun x ↦ ?_) bot_le))
      simp only [ne_eq, not_exists, not_and, not_not] at h
      exact fun hx ↦ h x hx
    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))
    have := Ideal.IsMaximal.eq_of_le (IsLocalRing.maximalIdeal.isMaximal R) hI_prime.ne_top this
    exact this ▸ (IsLocalRing.maximalIdeal.isMaximal R)

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f} ↔ Disjoint (↑(PrimeSpectrum.basicOpen f)) (Module.support R M)

Tactic:
PrimeSpectrum.basicOpen_eq_zeroLocus_compl,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f} ↔ Disjoint (PrimeSpectrum.zeroLocus {f})ᶜ (Module.support R M)
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:
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.Spectrum.Prime.LTSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h : (e ⟨closedPoint R, ⋯⟩).asIdeal.height ≤ 1
⊢ False

Tactic:
have hph : (e ⟨p₁, h₀.le⟩).1.height ≤ 0 :=
    Order.lt_one_iff_nonpos.mp (height_le_iff.mp h _ inferInstance (by simpa using h₁))

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h : (e ⟨closedPoint R, ⋯⟩).asIdeal.height ≤ 1
hph : (e ⟨p₁, ⋯⟩).asIdeal.height ≤ 0
⊢ False
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
J : Submodule R M
hJ : J ∈ s
y : Submodule R M
⊢ y ∈ s → (y.colon Set.univ).radical = (J.colon Set.univ).radical → y.IsPrimary

Tactic:
hy

Goal state after:
case refine_2.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
J : Submodule R M
hJ : J ∈ s
y : Submodule R M
hy : y ∈ s
⊢ (y.colon Set.univ).radical = (J.colon Set.univ).radical → y.IsPrimary
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.h
n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
⊢ y ∈ R → x * y = y * x

Tactic:
hy

Goal state after:
case intro.h
n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
⊢ x * y = y * x
Module: Mathlib.RingTheory.LocalProperties.FinitePresentation

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
s : Set R
hs : Ideal.span s = ⊤
Mₚ : ↑s → Type u_3
inst✝⁷ : (g : ↑s) → AddCommGroup (Mₚ g)
inst✝⁶ : (g : ↑s) → Module R (Mₚ g)
Rₚ : ↑s → Type u_4
inst✝⁵ : (g : ↑s) → CommRing (Rₚ g)
inst✝⁴ : (g : ↑s) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↑s), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↑s) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↑s), IsScalarTower R (Rₚ g) (Mₚ g)
ϕ : (g : ↑s) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↑s), IsLocalizedModule (Submonoid.powers ↑g) (ϕ g)
h : ∀ (g : ↑s), FinitePresentation (Rₚ g) (Mₚ g)
this : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
fsurj : Function.Surjective ⇑f
⊢ FinitePresentation R M

Tactic:
rw [← Module.FinitePresentation.fg_ker_iff f fsurj]

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
s : Set R
hs : Ideal.span s = ⊤
Mₚ : ↑s → Type u_3
inst✝⁷ : (g : ↑s) → AddCommGroup (Mₚ g)
inst✝⁶ : (g : ↑s) → Module R (Mₚ g)
Rₚ : ↑s → Type u_4
inst✝⁵ : (g : ↑s) → CommRing (Rₚ g)
inst✝⁴ : (g : ↑s) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↑s), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↑s) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↑s), IsScalarTower R (Rₚ g) (Mₚ g)
ϕ : (g : ↑s) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↑s), IsLocalizedModule (Submonoid.powers ↑g) (ϕ g)
h : ∀ (g : ↑s), FinitePresentation (Rₚ g) (Mₚ g)
this : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
fsurj : Function.Surjective ⇑f
⊢ f.ker.FG
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
this : Module.Free R S
e : (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) ≃ₗ[R ⧸ maximalIdeal R] S ⧸ maximalIdeal S
⊢ Module.finrank R S = Module.finrank (ResidueField R) (ResidueField S)

pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
this : Module.Free R S
⊢ ∀ (c : R ⧸ maximalIdeal R) (x : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)),
    (Ideal.quotEquivOfEq ⋯).toAddEquiv (c • x) = c • (Ideal.quotEquivOfEq ⋯).toAddEquiv x

Tactic:
· rw [← finrank_quotient_map (R := R) (S := S)]
    exact e.finrank_eq

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
this : Module.Free R S
⊢ ∀ (c : R ⧸ maximalIdeal R) (x : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)),
    (Ideal.quotEquivOfEq ⋯).toAddEquiv (c • x) = c • (Ideal.quotEquivOfEq ⋯).toAddEquiv x
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
s : ℕ
⊢ exp (-(s • 1)) = exp (-↑s)

Tactic:
nsmul_one

Goal state after:
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ exp (-↑s) = exp (-↑s)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
d : ℕ
f : K⟦X⟧
this : PowerSeries.X ^ d ∣ f ↔ ∀ n < d, (PowerSeries.coeff n) f = 0
⊢ (PowerSeries.idealX K).intValuation f ≤ exp (-↑d) ↔ PowerSeries.X ^ d ∣ f

Tactic:
← Ideal.span_singleton_dvd_span_singleton_iff_dvd,

Goal state after:
K : Type u_2
inst✝ : Field K
d : ℕ
f : K⟦X⟧
this : PowerSeries.X ^ d ∣ f ↔ ∀ n < d, (PowerSeries.coeff n) f = 0
⊢ (PowerSeries.idealX K).intValuation f ≤ exp (-↑d) ↔ Ideal.span {PowerSeries.X ^ d} ∣ Ideal.span {f}
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
⊢ ∃ v ∈ uniformity K⸨X⸩, ∀ y ∈ v, (y.1.coeff d, y.2.coeff d) ∈ S

Tactic:
use {P | Valued.v (P.snd - P.fst) < ↑γ}

Goal state after:
case h
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := ⋯
⊢ {P | Valued.v (P.2 - P.1) < ↑γ} ∈ uniformity K⸨X⸩ ∧
    ∀ y ∈ {P | Valued.v (P.2 - P.1) < ↑γ}, (y.1.coeff d, y.2.coeff d) ∈ S
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
p : Ideal R
inst✝¹⁵ : p.IsPrime
Rₚ : Type u_3
inst✝¹⁴ : CommRing Rₚ
inst✝¹³ : Algebra R Rₚ
inst✝¹² : IsLocalization.AtPrime Rₚ p
inst✝¹¹ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra S Sₚ
inst✝⁸ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁷ : Algebra Rₚ Sₚ
inst✝⁶ : IsDomain R
inst✝⁵ : IsDedekindDomain S
inst✝⁴ : IsTorsionFree R S
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : p.IsMaximal
hp : p ≠ ⊥
P : ↑(p.primesOver S)
this✝ : NeZero p
this : (↑P).IsMaximal
⊢ (maximalIdeal Rₚ).inertiaDeg' ↑((primesOverEquivPrimesOver p Rₚ Sₚ hp) P) = p.inertiaDeg' ↑P

Tactic:
have : (P.1.map (algebraMap S Sₚ)).LiesOver (maximalIdeal Rₚ) := liesOver_map_of_liesOver p _ _ _

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
p : Ideal R
inst✝¹⁵ : p.IsPrime
Rₚ : Type u_3
inst✝¹⁴ : CommRing Rₚ
inst✝¹³ : Algebra R Rₚ
inst✝¹² : IsLocalization.AtPrime Rₚ p
inst✝¹¹ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra S Sₚ
inst✝⁸ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁷ : Algebra Rₚ Sₚ
inst✝⁶ : IsDomain R
inst✝⁵ : IsDedekindDomain S
inst✝⁴ : IsTorsionFree R S
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : p.IsMaximal
hp : p ≠ ⊥
P : ↑(p.primesOver S)
this✝¹ : NeZero p
this✝ : (↑P).IsMaximal
this : (Ideal.map (algebraMap S Sₚ) ↑P).LiesOver (maximalIdeal Rₚ)
⊢ (maximalIdeal Rₚ).inertiaDeg' ↑((primesOverEquivPrimesOver p Rₚ Sₚ hp) P) = p.inertiaDeg' ↑P
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d) (coeff d f)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
q : MvPolynomial n R
b : R
hb : b ∣ coeff d f
d₂ : n →₀ ℕ
hd₂ : d₂ ∈ f.support
H : d₂ ≠ d
hm : 0 ≤ d₀
hpφ : (monomial 0) b ∣ φ
hq : ψ = (monomial 0) b * q
k : n →₀ ℕ
hk : ¬k = d
⊢ b ∣ coeff k (φ * X i + ψ)

Tactic:
simp [hq, hφ, Ne.symm hk]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
F_mul : (ofPowerSeries ℤ K) f.powerSeriesPart = (single (-HahnSeries.order f)) 1 * f
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

Tactic:
rw [← hF, hs, neg_neg, ← ofPowerSeries_X_pow s, ← inv_mul_eq_iff_eq_mul₀] at F_mul

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : (ofPowerSeries ℤ K) F = (ofPowerSeries ℤ K) (PowerSeries.X ^ s) * f
hs : HahnSeries.order f = -↑s
⊢ (ofPowerSeries ℤ K) (PowerSeries.X ^ s) ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ 0 < if hi : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ then 1 else 0

Tactic:
dif_pos hkm.1

Goal state after:
case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ 0 < 1
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ (ratfuncAdicComplRingEquiv K) { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm RatFunc.X) } =
    (ofPowerSeries ℤ K) PowerSeries.X

Tactic:
rw [ratfuncAdicComplRingEquiv_apply, PowerSeries.coe_X, ← RatFunc.coe_X, ← LaurentSeries_coe,
    ← compare_coe]

Goal state after:
K : Type u_2
inst✝ : Field K
⊢ ratfuncAdicComplPkg.compare (LaurentSeriesPkg K)
      { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm RatFunc.X) }.toCompletion =
    AbstractCompletion.compare ?pkg (LaurentSeriesPkg K)
      (AbstractCompletion.coe ?pkg (WithVal.toVal (polynomialValuationX K) RatFunc.X))

case pkg
K : Type u_2
inst✝ : Field K
⊢ AbstractCompletion.{?u.24, u_2} (WithVal (polynomialValuationX K))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
hS : ∃ i, i ≠ 0 ∧ Set.Iio i ⊆ S
⊢ ⇑Valued.v ⁻¹' S ∈
    Filter.comap (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) (𝓝 a)

Tactic:
obtain ⟨γ, γ_ne_zero, γ_le⟩ := hS

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ ⇑Valued.v ⁻¹' S ∈
    Filter.comap (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) (𝓝 a)
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
⊢ (coeff n) ((expand p hp) ↑φ) = (coeff n) ↑((MvPolynomial.expand p) φ)

Tactic:
simp only [MvPolynomial.coeff_coe]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
⊢ (coeff n) ((expand p hp) ↑φ) = MvPolynomial.coeff n ((MvPolynomial.expand p) φ)
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsPrecomplete I R
x : Perfection (R ⧸ I) p
y : R
n : ℕ
h : (Ideal.Quotient.mk I) y = (coeff (R ⧸ I) p n) x
this : x.teichmullerAux (n + 1) ≡ ⋯.choose [SMOD I ^ (n + 1)]
⊢ x.teichmullerFun ≡ y ^ p ^ n [SMOD I ^ (n + 1)]

Tactic:
exact this.symm.trans <| .pow_pow_add_one (I.natCast_mem_of_charP_quotient p) (m := n) <| by
    simp [SModEq.idealQuotientMk, h]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ (x * y).ghostFun = x.ghostFun * y.ghostFun

Tactic:
ghost_fun_tac X 0 * X 1, ![x.coeff, y.coeff]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
i : ℤ
⊢ i.castDef.ghostFun = ↑i

Tactic:
cases i <;> simp [*, Int.castDef, ghostFun_natCast, ghostFun_neg]

Goal state after:
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
rw [Finset.mem_range, Nat.lt_succ_iff] at hk

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k))
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C (↑p ^ n * ⅟↑p ^ n) * X n ^ p +
        C (↑p * ↑p ^ n * ⅟↑p ^ n) * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)

Tactic:
mul_assoc (p : ℚ) ((p : ℚ) ^ n),

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C (↑p ^ n * ⅟↑p ^ n) * X n ^ p +
        C (↑p * (↑p ^ n * ⅟↑p ^ n)) * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)