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

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n d : R
hd : d ∈ nonZeroDivisors R
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
v : Ideal R
hv✝ : Irreducible (Associates.mk v)
hv : Prime v
h : (valuation K { asIdeal := v, isPrime := ⋯, ne_bot := ⋯ }) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hv' : Irreducible (Associates.mk v)
⊢ Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {n}))

Tactic:
[

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n d : R
hd : d ∈ nonZeroDivisors R
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
v : Ideal R
hv✝ : Irreducible (Associates.mk v)
hv : Prime v
h : (valuation K { asIdeal := v, isPrime := ⋯, ne_bot := ⋯ }) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hv' : Irreducible (Associates.mk v)
⊢ Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {n}))
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ↑(weightedOrder w f).toNat = weightedOrder w f
⊢ ∃ d, (coeff d) f ≠ 0 ∧ ↑((weight w) d) = weightedOrder w f

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ↑(weightedOrder w f).toNat = weightedOrder w f
⊢ ∃ d, (coeff d) f ≠ 0 ∧ ↑((weight w) d) = weightedOrder w f
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x y : MvPolynomial σ R
h : ↑x = ↑y
m✝ : σ →₀ ℕ
⊢ coeff m✝ x = coeff m✝ y

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x y : MvPolynomial σ R
h : ↑x = ↑y
m✝ : σ →₀ ℕ
⊢ coeff m✝ x = coeff m✝ y
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case top
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff d) f = 0
⊢ ⊤ ≤ weightedOrder w f

pp: case coe
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff d) f = 0
⊢ ↑a✝ ≤ weightedOrder w f

Tactic:
· rw [top_le_iff, weightedOrder_eq_top_iff]
    ext d; exact h d (ENat.natCast_lt_top _)

Goal state after:
case coe
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff d) f = 0
⊢ ↑a✝ ≤ weightedOrder w f
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

Tactic:
obtain (⟨r, hr⟩ | ⟨r, hr⟩) :=
    ValuationRing.isInteger_or_isInteger (valuationSubringAtPrime K v) x

Goal state after:
case inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x⁻¹
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f✝ g✝ f g x : ι →₀ α
⊢ (∀ (i : ι), x i ∈ (f.rangeIcc g) i) ↔ f ≤ x ∧ x ≤ g

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f✝ g✝ f g x : ι →₀ α
⊢ (∀ (i : ι), x i ∈ (f.rangeIcc g) i) ↔ f ≤ x ∧ x ≤ g
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f g : ι →₀ α
⊢ #(Icc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i))

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f g : ι →₀ α
⊢ #(Icc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i))
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
ht : IsLowerSet ↑t
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hxs : x ∈ s
hxt : x ∈ t
i j : σ →₀ ℕ
hij : i + j = x
⊢ i ≤ x

Tactic:
simp [← hij]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
ht : IsLowerSet ↑t
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hxs : x ∈ s
hxt : x ∈ t
i j : σ →₀ ℕ
hij : i + j = x
⊢ j ≤ x

Tactic:
simp [← hij]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ (coeff d) (f * g) = 0

Tactic:
apply coeff_eq_zero_of_lt_weightedOrder w

Goal state after:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ ↑((weight w) d) < weightedOrder w (f * g)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ (coeff d) (g * f) = 0

Tactic:
apply coeff_eq_zero_of_lt_weightedOrder w

