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

Goal state before:
pp: case directed
A : Type u_1
inst✝ : Ring A
F G : IdealFilter A
I K : Ideal A
hK : K ∈ G
hIK : F.IsTorsionQuot I K
J L : Ideal A
hL : L ∈ G
hJL : F.IsTorsionQuot J L
⊢ I ⊓ J ∈ {L | ∃ K ∈ G, F.IsTorsionQuot L K}

Tactic:
exact ⟨K ⊓ L, G.inf_mem hK hL,
      (hIK.anti_right inf_le_left).inf (hJL.anti_right inf_le_right)⟩

Goal state after:
Module: Mathlib.Topology.Algebra.ClopenNhdofOne

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : g ∈ sInf {N | IsOpen ↑N ∧ ↑H ≤ N}
hg_not : g ∉ ↑H
U : Set G := (g • ↑H)ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : ↑N ⊆ U
NH : Subgroup G := ↑N.toOpenSubgroup ⊔ ↑H
hg' : g ∈ NH
y : G
hy : y ∈ ↑N.toOpenSubgroup
z : G
hz : z ∈ ↑H
hyz : y = g * z⁻¹
⊢ False

Tactic:
exact hN (hyz ▸ hy) <| mem_leftCoset g (inv_mem_iff.mpr hz)

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

Goal state before:
pp: 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
h : Ring.KrullDimLE 1 R
⊢ ringKrullDim R = 1

Tactic:
rw [Ring.krullDimLE_iff] at h
      exact le_antisymm h (Order.succ_le_of_lt (lt_of_not_ge this))

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
⊢ supportDim R M = ringKrullDim (R ⧸ annihilator R M)

Tactic:
simp only [supportDim]
  rw [support_eq_zeroLocus, ringKrullDim_quotient]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsLocalRing R
dim : Module.supportDim R N = 0
⊢ Nontrivial N

Tactic:
by simp [← Module.supportDim_ne_bot_iff_nontrivial R, dim]

Goal state after:
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
this : span ↑(insert x s') ≤ (q ⊔ span {x}).radical
⊢ ↑s' ⊆ ↑(q ⊔ span {x}).radical

Tactic:
rw [span_le, Finset.coe_insert, Set.insert_subset_iff] at this

Goal state after:
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
this : x ∈ ↑(q ⊔ span {x}).radical ∧ ↑s' ⊆ ↑(q ⊔ span {x}).radical
⊢ ↑s' ⊆ ↑(q ⊔ span {x}).radical
Module: Mathlib.RingTheory.KrullDimension.Module

Goal state before:
pp: case a
R : Type u_1
inst✝³ : CommRing R
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsLocalRing R
dim : Module.supportDim R N = 0
x✝ : Nontrivial N := ⋯
⊢ Module.support R N ⊆ {{ asIdeal := maximalIdeal R, isPrime := ⋯ }}

Tactic:
intro p

Goal state after:
case a
R : Type u_1
inst✝³ : CommRing R
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsLocalRing R
dim : Module.supportDim R N = 0
x✝ : Nontrivial N :=
  of_eq_true
    (Eq.trans
      ((fun M [AddCommGroup M] [Module R M] ↦ Eq.symm (propext (Module.supportDim_ne_bot_iff_nontrivial R M))) N)
      (Eq.trans (congrFun' (congrArg Ne dim) ⊥)
        (Eq.trans (congrArg Not WithBot.zero_ne_bot._simp_1) not_false_eq_true)))
p : PrimeSpectrum R
⊢ p ∈ Module.support R N → p ∈ {{ asIdeal := maximalIdeal R, isPrime := ⋯ }}
Module: Mathlib.RingTheory.KrullDimension.PID

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
⊢ Ring.KrullDimLE 1 R

Tactic:
refine Ring.krullDimLE_one_iff.2 fun I hI ↦ or_iff_not_imp_left.2 fun hI' ↦ ?_

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
hI' : I ∉ minimalPrimes R
⊢ I.IsMaximal
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this✝³ : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
this✝² : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (algebraMap R[X] Rₚ[X]) P
disj : Disjoint ↑(Submonoid.map C p.primeCompl) ↑P
eq : under R[X] (Ideal.map (algebraMap R[X] Rₚ[X]) P) = P
this✝¹ : (under R[X] P').IsMaximal
this✝ : P'.IsMaximal
this : P'.LiesOver p'
⊢ Disjoint ↑p.primeCompl ↑p

Tactic:
exact Disjoint.symm <| Set.disjoint_left.mpr fun _ a b ↦ b a

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
a✝¹ : Nontrivial M
a✝ : Nontrivial (QuotSMulTop x M)
this✝ : Nonempty ↑(support R M)
this : Nonempty ↑(support R (QuotSMulTop x M))
⊢ ∀ (i : LTSeries ↑(support R (QuotSMulTop x M))), ↑i.length + 1 ≤ ⨆ p, ↑p.length

Tactic:
intro p

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
a✝¹ : Nontrivial M
a✝ : Nontrivial (QuotSMulTop x M)
this✝ : Nonempty ↑(support R M)
this : Nonempty ↑(support R (QuotSMulTop x M))
p : LTSeries ↑(support R (QuotSMulTop x M))
⊢ ↑p.length + 1 ≤ ⨆ p, ↑p.length
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
⊢ I.minimalPrimes ⊆ radical '' ↑t

Tactic:
intro p

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
⊢ p ∈ I.minimalPrimes → p ∈ radical '' ↑t
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N

Tactic:
have hf : Monotone f := by
    intro n m hnm x hx
    simpa [hnm, smul_smul, ← pow_add] using! N.smul_mem (a ^ (m - n)) hx

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case bot
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule i.asIdeal.primeCompl ↑M)
⊢ ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (LocalizedModule P.primeCompl ↑M)

Tactic:
intro p

Goal state after:
case bot
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule i.asIdeal.primeCompl ↑M)
p : Ideal R
⊢ ∀ [inst : p.IsMaximal], Subsingleton (LocalizedModule p.primeCompl ↑M)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case bot
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ m, injectiveDimension (M.localizedModule m.asIdeal.primeCompl) ≤ ↑n
h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule i.asIdeal.primeCompl ↑M)
⊢ ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (LocalizedModule P.primeCompl ↑M)

