[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hpx : eval₂ (algebraMap O R) x p = 0
hvx : 1 < ↑v x
⊢ False
[PROOFSTEP]
rw [hpm.as_sum, eval₂_add, eval₂_pow, eval₂_X, eval₂_finset_sum, add_eq_zero_iff_eq_neg] at hpx 
[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hpx : x ^ natDegree p = -∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i)
hvx : 1 < ↑v x
⊢ False
[PROOFSTEP]
replace hpx := congr_arg v hpx
[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
⊢ False
[PROOFSTEP]
refine' ne_of_gt _ hpx
[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
⊢ ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i)) < ↑v (x ^ natDegree p)
[PROOFSTEP]
rw [v.map_neg, v.map_pow]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
⊢ ↑v (∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i)) < ↑v x ^ natDegree p
[PROOFSTEP]
refine' v.map_sum_lt' (zero_lt_one.trans_le (one_le_pow_of_one_le' hvx.le _)) fun i hi => _
[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range (natDegree p)
⊢ ↑v (eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i)) < ↑v x ^ natDegree p
[PROOFSTEP]
rw [eval₂_mul, eval₂_pow, eval₂_C, eval₂_X, v.map_mul, v.map_pow, ← one_mul (v x ^ p.natDegree)]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range (natDegree p)
⊢ ↑v (↑(algebraMap O R) (coeff p i)) * ↑v x ^ i < 1 * ↑v x ^ natDegree p
[PROOFSTEP]
cases' (hv.2 <| p.coeff i).lt_or_eq with hvpi hvpi
[GOAL]
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 : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range (natDegree p)
hvpi : ↑v (↑(algebraMap O R) (coeff p i)) < 1
⊢ ↑v (↑(algebraMap O R) (coeff p i)) * ↑v x ^ i < 1 * ↑v x ^ natDegree p
[PROOFSTEP]
exact mul_lt_mul₀ hvpi (pow_lt_pow₀ hvx <| Finset.mem_range.1 hi)
[GOAL]
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 : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range (natDegree p)
hvpi : ↑v (↑(algebraMap O R) (coeff p i)) = 1
⊢ ↑v (↑(algebraMap O R) (coeff p i)) * ↑v x ^ i < 1 * ↑v x ^ natDegree p
[PROOFSTEP]
erw [hvpi]
[GOAL]
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 : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range (natDegree p)
hvpi : ↑v (↑(algebraMap O R) (coeff p i)) = 1
⊢ 1 * ↑v x ^ i < 1 * ↑v x ^ natDegree p
[PROOFSTEP]
rw [one_mul, one_mul]
[GOAL]
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 : Integers v O
x : R
hx : IsIntegral O x
p : O[X]
hpm : Monic p
hvx : 1 < ↑v x
hpx : ↑v (x ^ natDegree p) = ↑v (-∑ i in Finset.range (natDegree p), eval₂ (algebraMap O R) x (↑C (coeff p i) * X ^ i))
i : ℕ
hi : i ∈ Finset.range (natDegree p)
hvpi : ↑v (↑(algebraMap O R) (coeff p i)) = 1
⊢ ↑v x ^ i < ↑v x ^ natDegree p
[PROOFSTEP]
exact pow_lt_pow₀ hvx (Finset.mem_range.1 hi)
