-- Mathlib/RingTheory/LaurentSeries.lean
theorem valuation_single_zpow (s : ℤ) :
    Valued.v (HahnSeries.single s (1 : K) : K⸨X⸩) =
      Multiplicative.ofAdd (-(s : ℤ))

Proof state:
K : Type u_2
inst✝ : Field K
s : ℤ
this : Valued.v ((single s) 1) * Valued.v ((single (-s)) 1) = 1
⊢ Valued.v ((single (-s)) 1) ≠ 0

Tactic:
simp only [Valuation.ne_zero_iff, ne_eq, one_ne_zero, not_false_iff, HahnSeries.single_ne_zero]

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
s : ℤ
this : Valued.v 1 = 1
⊢ Valued.v ((single s) 1) = ↑(Multiplicative.ofAdd (-s))

Tactic:
rw [← single_zero_one, ← add_neg_cancel s, ← mul_one 1, ← single_mul_single, map_mul,
  mul_eq_one_iff_eq_inv₀] at this

Result:
K : Type u_2
inst✝ : Field K
s : ℤ
this : Valued.v ((single s) 1) = (Valued.v ((single (-s)) 1))⁻¹
⊢ Valued.v ((single s) 1) = ↑(Multiplicative.ofAdd (-s))

K : Type u_2
inst✝ : Field K
s : ℤ
this : Valued.v ((single s) 1) * Valued.v ((single (-s)) 1) = 1
⊢ Valued.v ((single (-s)) 1) ≠ 0

Proof state:
case negSucc
K : Type u_2
inst✝ : Field K
s : ℕ
this : Valued.v ((single (Int.negSucc s)) 1) = (Valued.v ((single (-Int.negSucc s)) 1))⁻¹
⊢ (Valued.v ((single (-Int.negSucc s)) 1))⁻¹ = ↑(Multiplicative.ofAdd (-Int.negSucc s))

Tactic:
simp only [Int.negSucc_coe, neg_neg, ← HahnSeries.ofPowerSeries_X_pow, PowerSeries.coe_pow,
  valuation_X_pow, ofAdd_neg, WithZero.coe_inv, inv_inv]

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
s : ℤ
⊢ Valued.v ((single s) 1) = ↑(Multiplicative.ofAdd (-s))

Tactic:
have : Valued.v (1 : K⸨X⸩) = (1 : ℤₘ₀) := Valued.v.map_one

Result:
K : Type u_2
inst✝ : Field K
s : ℤ
this : Valued.v 1 = 1
⊢ Valued.v ((single s) 1) = ↑(Multiplicative.ofAdd (-s))

Proof state:
K : Type u_2
inst✝ : Field K
s : ℤ
this : Valued.v ((single s) 1) = (Valued.v ((single (-s)) 1))⁻¹
⊢ (Valued.v ((single (-s)) 1))⁻¹ = ↑(Multiplicative.ofAdd (-s))

Tactic:
obtain s | s := s

Result:
case ofNat
K : Type u_2
inst✝ : Field K
s : ℕ
this : Valued.v ((single (Int.ofNat s)) 1) = (Valued.v ((single (-Int.ofNat s)) 1))⁻¹
⊢ (Valued.v ((single (-Int.ofNat s)) 1))⁻¹ = ↑(Multiplicative.ofAdd (-Int.ofNat s))

case negSucc
K : Type u_2
inst✝ : Field K
s : ℕ
this : Valued.v ((single (Int.negSucc s)) 1) = (Valued.v ((single (-Int.negSucc s)) 1))⁻¹
⊢ (Valued.v ((single (-Int.negSucc s)) 1))⁻¹ = ↑(Multiplicative.ofAdd (-Int.negSucc s))

Proof state:
case ofNat
K : Type u_2
inst✝ : Field K
s : ℕ
this : Valued.v ((single (Int.ofNat s)) 1) = (Valued.v ((single (-Int.ofNat s)) 1))⁻¹
⊢ (Valued.v ((single (-Int.ofNat s)) 1))⁻¹ = ↑(Multiplicative.ofAdd (-Int.ofNat s))

Tactic:
rw [Int.ofNat_eq_coe, ← HahnSeries.ofPowerSeries_X_pow] at this

Result:
case ofNat
K : Type u_2
inst✝ : Field K
s : ℕ
this : Valued.v ((ofPowerSeries ℤ K) (PowerSeries.X ^ s)) = (Valued.v ((single (-↑s)) 1))⁻¹
⊢ (Valued.v ((single (-Int.ofNat s)) 1))⁻¹ = ↑(Multiplicative.ofAdd (-Int.ofNat s))

Proof state:
case ofNat
K : Type u_2
inst✝ : Field K
s : ℕ
this : Valued.v ((ofPowerSeries ℤ K) (PowerSeries.X ^ s)) = (Valued.v ((single (-↑s)) 1))⁻¹
⊢ (Valued.v ((single (-Int.ofNat s)) 1))⁻¹ = ↑(Multiplicative.ofAdd (-Int.ofNat s))

Tactic:
rw [Int.ofNat_eq_coe, ← this, PowerSeries.coe_pow, valuation_X_pow]

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
s : ℤ
this : Valued.v ((single s) 1) = (Valued.v ((single (-s)) 1))⁻¹
⊢ Valued.v ((single s) 1) = ↑(Multiplicative.ofAdd (-s))

Tactic:
rw [this]

Result:
K : Type u_2
inst✝ : Field K
s : ℤ
this : Valued.v ((single s) 1) = (Valued.v ((single (-s)) 1))⁻¹
⊢ (Valued.v ((single (-s)) 1))⁻¹ = ↑(Multiplicative.ofAdd (-s))