Tactic:
intro p

Goal state after:
case bot
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ m, injectiveDimension (M.localizedModule m.asIdeal.primeCompl) ≤ ↑n
h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule i.asIdeal.primeCompl ↑M)
p : Ideal R
⊢ ∀ [inst : p.IsMaximal], Subsingleton (LocalizedModule p.primeCompl ↑M)
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case bot
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule i.asIdeal.primeCompl ↑M)
⊢ ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (LocalizedModule P.primeCompl ↑M)

Tactic:
intro p

Goal state after:
case bot
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule i.asIdeal.primeCompl ↑M)
p : Ideal R
⊢ ∀ [inst : p.IsMaximal], Subsingleton (LocalizedModule p.primeCompl ↑M)
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case bot
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule i.asIdeal.primeCompl ↑M)
⊢ ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (LocalizedModule P.primeCompl ↑M)

Tactic:
intro p

Goal state after:
case bot
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule i.asIdeal.primeCompl ↑M)
p : Ideal R
⊢ ∀ [inst : p.IsMaximal], Subsingleton (LocalizedModule p.primeCompl ↑M)
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:
ext n
  simp [hasseDeriv_comp_coeff k l f n]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
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
⊢ f.coeff (↑s + ↑m) = 0

Tactic:
← neg_neg (s : ℤ),

Goal state after:
case neg
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
⊢ f.coeff (- -↑s + ↑m) = 0
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_3
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
hp : IsWeightedHomogeneous w ((pderiv i) p) n'
hq : IsWeightedHomogeneous w ((pderiv i) q) n'
⊢ IsWeightedHomogeneous w ((pderiv i) (p + q)) n'

Tactic:
map_add

Goal state after:
case refine_3
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
hp : IsWeightedHomogeneous w ((pderiv i) p) n'
hq : IsWeightedHomogeneous w ((pderiv i) q) n'
⊢ IsWeightedHomogeneous w ((pderiv i) p + (pderiv i) q) n'
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.IsMaximal
inst✝¹ : P.IsMaximal
inst✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
x : Rₚ ⧸ maximalIdeal Rₚ
⊢ (algebraMap (R ⧸ p) (S ⧸ P)) ((equivQuotMaximalIdeal p Rₚ).symm x) =
    (equivQuotientMapOfIsMaximal p Sₚ P).symm
      ((algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) x)

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
  obtain ⟨x, s, rfl⟩ := mk'_surjective p.primeCompl x
  simp [equivQuotMaximalIdeal_symm_apply_mk, map_mul, Quotient.algebraMap_mk_of_liesOver,
    IsLocalization.algebraMap_mk' S Rₚ Sₚ]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_2
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∃ F, (ofPowerSeries ℤ K) F = f) → ∀ n < 0, f.coeff n = 0

Tactic:
rintro ⟨F, rfl⟩ _ _

