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

Goal state before:
pp: case h₂
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ ↑⟨x, hx⟩ * ↑t ≤ᵥ y * ↑s

Tactic:
simpa using

Goal state after:
case h₂
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ x * ↑t ≤ᵥ y * ↑s
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁷ : Ring R
inst✝⁶ : ValuativeRel R
K : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : ValuativeRel K
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
x z : R
γ : (ofClass (valuation R)).ValueGroup₀ˣ
x✝ : True
y : R
hy : y ∈ {z_1 | (valuation R).restrict (z_1 - z) < ↑γ}
⊢ x +ᵥ y ∈ {z_1 | (valuation R).restrict (z_1 - (x + z)) < ↑γ}

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁷ : Ring R
inst✝⁶ : ValuativeRel R
K : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : ValuativeRel K
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
x z : R
γ : (ofClass (valuation R)).ValueGroup₀ˣ
x✝ : True
y : R
hy : y ∈ {z_1 | (valuation R).restrict (z_1 - z) < ↑γ}
⊢ (valuation R).restrict (y - z) < ↑γ
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
x✝¹ x' y y' z : R✝
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
x : R
S : Type u_3
Γ : Type u_4
inst✝¹ : Ring S
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x✝ y✝ z✝ : S
h0 : ¬v z✝ ≤ v 0
h : v x✝ * v z✝ ≤ v y✝ * v z✝
⊢ 0 < v z✝

Tactic:
simpa using

Goal state after:
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
x✝¹ x' y y' z : R✝
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
x : R
S : Type u_3
Γ : Type u_4
inst✝¹ : Ring S
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x✝ y✝ z✝ : S
h0 : ¬v z✝ ≤ v 0
h : v x✝ * v z✝ ≤ v y✝ * v z✝
⊢ ¬v z✝ = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x✝ : R
h : x✝ ∈ {x | x ≤ᵥ 0}
⊢ x • x✝ ∈ {x | x ≤ᵥ 0}

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x✝ : R
h : x✝ ∈ {x | x ≤ᵥ 0}
⊢ x * x✝ ≤ᵥ 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
a✝ x✝ : R
h : a✝ ∈ supp R
⊢ a✝ * x✝ ∈ supp R

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
a✝ x✝ : R
h : a✝ ∈ supp R
⊢ a✝ * x✝ ≤ᵥ 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : ValuativeRel R
x✝ : R
⊢ x✝ ∈ supp R ↔ x✝ ∈ (valuation R).supp

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : ValuativeRel R
x✝ : R
⊢ x✝ ≤ᵥ 0 ↔ (valuation R) x✝ = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
a : R
ha : a ≤ᵥ 1
n m : ℕ
hnm : n ≤ n + m
⊢ a ^ (n + m) ≤ᵥ a ^ n

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
a : R
ha : a ≤ᵥ 1
n m : ℕ
hnm : n ≤ n + m
⊢ a ^ n * a ^ m ≤ᵥ a ^ n
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁷ : Ring R
inst✝⁶ : ValuativeRel R
K : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : ValuativeRel K
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
cts_add : ContinuousConstVAdd R R
basis : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | (valuation R).restrict x < ↑γ}
γ : (ofClass (valuation R)).ValueGroup₀ˣ
x✝ : True
y : R
hy : y ∈ {x | (valuation R).restrict x < ↑γ}
⊢ -y ∈ {x | (valuation R).restrict x < ↑γ}

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁷ : Ring R
inst✝⁶ : ValuativeRel R
K : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : ValuativeRel K
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
cts_add : ContinuousConstVAdd R R
basis : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | (valuation R).restrict x < ↑γ}
γ : (ofClass (valuation R)).ValueGroup₀ˣ
x✝ : True
y : R
hy : y ∈ {x | (valuation R).restrict x < ↑γ}
⊢ (valuation R).restrict y < ↑γ
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
a : R
ha : 1 ≤ᵥ a
n m : ℕ
hnm : n ≤ n + m
⊢ a ^ n ≤ᵥ a ^ (n + m)

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
a : R
ha : 1 ≤ᵥ a
n m : ℕ
hnm : n ≤ n + m
⊢ a ^ n ≤ᵥ a ^ n * a ^ m
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
x : K
hx : x ≠ 0
⊢ 1 ≤ᵥ x⁻¹ ↔ x ≤ᵥ 1