Goal state after:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ ↑((weight w) d) < weightedOrder w (g * f)
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h : (trunc' R n) f = (trunc' R n) g
this : ∀ {f' : MvPowerSeries σ R}, (coeff n) f' = MvPolynomial.coeff n ((trunc' R n) f')
⊢ (coeff n) f = (coeff n) g

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h : (trunc' R n) f = (trunc' R n) g
this : ∀ {f' : MvPowerSeries σ R}, (coeff n) f' = MvPolynomial.coeff n ((trunc' R n) f')
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ n d, (coeff d) f ≠ 0 ∧ degree d = n

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ n d, (coeff d) f ≠ 0 ∧ degree d = n
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ Tendsto f l (𝓝 ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a

Tactic:
[

Goal state after:
α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ Tendsto f l (𝓝 ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
h : ↑f.order.toNat = f.order
⊢ ∃ d, (coeff d) f ≠ 0 ∧ ↑(degree d) = f.order

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
h : ↑f.order.toNat = f.order
⊢ ∃ d, (coeff d) f ≠ 0 ∧ ↑(degree d) = f.order
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: ⊢ ContinuousAdd ℕ∞

Tactic:
refine ⟨continuous_iff_continuousAt.mpr fun (a, b) ↦ ?_⟩
  match a, b with
  | ⊤, _ => exact tendsto_nhds_top_mono' continuousAt_fst fun p ↦ le_add_right le_rfl
  | (a : ℕ), ⊤ => exact tendsto_nhds_top_mono' continuousAt_snd fun p ↦ le_add_left le_rfl
  | (a : ℕ), (b : ℕ) => simp [ContinuousAt, nhds_prod_eq]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: case ind
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
k : ℕ
ih : ∀ m ≤ k, ∀ {x : σ →₀ ℕ}, degree x < n → MvPolynomial.coeff x ((truncTotal n) p ^ m) = (coeff x) (p ^ m)
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) p ^ k.succ) = (coeff x) (p ^ k.succ)

Tactic:
[

Goal state after:
case ind
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
k : ℕ
ih : ∀ m ≤ k, ∀ {x : σ →₀ ℕ}, degree x < n → MvPolynomial.coeff x ((truncTotal n) p ^ m) = (coeff x) (p ^ m)
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) p ^ k.succ) = (coeff x) (p ^ k.succ)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), degree d < n → (coeff d) f = 0
⊢ ↑n ≤ f.order

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), degree d < n → (coeff d) f = 0
⊢ ↑n ≤ f.order
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑(degree d) < n → (coeff d) f = 0
⊢ n ≤ f.order

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑(degree d) < n → (coeff d) f = 0
⊢ n ≤ f.order
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
⊢ f.order = ↑n ↔ (∃ d, (coeff d) f ≠ 0 ∧ degree d = n) ∧ ∀ (d : σ →₀ ℕ), degree d < n → (coeff d) f = 0

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
⊢ f.order = ↑n ↔ (∃ d, (coeff d) f ≠ 0 ∧ degree d = n) ∧ ∀ (d : σ →₀ ℕ), degree d < n → (coeff d) f = 0
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
n m : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) p ^ m) = (coeff x) (p ^ m)

Tactic:
induction m using Nat.caseStrongRecOn generalizing x with

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
n m : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
d : σ →₀ ℕ
hd : degree d < n
⊢ MvPolynomial.coeff d ((truncTotal n) (p ^ m)) = MvPolynomial.coeff d ((truncTotal n) (↑((truncTotal n) p) ^ m))

Tactic:
[

Goal state after:
case pos
σ : Type u_1
R : Type u_2
n m : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
d : σ →₀ ℕ
hd : degree d < n
⊢ MvPolynomial.coeff d ((truncTotal n) (p ^ m)) = MvPolynomial.coeff d ((truncTotal n) (↑((truncTotal n) p) ^ m))
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
n m : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ¬degree d < n
⊢ MvPolynomial.coeff d ((truncTotal n) (p ^ m)) = MvPolynomial.coeff d ((truncTotal n) (↑((truncTotal n) p) ^ m))

Tactic:
[

Goal state after:
case neg
σ : Type u_1
R : Type u_2
n m : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ¬degree d < n
⊢ MvPolynomial.coeff d ((truncTotal n) (p ^ m)) = MvPolynomial.coeff d ((truncTotal n) (↑((truncTotal n) p) ^ m))
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : TopologicalSpace R
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : TopologicalSpace S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous[inst✝⁵, inst✝²] ⇑φ
a : R
ha : Tendsto (fun x ↦ a ^ x) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ φ a ^ x) atTop (𝓝 0)

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : TopologicalSpace R
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : TopologicalSpace S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous[inst✝⁵, inst✝²] ⇑φ
a : R
ha : Tendsto (fun x ↦ a ^ x) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ φ a ^ x) atTop (𝓝 0)
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
a b : R
ha : IsTopologicallyNilpotent a
hab : Commute a b
⊢ IsTopologicallyNilpotent (a * b)

