-- Mathlib/RingTheory/LaurentSeries.lean
theorem exists_Polynomial_intValuation_lt (F : K⟦X⟧) (η : ℤₘ₀ˣ) :
    ∃ P : K[X], (PowerSeries.idealX K).intValuation (F - P) < η

Proof state:
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Tactic:
by_cases h_neg : 1 < η

Result:
case pos
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : 1 < η
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

case neg
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : ¬1 < η
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Proof state:
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
⊢ ∀ n < d + 1, (PowerSeries.coeff K n) (F - ↑(trunc (d + 1) F)) = 0

Tactic:
simpa only [map_sub, sub_eq_zero, Polynomial.coeff_coe, coeff_trunc] using
  fun _ h ↦ (if_pos h).symm

Result:
no goals

Proof state:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑(F - ↑(trunc (d + 1) F)) < ↑η

Tactic:
apply lt_of_le_of_lt this

Result:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ ↑η * ↑(Multiplicative.ofAdd (-1)) < ↑η

Proof state:
case neg
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : ¬1 < η
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Tactic:
rw [not_lt, ← Units.val_le_val, Units.val_one, ← WithZero.coe_one, ← coe_unzero η.ne_zero,
  coe_le_coe, ← Multiplicative.toAdd_le, toAdd_one] at h_neg

Result:
case neg
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Proof state:
case neg
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Tactic:
obtain ⟨d, hd⟩ := Int.exists_eq_neg_ofNat h_neg

Result:
case neg.intro
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Proof state:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
⊢ (PowerSeries.idealX K).intValuation (F - ↑(trunc (d + 1) F)) < ↑η

Tactic:
have : Valued.v ((ofPowerSeries ℤ K) (F - (trunc (d + 1) F))) ≤
  (Multiplicative.ofAdd (-(d + 1 : ℤ))) := by
  apply (intValuation_le_iff_coeff_lt_eq_zero K _).mpr
  simpa only [map_sub, sub_eq_zero, Polynomial.coeff_coe, coeff_trunc] using
    fun _ h ↦ (if_pos h).symm

Result:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((ofPowerSeries ℤ K) (F - ↑(trunc (d + 1) F))) ≤ ↑(Multiplicative.ofAdd (-(↑d + 1)))
⊢ (PowerSeries.idealX K).intValuation (F - ↑(trunc (d + 1) F)) < ↑η

Proof state:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ ↑η * ↑(Multiplicative.ofAdd (-1)) < ↑η

Tactic:
rw [← mul_one (η : ℤₘ₀), mul_assoc, one_mul]

Result:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ ↑η * ↑(Multiplicative.ofAdd (-1)) < ↑η * 1

Proof state:
case neg.intro
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Tactic:
use F.trunc (d + 1)

Result:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
⊢ (PowerSeries.idealX K).intValuation (F - ↑(trunc (d + 1) F)) < ↑η

Proof state:
case pos
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : 1 < η
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Tactic:
use 0

Result:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : 1 < η
⊢ (PowerSeries.idealX K).intValuation (F - ↑0) < ↑η

Proof state:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ (PowerSeries.idealX K).intValuation (F - ↑(trunc (d + 1) F)) < ↑η

Tactic:
rw [← valuation_of_algebraMap (K := K⸨X⸩) (PowerSeries.idealX K) (F - F.trunc (d + 1))]

Result:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑(F - ↑(trunc (d + 1) F)) < ↑η

Proof state:
case h.bc
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ 0 < 1

Tactic:
exact Int.zero_lt_one

Result:
no goals

Proof state:
case h.a0
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ 0 < ↑η

Tactic:
exact zero_lt_iff.2 η.ne_zero

Result:
no goals

Proof state:
case h.bc
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ ↑(Multiplicative.ofAdd (-1)) < 1

Tactic:
rw [← WithZero.coe_one, coe_lt_coe, ofAdd_neg, Right.inv_lt_one_iff, ← ofAdd_zero,
  Multiplicative.ofAdd_lt]

Result:
case h.bc
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ 0 < 1

Proof state:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((ofPowerSeries ℤ K) (F - ↑(trunc (d + 1) F))) ≤ ↑(Multiplicative.ofAdd (-(↑d + 1)))
⊢ (PowerSeries.idealX K).intValuation (F - ↑(trunc (d + 1) F)) < ↑η

Tactic:
rw [ neg_add, ofAdd_add, ← hd, ofAdd_toAdd, WithZero.coe_mul, coe_unzero,
  ← coe_algebraMap] at this

Result:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ (PowerSeries.idealX K).intValuation (F - ↑(trunc (d + 1) F)) < ↑η