Tactic:
simpa using

Goal state after:
K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
x : K
hx : x ≠ 0
⊢ 1 ≤ᵥ x⁻¹ ↔ x ≤ᵥ 1
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
x : K
hx : x ≠ 0
⊢ x⁻¹ ≤ᵥ 1 ↔ 1 ≤ᵥ x

Tactic:
simpa using

Goal state after:
K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
x : K
hx : x ≠ 0
⊢ x⁻¹ ≤ᵥ 1 ↔ 1 ≤ᵥ x
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
s : (ValueGroupWithZero R)ˣ
h : 1 ≠ s
⊢ ↑s ≠ 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
s : (ValueGroupWithZero R)ˣ
h : 1 ≠ s
⊢ ¬s = 1
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
r s : (ValueGroupWithZero R)ˣ
h : r ≠ s
hr : r ≠ 1
⊢ ↑r ≠ 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
r s : (ValueGroupWithZero R)ˣ
h : r ≠ s
hr : r ≠ 1
⊢ ¬r = 1
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case refine_4
R : Type u_1
inst✝⁷ : Ring R
inst✝⁶ : ValuativeRel R
K : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : ValuativeRel K
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
cts_add : ContinuousConstVAdd R R
basis : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | (valuation R).restrict x < ↑γ}
x₀ : R
⊢ Tendsto (fun x ↦ x₀ + x) (𝓝 0) (𝓝 x₀)

Tactic:
simpa using

Goal state after:
case refine_4
R : Type u_1
inst✝⁷ : Ring R
inst✝⁶ : ValuativeRel R
K : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : ValuativeRel K
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
cts_add : ContinuousConstVAdd R R
basis : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | (valuation R).restrict x < ↑γ}
x₀ : R
⊢ Tendsto (fun x ↦ x₀ + x) (𝓝 0) (𝓝 x₀)
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case refine_5
R : Type u_1
inst✝⁷ : Ring R
inst✝⁶ : ValuativeRel R
K : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : ValuativeRel K
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
cts_add : ContinuousConstVAdd R R
basis : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | (valuation R).restrict x < ↑γ}
x₀ : R
⊢ Tendsto (fun x ↦ -x₀ + x) (𝓝 x₀) (𝓝 0)

Tactic:
simpa using

Goal state after:
case refine_5
R : Type u_1
inst✝⁷ : Ring R
inst✝⁶ : ValuativeRel R
K : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : ValuativeRel K
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
cts_add : ContinuousConstVAdd R R
basis : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | (valuation R).restrict x < ↑γ}
x₀ : R
⊢ Tendsto (fun x ↦ -x₀ + x) (𝓝 x₀) (𝓝 0)
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsClosed[_i.toTopologicalSpace] {x | v.restrict x = 0}

Tactic:
simpa using

Goal state after:
case inl
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsClosed[_i.toTopologicalSpace] {x | v x = 0}
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
⊢ v r ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
⊢ ¬v r = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : v r ≠ 0
⊢ v r ≤ v ↑s → v r < v ↑s

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : v r ≠ 0
⊢ v r ≤ v ↑s → v r < v ↑s
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr✝ : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : v r ≠ 0
hγ' : v r ≤ v ↑s → v r < v ↑s
hr : ¬v r = 1
⊢ v r ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr✝ : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : v r ≠ 0
hγ' : v r ≤ v ↑s → v r < v ↑s
hr : ¬v r = 1
⊢ ¬v r = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr✝ : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : v r ≠ 0
hγ' : v r ≤ v ↑s → v r < v ↑s
hr : ¬v r = 1
⊢ v r ≠ 0

Tactic:
simpa using hγ

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
hr : v r ≠ 0
hr' : v r ≠ 1
⊢ (valuation R) r ≠ 1

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
hr : v r ≠ 0
hr' : v r ≠ 1
⊢ ¬(valuation R) r = 1
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
x : K
y : ↥(posSubmonoid K)
⊢ ValueGroupWithZero.mk x y = (valuation K) x / (valuation K) ↑y

Tactic:
ValueGroupWithZero.mk_eq_div

Goal state after:
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
x : K
y : ↥(posSubmonoid K)
⊢ (valuation K) x / (valuation K) ↑y = (valuation K) x / (valuation K) ↑y
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: K : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : ValuativeRel K
Γ₀ : Type u_3
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
inst✝³ : TopologicalSpace K
inst✝² : IsValuativeTopology K
inst✝¹ : MulArchimedean Γ₀
v : Valuation K Γ₀
inst✝ : v.Compatible
r : Γ₀
hr : r ≠ 0
h : ∀ (x : K), v x ≠ 0 → r < v x
⊢ ∀ (x : K), x ≠ 0 → v x = 1

Tactic:
simpa using

Goal state after:
K : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : ValuativeRel K
Γ₀ : Type u_3
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
inst✝³ : TopologicalSpace K
inst✝² : IsValuativeTopology K
inst✝¹ : MulArchimedean Γ₀
v : Valuation K Γ₀
inst✝ : v.Compatible
r : Γ₀
hr : r ≠ 0
h : ∀ (x : K), v x ≠ 0 → r < v x
⊢ ∀ (x : K), ¬x = 0 → v x = 1
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : ValuativeRel R
inst✝¹ : IsDiscrete R
inst✝ : IsNontrivial R
⊢ 0 < uniformizer R

Tactic:
by
  obtain ⟨γ, hγ, hγ'⟩ := IsNontrivial.exists_lt_one (R := R)
  exact hγ.trans_le (le_uniformizer_iff.mpr hγ')

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

Goal state before:
pp: α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : IsTopologicalRing α
inst✝⁶ : IsUniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : IsUniformAddGroup β
inst✝² : IsTopologicalRing β
f : α →+* β
hf✝ : Continuous ⇑f
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
hf' : Continuous ⇑↑f
hf : UniformContinuous ⇑f
⊢ Completion.extension (⇑f) 0 = 0

Tactic:
by simp_rw [← coe_zero, extension_coe hf, f.map_zero]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : v (a * ↑s) < v (b * ↑r)
⊢ (ofClass v) a * (ofClass v) ↑s < (ofClass v) b * (ofClass v) ↑r

Tactic:
simpa using

Goal state after:
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : v (a * ↑s) < v (b * ↑r)
⊢ v a * v ↑s < v b * v ↑r
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
γ : ValueGroupWithZero R
x : R
⊢ v.restrict x < (orderMonoidIso v) γ ↔ (valuation R) x < γ

Tactic:
simpa using

Goal state after:
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
γ : ValueGroupWithZero R
x : R
⊢ v.restrict x < (orderMonoidIso v) γ ↔ (valuation R) x < γ
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : ValuativeRel A
inst✝² : ValuativeRel B
inst✝¹ : Algebra A B
inst✝ : ValuativeExtension A B
x✝ : ↥(posSubmonoid A)
a : A
ha : a ∈ posSubmonoid A
⊢ (algebraMap A B) a ∈ posSubmonoid B

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : ValuativeRel A
inst✝² : ValuativeRel B
inst✝¹ : Algebra A B
inst✝ : ValuativeExtension A B
x✝ : ↥(posSubmonoid A)
a : A
ha : a ∈ posSubmonoid A
⊢ 0 <ᵥ a
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
⊢ zpowers (generator' v) = ⊤

Tactic:
by
  rw [← map_subtype_inj, MonoidHom.map_zpowers,
    subtype_apply, ← MonoidHom.range_eq_map, Subgroup.subtype_range]
  apply generator_zpowers_eq_valueGroup

Goal state after:
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 Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I : Ideal ↥v.valuationSubring
⊢ ∀ (P : Ideal ↥v.valuationSubring), P.IsPrime → Submodule.IsPrincipal P

Tactic:
intro P hP

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
⊢ Submodule.IsPrincipal P
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: 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
⊢ IsLocalRing.maximalIdeal A ≠ ⊥

Tactic:
simpa using

Goal state after:
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
⊢ ¬IsField A
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case h.right
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
v : Valuation K (WithZero (Multiplicative ℤ)) := ⋯
π : K := ⋯
hπ : v π = ↑(ofAdd (-1))
⊢ Units.mk0 (v π) ⋯ ≠ 1

Tactic:
simpa using

Goal state after:
case h.right
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
v : Valuation K (WithZero (Multiplicative ℤ)) := valuation K (maximalIdeal A)
π : K := ⋯.choose
hπ : v π = ↑(ofAdd (-1))
⊢ ¬Units.mk0 (↑(ofAdd 1))⁻¹ ⋯ = 1
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 r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h : v (x - y) < min (v s / v r * (v y * v y)) (v y)
hr' : 0 < v r
⊢ v (x⁻¹ - y⁻¹) * v r < v s

Tactic:
let γ : Γ₀ˣ := .mk0 (v s / v r) (by simp [hs, hr])

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h : v (x - y) < min (v s / v r * (v y * v y)) (v y)
hr' : 0 < v r
γ : Γ₀ˣ := Units.mk0 (v s / v r) ⋯
⊢ v (x⁻¹ - y⁻¹) * v r < v s
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 Γ₀
γ : (ofClass v).ValueGroup₀ˣ
r : K
hr : (restrict₀ (ofClass v)) r = ↑γ
⊢ v 0 < v r

Tactic:
simpa using

Goal state after:
K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
γ : (ofClass v).ValueGroup₀ˣ
r : K
hr : (restrict₀ (ofClass v)) r = ↑γ
⊢ 0 < v r
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ⟨↑x, hx⟩ < z
hz' : z < ⟨↑y, hy⟩
⊢ ∃ a, (↑a ∈ s ∧ x < a) ∧ a < y

Tactic:
simp only [← Subtype.coe_lt_coe] at hz hz'

Goal state after:
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ ∃ a, (↑a ∈ s ∧ x < a) ∧ a < y
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
γ' : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hdef : γ' = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
y : K
hy : v y < (ofClass v) x
⊢ y ∈ {k | v k < v x}

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
γ' : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hdef : γ' = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
y : K
hy : v y < (ofClass v) x
⊢ v y < v x
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: 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
⊢ MonoidHom.mker (valuation K (maximalIdeal A)) = Submonoid.map (algebraMap A K) (IsUnit.submonoid A)

Tactic:
by
  ext a
  simp only [MonoidHom.mem_mker, Submonoid.mem_map]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨b, rfl⟩ := IsDiscreteValuationRing.exists_lift_of_le_one h.le
    rw [valuation_eq_one_iff_notMem] at h
    simp only [IsDiscreteValuationRing.maximalIdeal, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
      not_not] at h
    use b, h
  · obtain ⟨x, h, rfl⟩ := h
    simpa [IsDiscreteValuationRing.maximalIdeal] using! h

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : v.restrict x ≠ 0
⊢ v x ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : v.restrict x ≠ 0
⊢ ¬x = 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
x : K
h : x ≠ 0
h0 : v x ≠ 0
⊢ v x ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
x : K
h : x ≠ 0
h0 : v x ≠ 0
⊢ ¬x = 0
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+ ℤ
he : ¬IsOfFinAddOrder (e 1)
⊢ AddSubgroup.zmultiples (e 1) = AddSubgroup.zmultiples 1

Tactic:
simpa using

Goal state after:
e : ℤ ≃+ ℤ
he : ¬IsOfFinAddOrder (e 1)
⊢ ⊤ = AddSubgroup.zmultiples (e 1)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
a : G
ha : a ∈ closure {x}
⊢ (fun x_1 ↦ ⟨1, ⋯⟩) ((fun x_1 ↦ ⟨1, ⋯⟩) ⟨a, ha⟩) = ⟨a, ha⟩

Tactic:
simpa using

Goal state after:
case refine_1
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
a : G
ha : a ∈ closure {x}
⊢ a = 1
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
a : G'
ha : a ∈ closure {y}
⊢ (fun x_1 ↦ ⟨1, ⋯⟩) ((fun x_1 ↦ ⟨1, ⋯⟩) ⟨a, ha⟩) = ⟨a, ha⟩

Tactic:
simpa using

Goal state after:
case refine_2
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
a : G'
ha : a ∈ closure {y}
⊢ a = 1