Tactic:
[

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
a b : R
ha : IsTopologicallyNilpotent a
hab : Commute a b
⊢ IsTopologicallyNilpotent (a * b)
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
hb : IsTopologicallyNilpotent b
hab : Commute a b
⊢ IsTopologicallyNilpotent (a * b)

Tactic:
[

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
hb : IsTopologicallyNilpotent b
hab : Commute a b
⊢ IsTopologicallyNilpotent (a * b)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = p
⊢ (coeff d) f = 0

Tactic:
apply coeff_eq_zero_of_lt_weightedOrder w

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = p
⊢ ↑((weight w) d) < weightedOrder w f
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : (weight w) x.1 < p
⊢ (coeff x.1) f * (coeff x.2) g = 0

Tactic:
← ENat.natCast_lt_natCast

Goal state after:
case pos.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : ↑((weight w) x.1) < ↑p
⊢ (coeff x.1) f * (coeff x.2) g = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos.inr.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : (weight w) x.2 < q
⊢ (coeff x.1) f * (coeff x.2) g = 0

Tactic:
← ENat.natCast_lt_natCast

Goal state after:
case pos.inr.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : ↑((weight w) x.2) < ↑q
⊢ (coeff x.1) f * (coeff x.2) g = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝⁴ : Field K
inst✝³ : CommSemiring S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
v : HeightOneSpectrum R
inst✝ : Algebra S K
l : S
⊢ UniformContinuous fun x ↦ l • x

Tactic:
[

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝⁴ : Field K
inst✝³ : CommSemiring S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
v : HeightOneSpectrum R
inst✝ : Algebra S K
l : S
⊢ UniformContinuous fun x ↦ l • x
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hm : constantCoeff f ^ m = 0
⊢ IsTopologicallyNilpotent f

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hm : constantCoeff f ^ m = 0
⊢ IsTopologicallyNilpotent f
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
H : IsTopologicallyNilpotent (constantCoeff f)
⊢ IsNilpotent (constantCoeff f)

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
H : IsTopologicallyNilpotent (constantCoeff f)
⊢ IsNilpotent (constantCoeff f)
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
g : MvPowerSeries σ R
⊢ HasSum f g ↔ ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) g)

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
g : MvPowerSeries σ R
⊢ HasSum f g ↔ ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) g)
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ Summable f ↔ ∀ (d : σ →₀ ℕ), Summable fun i ↦ (coeff d) (f i)

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ Summable f ↔ ∀ (d : σ →₀ ℕ), Summable fun i ↦ (coeff d) (f i)
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ ∀ (d : σ →₀ ℕ), Summable fun i ↦ (coeff d) (f i)

Tactic:
[

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ ∀ (d : σ →₀ ℕ), Summable fun i ↦ (coeff d) (f i)
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
⊢ uR • S = uR • ↑J ∪ (uR * uR) • ↑J

Tactic:
[

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
⊢ uR • S = uR • ↑J ∪ (uR * uR) • ↑J
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
d : σ →₀ ℕ
i : ι
hi : ∀ (b : ι), i ≤ b → ↑((Finsupp.weight w) d) < weightedOrder w (f b)
⊢ (support fun i ↦ (coeff d) (f i)) ⊆ Set.Iic i

Tactic:
[

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
d : σ →₀ ℕ
i : ι
hi : ∀ (b : ι), i ≤ b → ↑((Finsupp.weight w) d) < weightedOrder w (f b)
⊢ (support fun i ↦ (coeff d) (f i)) ⊆ Set.Iic i
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
h : constantCoeff f = 0
⊢ Tendsto (fun i ↦ (f ^ i).order) atTop (𝓝 ⊤)

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
h : constantCoeff f = 0
⊢ Tendsto (fun i ↦ (f ^ i).order) atTop (𝓝 ⊤)
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
⊢ uR' • S = uR' • ↑J ∪ uR • uR' • ↑J

Tactic:
[

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
⊢ uR' • S = uR' • ↑J ∪ uR • uR' • ↑J