awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
s : ℕ
rw :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₁ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
            (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₂ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
            (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₃ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          PowerSeries.X :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
⊢ 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) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
have rw₄ : HPow.hPow (α := WithZero (Multiplicative ℤ)) (exp (-1)) s = exp (-(↑s : ℤ))
Tactic: rw [map_pow, valuation_def, ← LaurentSeries.coe_algebraMap,
    valuation_of_algebraMap, intValuation_X, ← exp_nsmul, smul_neg, nsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
s : ℕ
rw :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₁ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
            (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₂ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
            (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₃ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          PowerSeries.X :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₄ : HPow.hPow (α := WithZero (Multiplicative ℤ)) (exp (-1)) s = exp (-(↑s : ℤ))
⊢ 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) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
have rw₅ : exp (HSMul.hSMul (β := ℤ) s (-1)) = exp (-(↑s : ℤ))
Tactic: rw [map_pow, valuation_def, ← LaurentSeries.coe_algebraMap,
    valuation_of_algebraMap, intValuation_X, ← exp_nsmul, smul_neg, nsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
s : ℕ
rw :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₁ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
            (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₂ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
            (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₃ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          PowerSeries.X :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₄ : HPow.hPow (α := WithZero (Multiplicative ℤ)) (exp (-1)) s = exp (-(↑s : ℤ))
rw₅ : exp (HSMul.hSMul (β := ℤ) s (-1)) = exp (-(↑s : ℤ))
⊢ 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) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
have rw₆ : exp (-HSMul.hSMul (β := ℤ) s 1) = exp (-(↑s : ℤ))
Tactic: rw [map_pow, valuation_def, ← LaurentSeries.coe_algebraMap,
    valuation_of_algebraMap, intValuation_X, ← exp_nsmul, smul_neg, nsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
s : ℕ
rw :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₁ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
            (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₂ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
            (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₃ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          PowerSeries.X :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₄ : HPow.hPow (α := WithZero (Multiplicative ℤ)) (exp (-1)) s = exp (-(↑s : ℤ))
rw₅ : exp (HSMul.hSMul (β := ℤ) s (-1)) = exp (-(↑s : ℤ))
rw₆ : exp (-HSMul.hSMul (β := ℤ) s 1) = exp (-(↑s : ℤ))
⊢ 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) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
have rw₇ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑s : ℤ))) (exp (-(↑s : ℤ)))
Tactic: rw [map_pow, valuation_def, ← LaurentSeries.coe_algebraMap,
    valuation_of_algebraMap, intValuation_X, ← exp_nsmul, smul_neg, nsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
s : ℤ
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single s : (a : K) → K⟦ℤ⟧) 1) =
    exp (-s)
have ofNat : ∀ (s : ℕ),
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.ofNat s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.ofNat s)
Tactic: obtain s | s := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
s : ℤ
ofNat :
  ∀ (s : ℕ),
    ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        ((single (Int.ofNat s) : (a : K) → K⟦ℤ⟧) 1) =
      exp (-Int.ofNat s)
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single s : (a : K) → K⟦ℤ⟧) 1) =
    exp (-s)
have negSucc : ∀ (s : ℕ),
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.negSucc s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.negSucc s)
Tactic: obtain s | s := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
s : ℕ
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.ofNat s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.ofNat s)
have ofNat : Eq (α := WithZero (Multiplicative ℤ))
  (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (↑s : ℤ) : (a : K) → K⟦ℤ⟧) 1) :
    WithZero (Multiplicative ℤ))
  (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
Tactic: rw [Int.ofNat_eq_natCast, ← HahnSeries.ofPowerSeries_X_pow, PowerSeries.coe_pow,
      valuation_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
s : ℕ
ofNat :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        ((single (↑s : ℤ) : (a : K) → K⟦ℤ⟧) 1) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.ofNat s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.ofNat s)
have ofNat₁ : 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)) :
    WithZero (Multiplicative ℤ))
  (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
Tactic: rw [Int.ofNat_eq_natCast, ← HahnSeries.ofPowerSeries_X_pow, PowerSeries.coe_pow,
      valuation_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
s : ℕ
ofNat :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        ((single (↑s : ℤ) : (a : K) → K⟦ℤ⟧) 1) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
ofNat₁ :
  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)) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.ofNat s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.ofNat s)
have ofNat₂ : 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) :
    WithZero (Multiplicative ℤ))
  (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
Tactic: rw [Int.ofNat_eq_natCast, ← HahnSeries.ofPowerSeries_X_pow, PowerSeries.coe_pow,
      valuation_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
s : ℕ
ofNat :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        ((single (↑s : ℤ) : (a : K) → K⟦ℤ⟧) 1) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
ofNat₁ :
  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)) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
ofNat₂ :
  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) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.ofNat s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.ofNat s)
have ofNat₃ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑s : ℤ))) (exp (-(↑s : ℤ)))
Tactic: rw [Int.ofNat_eq_natCast, ← HahnSeries.ofPowerSeries_X_pow, PowerSeries.coe_pow,
      valuation_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
s : ℕ
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.negSucc s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.negSucc s)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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)
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.negSucc s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.negSucc s)
have 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))⁻¹
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]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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))⁻¹
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.negSucc s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.negSucc s)
have 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))⁻¹
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]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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))⁻¹
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.negSucc s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.negSucc s)
have 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))⁻¹
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]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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))⁻¹
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.negSucc s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.negSucc s)
have 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))⁻¹
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]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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))⁻¹
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.negSucc s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.negSucc s)
have 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 ℤ))
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]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 ℤ))
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.negSucc s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.negSucc s)
have 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 ℤ))
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]