-- Mathlib/RingTheory/Valuation/Integral.lean
theorem mem_of_integral {x : R} (hx : IsIntegral O x) : x ∈ v.integer :=
  let ⟨p, hpm, hpx⟩ := hx
  le_of_not_lt fun hvx : 1 < v x => by
    rw [hpm.as_sum, eval₂_add, eval₂_pow, eval₂_X, eval₂_finset_sum, add_eq_zero_iff_eq_neg] at hpx
    replace hpx := congr_arg v hpx; refine ne_of_gt ?_ hpx
    rw [v.map_neg, v.map_pow]
    refine v.map_sum_lt' (zero_lt_one.trans_le (one_le_pow_of_one_le' hvx.le _)) fun i hi => ?_
    rw [eval₂_mul, eval₂_pow, eval₂_C, eval₂_X, v.map_mul, v.map_pow, ←
      one_mul (v x ^ p.natDegree)]
    rcases (hv.2 <| p.coeff i).lt_or_eq with hvpi | hvpi
    · exact mul_lt_mul'' hvpi (pow_lt_pow_right₀ hvx <| Finset.mem_range.1 hi) zero_le' zero_le'
    · rw [hvpi, one_mul, one_mul]; exact pow_lt_pow_right₀ hvx (Finset.mem_range.1 hi)

Proof state:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
hx : IsIntegral O x
p : O[X]
hpm : p.Monic
hvx : 1 < v x
hpx : v (x ^ p.natDegree) = v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i))
⊢ False

Tactic:
refine ne_of_gt ?_ hpx

Result:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
hx : IsIntegral O x
p : O[X]
hpm : p.Monic
hvx : 1 < v x
hpx : v (x ^ p.natDegree) = v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i))
⊢ v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i)) < v (x ^ p.natDegree)

Proof state:
case inr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
hx : IsIntegral O x
p : O[X]
hpm : p.Monic
hvx : 1 < v x
hpx : v (x ^ p.natDegree) = v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range p.natDegree
hvpi : v ((algebraMap O R) (p.coeff i)) = 1
⊢ v x ^ i < v x ^ p.natDegree

Tactic:
exact pow_lt_pow_right₀ hvx (Finset.mem_range.1 hi)

Result:
no goals

Proof state:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
hx : IsIntegral O x
p : O[X]
hpm : p.Monic
hvx : 1 < v x
hpx : v (x ^ p.natDegree) = v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i))
⊢ v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i)) < v (x ^ p.natDegree)

Tactic:
rw [v.map_neg, v.map_pow]

Result:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
hx : IsIntegral O x
p : O[X]
hpm : p.Monic
hvx : 1 < v x
hpx : v (x ^ p.natDegree) = v (-∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i))
⊢ v (∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i)) < v x ^ p.natDegree