mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬Valued.v a = 0 ∧ ∃ x, Valued.v a * ↑n = Valued.v x
a : adicCompletion K v
ha0 : ¬Valued.v a = 0
x : adicCompletion K v
hx : Valued.v a * ↑n = Valued.v x
b : K
hb : (valuation K v) b = Valued.v a
y : K
hy : (valuation K v) y = Valued.v x
⊢ Valued.v a * ↑n = Valued.v x

Tactic:
]

Goal state after:
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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬Valued.v a = 0 ∧ ∃ x, Valued.v a * ↑n = Valued.v x
a : adicCompletion K v
ha0 : ¬Valued.v a = 0
x : adicCompletion K v
hx : Valued.v a * ↑n = Valued.v x
b : K
hb : (valuation K v) b = Valued.v a
y : K
hy : (valuation K v) y = Valued.v x
⊢ Valued.v a * ↑n = Valued.v x
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f : MvPowerSeries σ R
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) ↑((trunc' R i) f)) atTop (𝓝 ((coeff d) f))

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f : MvPowerSeries σ R
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) ↑((trunc' R i) f)) atTop (𝓝 ((coeff d) f))
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) ↑((trunc R i) f)) atTop (𝓝 ((coeff d) f))

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) ↑((trunc R i) f)) atTop (𝓝 ((coeff d) f))
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
p : ℕ
hf : f.IsHomogeneous p
d : σ →₀ ℕ
hd : (weight fun x ↦ 1) d ≠ p
⊢ (weight 1) d ≠ p

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
p : ℕ
hf : f.IsHomogeneous p
d : σ →₀ ℕ
hd : (weight fun x ↦ 1) d ≠ p
⊢ (weight 1) d ≠ p
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
p : ℕ
d : σ →₀ ℕ
f : MvPowerSeries σ R
⊢ (coeff d) ((homogeneousComponent p) f) = if (weight fun x ↦ 1) d = p then (coeff d) f else 0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
p : ℕ
d : σ →₀ ℕ
f : MvPowerSeries σ R
⊢ (coeff d) ((homogeneousComponent p) f) = if (weight fun x ↦ 1) d = p then (coeff d) f else 0
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 : adicCompletion K v
⊢ ¬Valued.v x ≤ 1 ↔ 1 < Valued.v x

Tactic:
]

Goal state after:
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 : adicCompletion K v
⊢ ¬Valued.v x ≤ 1 ↔ 1 < Valued.v x
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h✝ : True
n : σ →₀ ℕ
hn : n ≥ d + Finsupp.single s 1
⊢ (coeff d) f = (coeff d) f

pp: case hc
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h✝ : True
n : σ →₀ ℕ
hn : n ≥ d + Finsupp.single s 1
⊢ d < n

Tactic:
]

Goal state after:
case hc
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h✝ : True
n : σ →₀ ℕ
hn : n ≥ d + Finsupp.single s 1
⊢ d < n
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case ih
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
r : S
x : WithVal (valuation K v)
⊢ ↑x * (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r =
    ↑x * (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r

Tactic:
]

Goal state after:
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✝ : DiscreteTopology M
⊢ (pure 0).HasBasis (fun x ↦ True) fun x ↦ ↑⊥

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✝ : DiscreteTopology M
⊢ (pure 0).HasBasis (fun x ↦ True) fun x ↦ ↑⊥
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
S₀ : Type u_4
inst✝³ : CommSemiring S₀
inst✝² : Algebra S₀ S
inst✝¹ : Algebra S₀ K
inst✝ : IsScalarTower S₀ S K
x : S₀
⊢ (algebraMap S (valuation K v).Completion) ((algebraMap S₀ S) x) =
    (algebraMap S (valuation K v).Completion) ((algebraMap S₀ S) x)

Tactic:
]

Goal state after:
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
hf : constantCoeff f = 0
⊢ IsNilpotent 0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ IsNilpotent 0
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
⊢ DenseRange ((fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K v)).symm x) }) ∘ ⇑(algebraMap K K))

Tactic:
]

Goal state after:
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
⊢ DenseRange ((fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K v)).symm x) }) ∘ ⇑(algebraMap K K))
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
r : R
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) } ≤ 1

Tactic:
]

Goal state after:
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
r : R
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) } ≤ 1
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
⊢ ∀ (x : σ →₀ ℕ), HasSum (fun i ↦ (monomial i) ((coeff i) f) x) (f x)

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ ∀ (x : σ →₀ ℕ), HasSum (fun i ↦ (monomial i) ((coeff i) f) x) (f x)
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
r : R
⊢ Valued.v ((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) ≤ 1

Tactic:
]

Goal state after:
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
r : R
⊢ Valued.v ((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) ≤ 1
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
r : R
⊢ Valued.v ((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) ≤ 1

Tactic:
simpa using v.valuation_le_one _

Goal state after:
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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ (algebraMap R (adicCompletion K v)) r * ↑x ∈ adicCompletionIntegers K v

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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ (algebraMap R (adicCompletion K v)) r * ↑x ∈ adicCompletionIntegers K v
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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ ((fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K v)).symm x) }) ∘ ⇑(algebraMap R K)) r ∈
    adicCompletionIntegers K v

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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ ((fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K v)).symm x) }) ∘ ⇑(algebraMap R K)) r ∈
    adicCompletionIntegers K v
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
r : R
x : ↥(adicCompletionIntegers K v)
⊢ x *
      { toFun := fun r ↦ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) }, ⋯⟩,
          map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
        r =
    x *
      { toFun := fun r ↦ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) }, ⋯⟩,
          map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
        r

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
hf : φ ≠ 0
⊢ φ.order = φ.order