Goal state after:
case refine_2
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ ((ofPowerSeries ℤ K) F).coeff n✝ = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.refine_1
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))) ⋯
x : K⸨X⸩
hx : Valued.v x = ↑γ
this : Valued.v.restrict x ≠ 0
⊢ {P |
      Valued.v (P.2 - P.1) <
        MonoidWithZeroHom.ValueGroup₀.embedding
          ((MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x)} ∈
    uniformity K⸨X⸩

Tactic:
simp_rw [← Valued.v.restrict_lt_iff_lt_embedding]

Goal state after:
case h.refine_1
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))) ⋯
x : K⸨X⸩
hx : Valued.v x = ↑γ
this : Valued.v.restrict x ≠ 0
⊢ {P |
      Valued.v.restrict (P.2 - P.1) <
        (MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x} ∈
    uniformity K⸨X⸩
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✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : IsTorsionFree R S
inst✝² : Algebra R Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
Q Q' : ↑(p.primesOver S)
⊢ { toFun := fun P ↦ ⟨Ideal.map (algebraMap S Sₚ) ↑P, ⋯⟩, invFun := fun Q ↦ ⟨comap (algebraMap S Sₚ) ↑Q, ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        Q ≤
      { toFun := fun P ↦ ⟨Ideal.map (algebraMap S Sₚ) ↑P, ⋯⟩, invFun := fun Q ↦ ⟨comap (algebraMap S Sₚ) ↑Q, ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        Q' ↔
    Q ≤ Q'

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ map_mono h⟩
    have : Q'.1.IsMaximal :=
      (primesOver.isPrime p Q').isMaximal (ne_bot_of_mem_primesOver hp Q'.prop)
    simpa [under_map_of_isMaximal S p] using le_comap_of_map_le h

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this✝ : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
⊢ (s ⟨↑⟨m - 1, ⋯⟩, hm⟩ - if hi : ↑⟨m - 1, ⋯⟩ + 1 < m then s ⟨↑⟨m - 1, ⋯⟩ + 1, hi⟩ else 0) = s ⟨m - 1, hm⟩

pp: case refine_2.ht
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this✝ : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
⊢ ∀ (j : Fin n), m ≤ ↑j → invAccumulate n m s j = 0

Tactic:
dif_neg this.not_gt,

Goal state after:
case refine_2
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this✝ : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
⊢ s ⟨↑⟨m - 1, ⋯⟩, hm⟩ - 0 = s ⟨m - 1, hm⟩

case refine_2.ht
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this✝ : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
⊢ ∀ (j : Fin n), m ≤ ↑j → invAccumulate n m s j = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case inr.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
k : σ
hk : (fun x1 x2 ↦ x1 < x2) k i
⊢ (ofLex (p.support.sup ⇑toLex)) k = (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))) k

pp: case inr.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ (ofLex (p.support.sup ⇑toLex)) i < (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))) i

Tactic:
· conv_rhs => rw [← Equiv.swap_apply_of_ne_of_ne hk.ne (hk.trans_le hle).ne]
    rw [Finsupp.mapDomain_apply (Equiv.injective _), supDegree]; rfl

Goal state after:
case inr.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ (ofLex (p.support.sup ⇑toLex)) i < (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))) i
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
⊢ Function.Surjective ⇑(esymmAlgHom (Fin m) R n)

Tactic:
intro p

Goal state after:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : ↥(symmetricSubalgebra (Fin m) R)
⊢ ∃ a, (esymmAlgHom (Fin m) R n) a = p
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case add
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p q : MvPolynomial (Fin m) R
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
hq : (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) (p + q) ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
map_add

Goal state after:
case add
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p q : MvPolynomial (Fin m) R
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
hq : (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) p + (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range
Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced

Goal state before:
pp: k : Type u_1
A : Type u_2
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
h : ∀ (B : Subalgebra k A), B.FG → IsGeometricallyReduced k ↥B
⊢ IsGeometricallyReduced k A

Tactic:
simp_rw [isGeometricallyReduced_field_iff] at h ⊢

Goal state after:
k : Type u_1
A : Type u_2
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
h : ∀ (B : Subalgebra k A), B.FG → IsReduced (AlgebraicClosure k ⊗[k] ↥B)
⊢ IsReduced (AlgebraicClosure k ⊗[k] A)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
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
⊢ Tendsto (⇑Valued.v)
    (Filter.comap (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) (𝓝 a))
    (𝓝 (Valued.v a))

Tactic:
· rw [WithZeroTopology.tendsto_of_ne_zero ((Valuation.ne_zero_iff Valued.v).mpr ha),
      Filter.eventually_comap, Filter.Eventually, Valued.mem_nhds]
    use Units.mk0 (Valued.v.restrict a) (by simp [Valuation.restrict_def, ha])
    simp only [Units.val_mk0, v_def, Set.ofPred_subset_ofPred]
    rintro y val_y b rfl
    rw [← valuedAdicCompletion_eq_valuation']
    exact (Valuation.restrict_inj _).mp <| Valuation.map_eq_of_sub_lt Valued.v.restrict val_y

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
hx : x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K) x
hf : f = (ratfuncAdicComplRingEquiv K) x
hval : Valued.v f ≤ 1
F : K⟦X⟧
hF : (ofPowerSeries ℤ K) F = f
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) = x

Tactic:
by rw [hF, hf, RingEquiv.symm_apply_apply]

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

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ n ∈ (C (⅟↑p ^ n) * (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))).vars ∧
    (C (⅟↑p ^ n) * (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))).vars ⊆ range (n + 1)

Tactic:
vars_C_mul _ (Invertible.ne_zero _),

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ n ∈ (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars ∧
    (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars ⊆ range (n + 1)