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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
hasup : ∃ a_1, a_1 * x = a
u : R
hi : u * x ∈ I
⊢ u * x ∈ span {x * y}

Tactic:
obtain ⟨v, rfl⟩ := hasup

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I ↑(span {v * x}) = span {y}
⊢ u * x ∈ span {x * y}
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
H : Associated π₁ π₂
⊢ v.IsUniformizer ↑π₂

Tactic:
obtain ⟨u, hu⟩ := H

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
u : (↥v.valuationSubring)ˣ
hu : π₁ * ↑u = π₂
⊢ v.IsUniformizer ↑π₂
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
H :
  (valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ n)) *
        (valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ m))⁻¹ *
      (valuation K (maximalIdeal A)) ((algebraMap A K) ↑w)⁻¹ ≤
    1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
map_inv₀,

Goal state after:
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
H :
  (valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ n)) *
        ((valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ m)))⁻¹ *
      (valuation K (maximalIdeal A)) ((algebraMap A K) ↑w)⁻¹ ≤
    1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
H :
  (valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ n)) *
        ((valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ m)))⁻¹ *
      (valuation K (maximalIdeal A)) ((algebraMap A K) ↑w)⁻¹ ≤
    1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
map_inv₀,

Goal state after:
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
H :
  (valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ n)) *
        ((valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ m)))⁻¹ *
      ((valuation K (maximalIdeal A)) ((algebraMap A K) ↑w))⁻¹ ≤
    1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ v x⁻¹ * v (y - x) * v y⁻¹ = (v x)⁻¹ * v (y - x) * (v y)⁻¹

Tactic:
map_inv₀,

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ (v x)⁻¹ * v (y - x) * v y⁻¹ = (v x)⁻¹ * v (y - x) * (v y)⁻¹
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : Function.Surjective ⇑v
γ : Γ₀ˣ
r : K
hr : v r = ↑γ
⊢ 0 < v r ∧ 0 < v 1 ∧ v r / v 1 = ↑γ

Tactic:
simp [hr]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ b ∈ closure {a} ↔ ∃! k, a ^ k = b

Tactic:
mem_closure_singleton

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ (∃ n, a ^ n = b) ↔ ∃! k, a ^ k = b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: x : ℤ ≃+ ℤ
⊢ x ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_2

Tactic:
obtain rfl | rfl := Int.addEquiv_eq_refl_or_neg x <;>
    simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
this : closure {a} = closure {b}
ha : a ∈ closure {b}
⊢ b = |a|ₘ ∧ 1 < b

Tactic:
mem_closure_singleton

Goal state after:
case mp
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
this : closure {a} = closure {b}
ha : ∃ n, b ^ n = a
⊢ b = |a|ₘ ∧ 1 < b
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 Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
⊢ Tendsto (fun p ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 (1 * 1))