Tactic:
]

Goal state after:
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.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✝ : FaithfulSMul R K
⊢ Function.Injective ⇑(algebraMap R ↥(adicCompletionIntegers K v))

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✝ : FaithfulSMul R K
⊢ Function.Injective ⇑(algebraMap R ↥(adicCompletionIntegers K v))
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑n

pp: case hnc
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ¬φ = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑n

case hnc
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ¬φ = 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✝ : FaithfulSMul R K
x y : R
⊢ ↑((algebraMap R ↥(adicCompletionIntegers K v)) x) = ↑((algebraMap R ↥(adicCompletionIntegers K v)) y) → x = y

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✝ : FaithfulSMul R K
x y : R
⊢ ↑((algebraMap R ↥(adicCompletionIntegers K v)) x) = ↑((algebraMap R ↥(adicCompletionIntegers K v)) y) → x = y
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
r : R
⊢ Valued.v (↑r).toCompletion = (valuation K v) ↑r

Tactic:
]

Goal state after:
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
r : R
⊢ Valued.v (↑r).toCompletion = (valuation K v) ↑r
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
h' : ¬φ = 0
⊢ n < φ.order.toNat

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
h' : ¬φ = 0
⊢ n < φ.order.toNat
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
k : K
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm k) }.toCompletion = (valuation K v) k

Tactic:
]

Goal state after:
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
k : K
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm k) }.toCompletion = (valuation K v) k
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
r : R
⊢ (valuation K v) ↑r ≤ 1

Tactic:
]

Goal state after:
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
r : R
⊢ (valuation K v) ↑r ≤ 1
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
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
a : adicCompletion K v
ha : 1 < Valued.v a
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
]

Goal state after:
case neg
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
a : adicCompletion K v
ha : 1 < Valued.v a
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: case inr
σ : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
i : ι
hi : ∀ (b : ι), i ≤ b → ↑((Finsupp.weight w) d) < weightedOrder w (f b)
s : Finset ι
hs : ¬↑s ⊆ Set.Iio i
x : ι
hxs : x ∈ ↑s
hxi : i ≤ x
⊢ (coeff d) (∏ i ∈ s, f i) = 0

Tactic:
]

Goal state after:
case inr
σ : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
i : ι
hi : ∀ (b : ι), i ≤ b → ↑((Finsupp.weight w) d) < weightedOrder w (f b)
s : Finset ι
hs : ¬↑s ⊆ Set.Iio i
x : ι
hxs : x ∈ ↑s
hxi : i ≤ x
⊢ (coeff d) (∏ i ∈ s, f i) = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
i : ℕ
hi : ↑(Finsupp.degree (single () i)) < MvPowerSeries.order φ
⊢ (coeff i) φ = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
i : ℕ
hi : ↑(Finsupp.degree (single () i)) < MvPowerSeries.order φ
⊢ (coeff i) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
⊢ φ.order ≤ φ.order ∧ φ.order ≤ ψ.order

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
⊢ φ.order ≤ φ.order ∧ φ.order ≤ ψ.order
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : ¬m < n
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ (∀ (i : ℕ), ↑i = φ.order → (coeff i) (φ + ψ) ≠ 0) ∧ ∀ (i : ℕ), ↑i < φ.order → (coeff i) (φ + ψ) = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ (∀ (i : ℕ), ↑i = φ.order → (coeff i) (φ + ψ) ≠ 0) ∧ ∀ (i : ℕ), ↑i < φ.order → (coeff i) (φ + ψ) = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) (φ + ψ) ≠ 0

Tactic:
]

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) (φ + ψ) ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) φ ≠ 0

Tactic:
]

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) φ ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
hi : ↑i < φ.order
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ∑ x ∈ range n, (Polynomial.monomial x) ((coeff x) f) + (Polynomial.monomial n) ((coeff n) f) =
    ∑ m ∈ range n, (Polynomial.monomial m) ((coeff m) f) + (Polynomial.monomial n) ((coeff n) f)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
⊢ 0 = 0

pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
⊢ ∀ x ∈ antidiagonal n, (coeff x.1) φ * (coeff x.2) ψ = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
⊢ ∀ x ∈ antidiagonal n, (coeff x.1) φ * (coeff x.2) ψ = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ↑i < φ.order
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : φ.order ≤ ↑i
hj : ↑j < ψ.order
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : ((trunc (n + 1)) f).natDegree < n + 1
⊢ ∑ i ∈ range (n + 1), G (((trunc (n + 1)) f).coeff i) * s ^ i = ∑ i ∈ range (n + 1), G ((coeff i) f) * s ^ i

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : ((trunc (n + 1)) f).natDegree < n + 1
⊢ ∑ i ∈ range (n + 1), G (((trunc (n + 1)) f).coeff i) * s ^ i = ∑ i ∈ range (n + 1), G ((coeff i) f) * s ^ i
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : R
h_mono : Monotone ⇑(toNNReal ⋯)
⊢ (toNNReal ⋯) (v.intValuation (x + y)) ≤ (toNNReal ⋯) (max (v.intValuation x) (v.intValuation y))

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : R
h_mono : Monotone ⇑(toNNReal ⋯)
⊢ (toNNReal ⋯) (v.intValuation (x + y)) ≤ (toNNReal ⋯) (max (v.intValuation x) (v.intValuation y))
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j).1 + (i, j).2 = n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ ↑n = ↑n

Tactic:
]

Goal state after: