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 : ℕ
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 ℤ))
⊢ ((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 ℤ))
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s.succ)) :
    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 ℤ))
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 ℤ))
⊢ ((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 ℤ))
      (HPow.hPow (α := K⟦ℤ⟧) (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X : K⟦ℤ⟧) s.succ) :
    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 ℤ))
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 ℤ))
⊢ ((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 ℤ)) (exp (-(↑s.succ : ℤ))) (exp (↑s.succ : ℤ))⁻¹
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
n d : ℕ
f : K⟦X⟧
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
hnd : n < d
⊢ Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) f : K) (0 : K)
have apply : HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
Tactic: apply (PowerSeries.X_pow_dvd_iff).mp _ n hnd
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
n d : ℕ
f : K⟦X⟧
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
hnd : n < d
⊢ HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
have rwa : ∀
  (H :
    LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) f) :
        WithZero (Multiplicative ℤ))
      (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
  (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
Tactic: rwa [← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap,
    intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d, PowerSeries.idealX,
    Ideal.span_singleton_pow, Ideal.span_singleton_dvd_span_singleton_iff_dvd] at H
Cleared hypotheses: H, hnd
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
n d : ℕ
f : K⟦X⟧
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
hnd : n < d
rwa :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
            ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
⊢ HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
have rwa₁ : ∀
  (H :
    LE.le (α := 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⸩) f) :
        WithZero (Multiplicative ℤ))
      (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
  (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
Tactic: rwa [← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap,
    intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d, PowerSeries.idealX,
    Ideal.span_singleton_pow, Ideal.span_singleton_dvd_span_singleton_iff_dvd] at H
Cleared hypotheses: H, hnd
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
n d : ℕ
f : K⟦X⟧
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
hnd : n < d
rwa :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
            ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₁ :
  ∀
    (H :
      LE.le (α := 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⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
⊢ HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
have rwa₂ : ∀
  (H :
    LE.le (α := WithZero (Multiplicative ℤ))
      (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          f :
        WithZero (Multiplicative ℤ))
      (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
  (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
Tactic: rwa [← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap,
    intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d, PowerSeries.idealX,
    Ideal.span_singleton_pow, Ideal.span_singleton_dvd_span_singleton_iff_dvd] at H
Cleared hypotheses: H, hnd
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
n d : ℕ
f : K⟦X⟧
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
hnd : n < d
rwa :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
            ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₁ :
  ∀
    (H :
      LE.le (α := 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⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₂ :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
              (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
            f :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
⊢ HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
have rwa₃ : ∀ (H : HPow.hPow (α := Ideal K⟦X⟧) (asIdeal (PowerSeries.idealX K)) d ∣ Ideal.span {f}) (hnd : n < d),
  HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
Tactic: rwa [← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap,
    intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d, PowerSeries.idealX,
    Ideal.span_singleton_pow, Ideal.span_singleton_dvd_span_singleton_iff_dvd] at H
Cleared hypotheses: H, hnd
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
n d : ℕ
f : K⟦X⟧
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
hnd : n < d
rwa :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
            ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₁ :
  ∀
    (H :
      LE.le (α := 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⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₂ :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
              (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
            f :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₃ :
  ∀ (H : HPow.hPow (α := Ideal K⟦X⟧) (asIdeal (PowerSeries.idealX K)) d ∣ Ideal.span {f}) (hnd : n < d),
    HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
⊢ HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
have rwa₄ : ∀
  (H :
    HPow.hPow (α := Ideal K⟦X⟧)
        (asIdeal
          { asIdeal := Ideal.span {PowerSeries.X}, isPrime := sorry, ne_bot := sorry :
            IsDedekindDomain.HeightOneSpectrum K⟦X⟧ })
        d ∣
      Ideal.span {f})
  (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
Tactic: rwa [← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap,
    intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d, PowerSeries.idealX,
    Ideal.span_singleton_pow, Ideal.span_singleton_dvd_span_singleton_iff_dvd] at H
Cleared hypotheses: H, hnd
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
n d : ℕ
f : K⟦X⟧
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
hnd : n < d
rwa :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
            ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₁ :
  ∀
    (H :
      LE.le (α := 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⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₂ :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
              (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
            f :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₃ :
  ∀ (H : HPow.hPow (α := Ideal K⟦X⟧) (asIdeal (PowerSeries.idealX K)) d ∣ Ideal.span {f}) (hnd : n < d),
    HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₄ :
  ∀
    (H :
      HPow.hPow (α := Ideal K⟦X⟧)
          (asIdeal
            { asIdeal := Ideal.span {PowerSeries.X}, isPrime := ⋯, ne_bot := ⋯ :
              IsDedekindDomain.HeightOneSpectrum K⟦X⟧ })
          d ∣
        Ideal.span {f})
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
⊢ HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
have rwa₅ : ∀ (H : Dvd.dvd (α := Ideal K⟦X⟧) (Ideal.span {HPow.hPow (α := K⟦X⟧) PowerSeries.X d}) (Ideal.span {f})) (hnd : n < d),
  HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
Tactic: rwa [← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap,
    intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d, PowerSeries.idealX,
    Ideal.span_singleton_pow, Ideal.span_singleton_dvd_span_singleton_iff_dvd] at H
Cleared hypotheses: H, hnd
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
n d : ℕ
f : K⟦X⟧
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
hnd : n < d
rwa :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
            ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₁ :
  ∀
    (H :
      LE.le (α := 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⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₂ :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
              (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
            f :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₃ :
  ∀ (H : HPow.hPow (α := Ideal K⟦X⟧) (asIdeal (PowerSeries.idealX K)) d ∣ Ideal.span {f}) (hnd : n < d),
    HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₄ :
  ∀
    (H :
      HPow.hPow (α := Ideal K⟦X⟧)
          (asIdeal
            { asIdeal := Ideal.span {PowerSeries.X}, isPrime := ⋯, ne_bot := ⋯ :
              IsDedekindDomain.HeightOneSpectrum K⟦X⟧ })
          d ∣
        Ideal.span {f})
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₅ :
  ∀ (H : Dvd.dvd (α := Ideal K⟦X⟧) (Ideal.span {HPow.hPow (α := K⟦X⟧) PowerSeries.X d}) (Ideal.span {f})) (hnd : n < d),
    HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
⊢ HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
have rwa₆ : ∀ (H : HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f) (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
Tactic: rwa [← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap,
    intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d, PowerSeries.idealX,
    Ideal.span_singleton_pow, Ideal.span_singleton_dvd_span_singleton_iff_dvd] at H
Cleared hypotheses: H, hnd