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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • (hasseDeriv R (k + l)) f).coeff n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
⊢ (hasseDeriv R k) ((hasseDeriv R l) f) = (k + l).choose k • (hasseDeriv R (k + l)) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : V⸨X⸩
⊢ (derivative R) f = (hasseDeriv R 1) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : ¬IsLocalRing R
⊢ ∃ K₁ K₂ x x_1 f, Function.Surjective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
⊢ (⇑(derivative R))^[k] f = k.factorial • (hasseDeriv R k) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((⇑(derivative R))^[k] f).coeff n = (descPochhammer ℤ k).smeval (n + ↑k) • f.coeff (n + ↑k)

Tactic:
derivative_iterate,

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
n : ℤ
⊢ (k.factorial • (hasseDeriv R k) f).coeff n = (descPochhammer ℤ k).smeval (n + ↑k) • f.coeff (n + ↑k)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((⇑(derivative R))^[k] f).coeff n = (descPochhammer ℤ k).smeval (n + ↑k) • f.coeff (n + ↑k)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R⟦X⟧
n : ℕ
⊢ ((ofPowerSeries ℤ R) x).coeff ↑n = (PowerSeries.coeff n) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x.powerSeriesPart = 0 ↔ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ (single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
⊢ Function.Surjective ⇑(stabilizerHom Q P G)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ (ofPowerSeries ℤ R) x.powerSeriesPart = (single (-order x)) 1 * x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⸨X⸩
hn : ↑n = order f
⊢ (ofPowerSeries ℤ R) (PowerSeries.X ^ n * f.powerSeriesPart) = f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ∀ (y : ↥(Submonoid.powers PowerSeries.X)), IsUnit ((algebraMap R⟦X⟧ R⸨X⸩) ↑y)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
⊢ ∃ x, z * (algebraMap R⟦X⟧ R⸨X⸩) ↑x.2 = (algebraMap R⟦X⟧ R⸨X⸩) x.1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R⟦X⟧
⊢ (algebraMap R⟦X⟧ R⸨X⸩) x = (algebraMap R⟦X⟧ R⸨X⸩) y → ∃ c, ↑c * x = ↑c * y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
i : ℤ
⊢ ((ofPowerSeries ℤ R) f).coeff i = if i < 0 then 0 else (coeff i.natAbs) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
S : Type u_3
inst✝¹ : Semiring S
inst✝ : Module R S
r : R
x : S⟦X⟧
⊢ (ofPowerSeries ℤ S) (r • x) = r • (ofPowerSeries ℤ S) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
F : Type u
inst✝ : Field F
p q : F[X]
f g : F⟮X⟯
⊢ FaithfulSMul F[X] F⸨X⸩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: F : Type u
inst✝ : Field F
P : F[X]
⊢ (ofPowerSeries ℤ F) ↑P = (algebraMap F⟮X⟯ F⸨X⸩) ↑P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ (algebraMap F⟮X⟯ F⸨X⸩) X = (single 1) 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
n : ℕ
⊢ (single ↑n) 1 = (single 1) 1 ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: F : Type u
inst✝ : Field F
n : ℤ
⊢ (single n) 1 = (single 1) 1 ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: F : Type u
inst✝ : Field F
p q : F[X]
⊢ (algebraMap F⟮X⟯ F⸨X⸩) ((algebraMap F[X] F⟮X⟯) p / (algebraMap F[X] F⟮X⟯) q) =
    (algebraMap F[X] F⸨X⸩) p / (algebraMap F[X] F⸨X⸩) q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : Field K
⊢ Ideal.span {X} ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ ↑P ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Subring

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Injective ⇑f
h : ∀ a ∈ R⁰, IsUnit a
⊢ IsLocalRing R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
⊢ Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ ↑P ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K[X]
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ (idealX K).intValuation X = exp (-1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K⟮X⟯
f g : K[X]
h : g ≠ 0
⊢ ↑g ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K⟮X⟯
⊢ (polynomialValuationX K) P = (valuation K⸨X⸩ (PowerSeries.idealX K)) ((algebraMap K⟮X⟯ K⸨X⸩) P)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⟮X⟯
⊢ Valued.v ((algebraMap K⟮X⟯ K⸨X⸩) f) = Valued.v f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
s : ℕ
⊢ Valued.v ((ofPowerSeries ℤ K) PowerSeries.X ^ s) = exp (-↑s)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
s : ℤ
⊢ Valued.v ((single s) 1) = exp (-s)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((ofPowerSeries ℤ K) f) ≤ exp (-↑d)
⊢ n < d → (PowerSeries.coeff n) f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((ofPowerSeries ℤ K) f) ≤ exp (-↑d)
⊢ n < d → (PowerSeries.coeff n) f = 0

Tactic:
by
  intro hnd
  apply (PowerSeries.X_pow_dvd_iff).mp _ n hnd
  rwa [← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap,
    intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d, PowerSeries.idealX,
    Ideal.span_singleton_pow, Ideal.span_singleton_dvd_span_singleton_iff_dvd] at H

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
d : ℕ
f : K⟦X⟧
⊢ Valued.v ((ofPowerSeries ℤ K) f) ≤ exp (-↑d) ↔ ∀ n < d, (PowerSeries.coeff n) f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
⊢ 0 ≤ D + ↑s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
a : R × S
a_in : a ∈ f.pullback g
⊢ IsUnit ⟨a, a_in⟩ ↔ IsUnit a.1 ∧ IsUnit a.2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
h : Function.Surjective ⇑g
r : R
⊢ ∃ a, (f.pullbackFst g) a = r

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
h : Function.Surjective ⇑f
s : S
⊢ ∃ a, (f.pullbackSnd g) a = s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
d : ℕ
hd : D + ↑s = ↑d
⊢ m < ?m.152

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
s : S
hs : s ∈ ker g
⊢ (0, s) ∈ f.pullback g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
s : S
hs : s ∈ ker g
⊢ ⟨(0, s), ⋯⟩ ∈ ker (f.pullbackFst g)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
⊢ Ideal.map (f.pullbackSnd g) (ker (f.pullbackFst g)) = ker g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst✝³ : (i : ι) → CommSemiring (R i)
inst✝² : (i : ι) → CommSemiring (S i)
inst✝¹ : (i : ι) → Algebra (R i) (S i)
M : (i : ι) → Submonoid (R i)
inst✝ : ∀ (i : ι), IsLocalization (M i) (S i)
z : (i : ι) → S i
⊢ ∃ x, z * (algebraMap ((i : ι) → R i) ((i : ι) → S i)) ↑x.2 = (algebraMap ((i : ι) → R i) ((i : ι) → S i)) x.1

Tactic:
choose rm h using fun i ↦ surj (M := M i) (z i)

Goal state after:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst✝³ : (i : ι) → CommSemiring (R i)
inst✝² : (i : ι) → CommSemiring (S i)
inst✝¹ : (i : ι) → Algebra (R i) (S i)
M : (i : ι) → Submonoid (R i)
inst✝ : ∀ (i : ι), IsLocalization (M i) (S i)
z : (i : ι) → S i
rm : (i : ι) → R i × ↥(M i)
h : ∀ (i : ι), z i * (algebraMap (R i) (S i)) ↑(rm i).2 = (algebraMap (R i) (S i)) (rm i).1
⊢ ∃ x, z * (algebraMap ((i : ι) → R i) ((i : ι) → S i)) ↑x.2 = (algebraMap ((i : ι) → R i) ((i : ι) → S i)) x.1
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst✝³ : (i : ι) → CommSemiring (R i)
inst✝² : (i : ι) → CommSemiring (S i)
inst✝¹ : (i : ι) → Algebra (R i) (S i)
M : (i : ι) → Submonoid (R i)
inst✝ : ∀ (i : ι), IsLocalization (M i) (S i)
z : (i : ι) → S i
⊢ ∃ x, z * (algebraMap ((i : ι) → R i) ((i : ι) → S i)) ↑x.2 = (algebraMap ((i : ι) → R i) ((i : ι) → S i)) x.1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst✝³ : (i : ι) → CommSemiring (R i)
inst✝² : (i : ι) → CommSemiring (S i)
inst✝¹ : (i : ι) → Algebra (R i) (S i)
M : (i : ι) → Submonoid (R i)
inst✝ : ∀ (i : ι), IsLocalization (M i) (S i)
x y : (i : ι) → R i
eq : (algebraMap ((i : ι) → R i) ((i : ι) → S i)) x = (algebraMap ((i : ι) → R i) ((i : ι) → S i)) y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
hn : n ∈ Submonoid.pi Set.univ fun i ↦ Submonoid.map (Pi.evalRingHom R i) M
⊢ ∃ m ∈ M, n ∣ m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst✝⁵ : (i : ι) → CommSemiring (R i)
inst✝⁴ : (i : ι) → CommSemiring (S i)
inst✝³ : (i : ι) → Algebra (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst✝² : ∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)
inst✝¹ : ∀ (i : ι), Ring.KrullDimLE 0 (R i)
inst✝ : ∀ (i : ι), IsLocalRing (R i)
i : ι
h₀ : 0 ∉ Submonoid.map (Pi.evalRingHom R i) M
⊢ ?m.103 ≤ IsUnit.submonoid (R i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst✝⁵ : (i : ι) → CommSemiring (R i)
inst✝⁴ : (i : ι) → CommSemiring (S i)
inst✝³ : (i : ι) → Algebra (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst✝² : ∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)
inst✝¹ : ∀ (i : ι), Ring.KrullDimLE 0 (R i)
inst✝ : ∀ (i : ι), IsLocalRing (R i)
⊢ Surjective ⇑(RingHom.pi fun i ↦ (algebraMap (R i) (S i)).comp (Pi.evalRingHom R i))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
⊢ 0 ≤ n - ↑s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Rat

Goal state before:
pp: q : ℚ
⊢ IsLocalization.IsInteger ℤ q ↔ q ∈ Set.range Int.cast

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Rat

Goal state before:
pp: q : ℚ
⊢ ↑q.den ∈ nonZeroDivisors ℤ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Rat

Goal state before:
pp: q : ℚ
⊢ IsRelPrime q.num ↑⟨↑q.den, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
⊢ 0 ≤ D - ↑s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Rat

Goal state before:
pp: q : ℚ
⊢ IsLocalization.mk' ℚ q.num ⟨↑q.den, ⋯⟩ = q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Rat

Goal state before:
pp: q : ℚ
⊢ (↑(IsFractionRing.den ℤ q)).natAbs = q.den

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝⁶ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝³ : ∀ (i : ι), Ring.KrullDimLE 0 (R i)
inst✝² : ∀ (i : ι), IsLocalRing (R i)
inst✝¹ : IsLocalization M S'
inst✝ : Finite ι
⊢ Surjective ⇑(algebraMap ((i : ι) → R i) S')

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
d : ℕ
hd : D - ↑s = ↑d
⊢ m < ?m.299

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
⊢ n < D → f.coeff n = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: Rₚ : Type u_3
inst✝⁵ : CommRing Rₚ
inst✝⁴ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra Rₚ Sₚ
Q : Ideal Sₚ
inst✝¹ : Q.IsMaximal
inst✝ : Algebra.IsIntegral Rₚ Sₚ
⊢ Q ∈ (maximalIdeal Rₚ).primesOver Sₚ

Tactic:
by

Goal state after:
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ₚ
T : Type u_5
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra Rₚ T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsScalarTower R Rₚ T
Q : Ideal T
inst✝ : Q.LiesOver (maximalIdeal Rₚ)
⊢ Q.LiesOver p

Tactic:
by

Goal state after:
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ₚ
T : Type u_5
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra Rₚ T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsScalarTower R Rₚ T
Q : Ideal T
inst✝ : Q.LiesOver (maximalIdeal Rₚ)
⊢ (comap (algebraMap S T) Q).LiesOver p

Tactic:
by

Goal state after:
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ₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
⊢ (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)

Tactic:
by

Goal state after:
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
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs : (Ideal.Quotient.mk P) s' = ((Ideal.Quotient.mk P) ↑s)⁻¹
h₀ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : ↑s ∉ P
⊢ (algebraMap S Sₚ) ↑s ∉ Ideal.map (algebraMap S Sₚ) P

Tactic:
by

Goal state after:
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
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P
⊢ ∃ a, (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) a = x

Tactic:
by

Goal state after:
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ₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
⊢ P = RingHom.ker (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P))

Tactic:
by

Goal state after:
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
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
⊢ (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
⊢ Valued.v f ≤ exp (-D) ↔ ∀ n < D, f.coeff n = 0

Tactic:
by

Goal state after:
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
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
h₂ : (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) ≠ 0
⊢ (equivQuotientMapOfIsMaximal p Sₚ P).symm ((Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) (mk' Sₚ x s)) =
    (Ideal.Quotient.mk P) x * ((Ideal.Quotient.mk P) ↑s)⁻¹

Tactic:
rw [RingEquiv.symm_apply_eq, ← mul_left_inj' h₂, map_mul, mul_assoc, ← map_mul,
    inv_mul_cancel₀ h₁, map_one, mul_one, equivQuotientMapOfIsMaximal_apply_mk,
    ← map_mul, mk'_spec, Quotient.mk_algebraMap, equivQuotientMapOfIsMaximal_apply_mk,
    Quotient.mk_algebraMap]

Goal state after: