Proving that an element is an integer of a valuation ring

Stream: new members

[Stepan Nesterov]

Let's say I want to write down an element of a ring docs#valuation.integer. I try doing it like this:

import ring_theory.valuation.basic
import algebra.order.monoid.with_zero.defs
variables {R : Type*} [comm_ring R] {w : valuation R ℤₘ₀}
def my_integer (a : R) (ha : w a = 0) : w.integer := ⟨a, begin rw set.mem_def, end⟩

but get a message

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_2 ∈ ?m_3

[Stepan Nesterov]

How do I figure out what the right ∈ is, so that I can rw it?

[Gareth Ma]

Not sure if this answers your question, but:

import ring_theory.valuation.basic
import ring_theory.valuation.integers
import algebra.order.monoid.with_zero.defs

open_locale discrete_valuation

variables {R : Type*} [comm_ring R] {w : valuation R ℤₘ₀}
example (a : R) (ha : w a = 0) : a ∈ w.integer :=
begin
  simp only [valuation.integer, subring.mem_mk, mem_set_of_eq, ha, zero_le_one],
end

[Adam Topaz]

@Stepan Nesterov can you please provide a working #mwe ?

[Adam Topaz]

Anyway, it seems like whoever wrote this part of the valuation theory library forgot to make a valuation.mem_integer lemma.
The following is (approximately) what I would do in this case.

import ring_theory.valuation.integers

variables {R Γ : Type*} [comm_ring R] [linear_ordered_comm_group_with_zero Γ] {w : valuation R Γ}

lemma valuation.mem_integer_iff (a : R) : a ∈ w.integer ↔ w a ≤ 1 := iff.rfl

example (a : R) (ha : w a = 0) : a ∈ w.integer :=
begin
  rw [valuation.mem_integer_iff, ha],
  exact zero_le_one,
end