-- 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:
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 ((algebraMap O R) (p.coeff i)) * v x ^ i < 1 * v x ^ p.natDegree

Tactic:
rw [hvpi, one_mul, one_mul]

Result:
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

Proof state:
case inl
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 ((algebraMap O R) (p.coeff i)) * v x ^ i < 1 * v x ^ p.natDegree

Tactic:
exact mul_lt_mul'' hvpi (pow_lt_pow_right₀ hvx <| Finset.mem_range.1 hi) zero_le' zero_le'

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))
i : ℕ
hi : i ∈ Finset.range p.natDegree
⊢ v (eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i)) < v x ^ p.natDegree

Tactic:
rw [eval₂_mul, eval₂_pow, eval₂_C, eval₂_X, v.map_mul, v.map_pow, ←
  one_mul (v x ^ p.natDegree)]

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))
i : ℕ
hi : i ∈ Finset.range p.natDegree
⊢ v ((algebraMap O R) (p.coeff i)) * v x ^ i < 1 * v x ^ p.natDegree

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))
i : ℕ
hi : i ∈ Finset.range p.natDegree
⊢ v ((algebraMap O R) (p.coeff i)) * v x ^ i < 1 * v x ^ p.natDegree

Tactic:
rcases (hv.2 <| p.coeff i).lt_or_eq with hvpi | hvpi

Result:
case inl
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 ((algebraMap O R) (p.coeff i)) * v x ^ i < 1 * v x ^ p.natDegree

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 ((algebraMap O R) (p.coeff i)) * v x ^ i < 1 * v x ^ p.natDegree

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
hpx : x ^ p.natDegree = -∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i)
hvx : 1 < v x
⊢ False

Tactic:
replace hpx := congr_arg v 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))
⊢ False

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
hpx : eval₂ (algebraMap O R) x p = 0
hvx : 1 < v x
⊢ False

Tactic:
rw [hpm.as_sum, eval₂_add, eval₂_pow, eval₂_X, eval₂_finset_sum, add_eq_zero_iff_eq_neg] at 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
hpx : x ^ p.natDegree = -∑ i ∈ Finset.range p.natDegree, eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i)
hvx : 1 < v x
⊢ False

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:
refine v.map_sum_lt' (zero_lt_one.trans_le (one_le_pow_of_one_le' hvx.le _)) fun i hi => ?_

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))
i : ℕ
hi : i ∈ Finset.range p.natDegree
⊢ v (eval₂ (algebraMap O R) x (C (p.coeff i) * X ^ i)) < v x ^ p.natDegree