-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
s : ℕ
negSucc :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (-HAdd.hAdd (α := ℤ) (↑s : ℤ) 1) : (a : K) → K⟦ℤ⟧) 1) =
    exp (- -HAdd.hAdd (α := ℤ) (↑s : ℤ) 1)
negSucc₁ :
  (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        ((single (-HAdd.hAdd (α := ℤ) (↑s : ℤ) 1) : (a : K) → K⟦ℤ⟧) 1))⁻¹ =
    (exp (- -HAdd.hAdd (α := ℤ) (↑s : ℤ) 1))⁻¹
negSucc₂ :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (-HAdd.hAdd (α := ℤ) (↑s : ℤ) 1) : (a : K) → K⟦ℤ⟧) 1)⁻¹ =
    (exp (- -HAdd.hAdd (α := ℤ) (↑s : ℤ) 1))⁻¹
negSucc₃ :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (- -HAdd.hAdd (α := ℤ) (↑s : ℤ) 1) : (a : K) → K⟦ℤ⟧) 1⁻¹) =
    (exp (- -HAdd.hAdd (α := ℤ) (↑s : ℤ) 1))⁻¹
negSucc₄ :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (HAdd.hAdd (α := ℤ) (↑s : ℤ) 1) : (a : K) → K⟦ℤ⟧) 1⁻¹) =
    (exp (HAdd.hAdd (α := ℤ) (↑s : ℤ) 1))⁻¹
negSucc₅ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        ((single (↑s.succ : ℤ) : (a : K) → K⟦ℤ⟧) 1⁻¹) :
      WithZero (Multiplicative ℤ))
    ((exp (↑s.succ : ℤ))⁻¹ : WithZero (Multiplicative ℤ))
negSucc₆ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        ((single (↑s.succ : ℤ) : (a : K) → K⟦ℤ⟧) 1) :
      WithZero (Multiplicative ℤ))
    ((exp (↑s.succ : ℤ))⁻¹ : WithZero (Multiplicative ℤ))
negSucc₇ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s.succ)) :
      WithZero (Multiplicative ℤ))
    ((exp (↑s.succ : ℤ))⁻¹ : WithZero (Multiplicative ℤ))
negSucc₈ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := K⟦ℤ⟧) (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X : K⟦ℤ⟧)
          s.succ) :
      WithZero (Multiplicative ℤ))
    ((exp (↑s.succ : ℤ))⁻¹ : WithZero (Multiplicative ℤ))
negSucc₉ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑s.succ : ℤ))) (exp (↑s.succ : ℤ))⁻¹
negSucc₁₀ negSucc₁₁ : Eq (α := WithZero (Multiplicative ℤ)) (exp (↑s.succ : ℤ))⁻¹ (exp (↑s.succ : ℤ))⁻¹
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.negSucc s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.negSucc s)

Tactic:
rw [Int.negSucc_eq, ← inv_inj, ← map_inv₀, inv_single, neg_neg, ← Int.natCast_succ, inv_one,
      ← HahnSeries.ofPowerSeries_X_pow, PowerSeries.coe_pow, valuation_X_pow, exp_neg]

Premises used: HahnSeries.ofPowerSeries_X_pow, inv_one, map_inv₀, neg_neg, Int.natCast_succ, inv_inj, Int.negSucc_eq, HahnSeries.inv_single, PowerSeries.coe_pow, LaurentSeries.valuation_X_pow, WithZero.exp_neg