Tactic:
refine
          Tendsto.mul continuous_fst.continuousAt (Tendsto.comp ?_ continuous_snd.continuousAt)

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
⊢ Tendsto Inv.inv (𝓝 (1, 1).2) (𝓝 1)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
⊢ Nonempty (Additive G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
exact LinearOrderedAddCommGroup.discrete_or_denselyOrdered (Additive G)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case pos
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : lmax ≤ 1
⊢ ∃ C, IsIntegral R (C • W)

Tactic:
use ⟨1, 0, 0, 0⟩
    apply isIntegral_of_exists_lift R
    all_goals simpa [← mem_integer_iff, variableChange_def, Valuation.mem_integer_iff]
      using (hlmax _ (by simp [l₀, l])).trans hlmax_le_1

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = if single s 1 = single t 1 then 1 else 0
⊢ s = t

Tactic:
split_ifs at h with H

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : single s 1 = single t 1
h : 1 = 1
⊢ s = t

case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : ¬single s 1 = single t 1
h : 1 = 0
⊢ s = t
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
⊢ n ≤ m s

Tactic:
← hij,

Goal state after:
case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
⊢ n ≤ ((single s n, j).1 + (single s n, j).2) s
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
n : ℕ
⊢ b ^ n * (a ^ n * (coeff n) f) = (a * b) ^ n * (coeff n) f

Tactic:
rw [mul_pow, mul_comm _ (b ^ n), mul_assoc]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ (i, j) = (single s n, m - single s n)

Tactic:
← hij,

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ (i, j) = (single s n, (i, j).1 + (i, j).2 - single s n)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r = 0
⊢ v.intValuation r < 1 ↔ v.asIdeal ∣ Ideal.span {r}

Tactic:
simp [hr]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ m - single s n + single s n = m

Tactic:
← hij,

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ (i, j).1 + (i, j).2 - single s n + single s n = (i, j).1 + (i, j).2
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
this : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ ∑ p ∈ {(0, 1), (1, 0)}, (coeff p.1) φ * (coeff p.2) ψ = (coeff 1) φ * constantCoeff ψ + (coeff 1) ψ * constantCoeff φ

Tactic:
Finset.sum_insert,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
this : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (coeff (0, 1).1) φ * (coeff (0, 1).2) ψ + ∑ x ∈ {(1, 0)}, (coeff x.1) φ * (coeff x.2) ψ =
    (coeff 1) φ * constantCoeff ψ + (coeff 1) ψ * constantCoeff φ

R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
this : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (0, 1) ∉ {(1, 0)}
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case inr.succ
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ ∑ p ∈ {(0, 1), (1, 0)}, (coeff p.1) (φ ^ n') * (coeff p.2) φ =
    ↑(n' + 1) * (coeff 1) φ * constantCoeff φ ^ (n' + 1 - 1)

Tactic:
Finset.sum_insert,

Goal state after:
case inr.succ
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (coeff (0, 1).1) (φ ^ n') * (coeff (0, 1).2) φ + ∑ x ∈ {(1, 0)}, (coeff x.1) (φ ^ n') * (coeff x.2) φ =
    ↑(n' + 1) * (coeff 1) φ * constantCoeff φ ^ (n' + 1 - 1)

case inr.succ
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (0, 1) ∉ {(1, 0)}
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ constantCoeff φ ^ n' * (coeff 1) φ + (coeff 1) (φ ^ n') * constantCoeff φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
rw [ih]

Goal state after:
case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ constantCoeff φ ^ n' * (coeff 1) φ + ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1) * constantCoeff φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ n' > 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ ∃ π, v.intValuation π = exp (-1)

Tactic:
by
  have hv : Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible
  have hlt : v.asIdeal ^ 2 < v.asIdeal := by
    rw [← Ideal.dvdNotUnit_iff_lt]
    exact ⟨v.ne_bot, v.asIdeal, Ideal.isUnit_iff.not.mpr v.isPrime.ne_top, sq v.asIdeal⟩
  obtain ⟨π, mem, notMem⟩ := SetLike.exists_of_lt hlt
  have hπ : Associates.mk (Ideal.span {π}) ≠ 0 := by
    rw [Associates.mk_ne_zero']
    intro h
    rw [h] at notMem
    exact notMem (Submodule.zero_mem (v.asIdeal ^ 2))
  use π
  rw [intValuation_if_neg _ (Associates.mk_ne_zero'.mp hπ), exp_inj]
  apply congr_arg
  rw [← Int.ofNat_one, Int.natCast_inj]
  rw [← Ideal.dvd_span_singleton, ← Associates.mk_le_mk_iff_dvd] at mem notMem
  rw [← pow_one (Associates.mk v.asIdeal), Associates.prime_pow_dvd_iff_le hπ hv] at mem
  rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le hπ hv, not_le] at notMem
  exact Nat.eq_of_le_of_lt_succ mem notMem

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
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ v.intValuation r ≤ 1

Tactic:
exact v.intValuation_le_one r

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
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
⊢ IsLocalization.mk' K n ⟨d, hd⟩ ∈ (algebraMap R K).range

Tactic:
obtain rfl | hn0 := eq_or_ne n 0

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
d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K 0 ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K 0 ⟨d, hd⟩ * (algebraMap R K) ↑(0, ⟨d, hd⟩).2 = (algebraMap R K) (0, ⟨d, hd⟩).1
⊢ IsLocalization.mk' K 0 ⟨d, hd⟩ ∈ (algebraMap R K).range

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
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
⊢ IsLocalization.mk' K n ⟨d, hd⟩ ∈ (algebraMap R K).range
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
⊢ (valuation K v).valuationSubring ≠ ⊤

Tactic:
simp only [ne_eq, Valuation.valuationSubring_eq_top_iff, not_not]

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
⊢ (valuation K v).IsNontrivial
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ weightedOrder w ((monomial d) a) = ⊤

Tactic:
rw [h, weightedOrder_eq_top_iff, map_zero]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz : v.intValuation a ≠ 0
hγz : ↑γ ≠ 0
n : ℕ
hna : exp (-↑n) < v.intValuation a
hnγ : exp (-↑n) < ↑γ
⊢ exp (-↑n) ≤ v.intValuation a

Tactic:
hna

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz : v.intValuation a ≠ 0
hγz : ↑γ ≠ 0
n : ℕ
hna : exp (-↑n) < v.intValuation a
hnγ : exp (-↑n) < ↑γ
⊢ v.intValuation a ≤ v.intValuation a
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ ↑((weight w) i)
hj : weightedOrder w g ≤ ↑((weight w) j)
hij : i + j = d
⊢ ↑((weight w) d) = ↑((weight w) i) + ↑((weight w) j)

Tactic:
← hij,

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ ↑((weight w) i)
hj : weightedOrder w g ≤ ↑((weight w) j)
hij : i + j = d
⊢ ↑((weight w) (i + j)) = ↑((weight w) i) + ↑((weight w) j)
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m ((trunc' R n) φ) = if m ≤ n then (coeff m) φ else 0

Tactic:
simpa using! coeff_truncFinset (s := Iic n) (x := m) φ

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
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : adicCompletion K v
⊢ (valuation K v) x = embedding (Valued.v.restrict x.toCompletion)

Tactic:
embedding_restrict

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
⊢ (valuation K v) x = Valued.v x.toCompletion
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: case inl
σ : 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 : IsEmpty ι
⊢ Summable f

Tactic:
apply summable_empty

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

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

Tactic:
← Finsupp.degree_single () i

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
⊢ (φ + ψ).order = φ.order

Tactic:
order_eq

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.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ((monomial n) a).order = ↑n

Tactic:
order_eq

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∀ (i : ℕ), ↑i = ↑n → (coeff i) ((monomial n) a) ≠ 0) ∧ ∀ (i : ℕ), ↑i < ↑n → (coeff i) ((monomial n) a) = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ emultiplicity X φ = ↑φ.order.toNat

Tactic:
apply le_antisymm _

Goal state after:
case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ ↑φ.order.toNat ≤ emultiplicity X φ

R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ emultiplicity X φ ≤ ↑φ.order.toNat
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable f

Tactic:
apply summable_empty

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
φ : R →+* S
a : S
inst✝¹ : UniformSpace R
inst✝ : UniformSpace S
⊢ Polynomial.eval₂ φ a Polynomial.X = a

Tactic:
Polynomial.eval₂_X

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
φ : R →+* S
a : S
inst✝¹ : UniformSpace R
inst✝ : UniformSpace S
⊢ a = a