awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
rw :
  Eq (α := ℕ∞)
    (if x : Eq (α := MvPowerSeries σ R) 0 0 then ⊤
    else
      (↑(Nat.find (p := fun (n : ℕ) ↦
            ∃ (d : σ →₀ ℕ),
              Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R) (0 : R) ∧
                (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
            ⋯) :
        ℕ∞))
    ⊤
⊢ weightedOrder.{u_1, u_2} (R := R) w 0 = ⊤
have rw₁ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [weightedOrder, dif_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ weightedOrder w f = ⊤ ↔ f = 0
have rw : ¬weightedOrder w f = ⊤ ↔ ¬f = 0
Tactic: rw [← not_iff_not, ← ne_eq, ← ne_eq, ne_zero_iff_weightedOrder_finite w, coe_toNat_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
rw : ¬weightedOrder w f = ⊤ ↔ ¬f = 0
⊢ weightedOrder w f = ⊤ ↔ f = 0
have rw₁ : weightedOrder w f ≠ ⊤ ↔ ¬f = 0
Tactic: rw [← not_iff_not, ← ne_eq, ← ne_eq, ne_zero_iff_weightedOrder_finite w, coe_toNat_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
rw : ¬weightedOrder w f = ⊤ ↔ ¬f = 0
rw₁ : weightedOrder w f ≠ ⊤ ↔ ¬f = 0
⊢ weightedOrder w f = ⊤ ↔ f = 0
have rw₂ : weightedOrder w f ≠ ⊤ ↔ f ≠ 0
Tactic: rw [← not_iff_not, ← ne_eq, ← ne_eq, ne_zero_iff_weightedOrder_finite w, coe_toNat_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
rw : ¬weightedOrder w f = ⊤ ↔ ¬f = 0
rw₁ : weightedOrder w f ≠ ⊤ ↔ ¬f = 0
rw₂ : weightedOrder w f ≠ ⊤ ↔ f ≠ 0
⊢ weightedOrder w f = ⊤ ↔ f = 0
have rw₃ : weightedOrder w f ≠ ⊤ ↔ (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
Tactic: rw [← not_iff_not, ← ne_eq, ← ne_eq, ne_zero_iff_weightedOrder_finite w, coe_toNat_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
rw : ¬weightedOrder w f = ⊤ ↔ ¬f = 0
rw₁ : weightedOrder w f ≠ ⊤ ↔ ¬f = 0
rw₂ : weightedOrder w f ≠ ⊤ ↔ f ≠ 0
rw₃ : weightedOrder w f ≠ ⊤ ↔ (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
⊢ weightedOrder w f = ⊤ ↔ f = 0
have rw₄ : weightedOrder w f ≠ ⊤ ↔ weightedOrder w f ≠ ⊤
Tactic: rw [← not_iff_not, ← ne_eq, ← ne_eq, ne_zero_iff_weightedOrder_finite w, coe_toNat_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
have simp_rw : ∃ (d : σ →₀ ℕ),
  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
    (weight w : (a : σ →₀ ℕ) → ℕ) d =
      Nat.find (p := fun (n : ℕ) ↦
        ∃ (d : σ →₀ ℕ),
          Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
            (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
        sorry
Tactic: simp_rw [weightedOrder, dif_neg ((ne_zero_iff_weightedOrder_finite w).mpr h), Nat.cast_inj]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (weight w : (a : σ →₀ ℕ) → ℕ) d =
        Nat.find (p := fun (n : ℕ) ↦
          ∃ (d : σ →₀ ℕ),
            Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
              (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
          ⋯
have h1 : ∃ (n : ℕ) (d : σ →₀ ℕ),
  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧ (weight w : (a : σ →₀ ℕ) → ℕ) d = n
Tactic: generalize_proofs h1
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
have simp_rw : ∃ (d : σ →₀ ℕ),
  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
    Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
      (if x : f = 0 then ⊤
      else
        (↑(Nat.find (p := fun (n : ℕ) ↦
              ∃ (d : σ →₀ ℕ),
                Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
                  (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
              sorry) :
          ℕ∞))
Tactic: classical
  simp_rw [weightedOrder, dif_neg ((ne_zero_iff_weightedOrder_finite w).mpr h), Nat.cast_inj]
  generalize_proofs h1
  exact Nat.find_spec h1
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
simp_rw :
  ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
        (if x : f = 0 then ⊤
        else
          (↑(Nat.find (p := fun (n : ℕ) ↦
                ∃ (d : σ →₀ ℕ),
                  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
                    (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
                ⋯) :
            ℕ∞))
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
have simp_rw₁ : ∃ (d : σ →₀ ℕ),
  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
    Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
      (↑(Nat.find (p := fun (n : ℕ) ↦
            ∃ (d : σ →₀ ℕ),
              Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
                (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
            sorry) :
        ℕ∞)
Tactic: classical
  simp_rw [weightedOrder, dif_neg ((ne_zero_iff_weightedOrder_finite w).mpr h), Nat.cast_inj]
  generalize_proofs h1
  exact Nat.find_spec h1
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
simp_rw :
  ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
        (if x : f = 0 then ⊤
        else
          (↑(Nat.find (p := fun (n : ℕ) ↦
                ∃ (d : σ →₀ ℕ),
                  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
                    (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
                ⋯) :
            ℕ∞))
simp_rw₁ :
  ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
        (↑(Nat.find (p := fun (n : ℕ) ↦
              ∃ (d : σ →₀ ℕ),
                Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
                  (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
              ⋯) :
          ℕ∞)
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
have simp_rw₂ : ∃ (d : σ →₀ ℕ),
  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
    (weight w : (a : σ →₀ ℕ) → ℕ) d =
      Nat.find (p := fun (n : ℕ) ↦
        ∃ (d : σ →₀ ℕ),
          Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
            (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
        sorry
Tactic: classical
  simp_rw [weightedOrder, dif_neg ((ne_zero_iff_weightedOrder_finite w).mpr h), Nat.cast_inj]
  generalize_proofs h1
  exact Nat.find_spec h1
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
simp_rw :
  ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
        (if x : f = 0 then ⊤
        else
          (↑(Nat.find (p := fun (n : ℕ) ↦
                ∃ (d : σ →₀ ℕ),
                  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
                    (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
                ⋯) :
            ℕ∞))
simp_rw₁ :
  ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
        (↑(Nat.find (p := fun (n : ℕ) ↦
              ∃ (d : σ →₀ ℕ),
                Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
                  (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
              ⋯) :
          ℕ∞)
simp_rw₂ :
  ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (weight w : (a : σ →₀ ℕ) → ℕ) d =
        Nat.find (p := fun (n : ℕ) ↦
          ∃ (d : σ →₀ ℕ),
            Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
              (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
          ⋯
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
have simp_rw₃ : ∀
  (h1 :
    ∃ (n : ℕ) (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight w : (a : σ →₀ ℕ) → ℕ) d = n),
  ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (weight w : (a : σ →₀ ℕ) → ℕ) d =
        Nat.find (p := fun (n : ℕ) ↦
          ∃ (d : σ →₀ ℕ),
            Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
              (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
          h1
Tactic: classical
  simp_rw [weightedOrder, dif_neg ((ne_zero_iff_weightedOrder_finite w).mpr h), Nat.cast_inj]
  generalize_proofs h1
  exact Nat.find_spec h1
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have rw : LE.le (α := ℕ∞)
  (↑(Nat.find (p := fun (n : ℕ) ↦
        ∃ (d : σ →₀ ℕ),
          Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
            (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
        sorry) :
    ℕ∞)
  (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
Tactic: rw [weightedOrder, dif_neg]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
rw :
  LE.le (α := ℕ∞)
    (↑(Nat.find (p := fun (n : ℕ) ↦
          ∃ (d : σ →₀ ℕ),
            Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
              (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
          ⋯) :
      ℕ∞)
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
⊢ weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have hnc : ¬f = 0
Tactic: rw [weightedOrder, dif_neg]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ LE.le (α := ℕ∞)
    (↑(Nat.find (p := fun (n : ℕ) ↦
          ∃ (d : σ →₀ ℕ),
            Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
              (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
          ⋯) :
      ℕ∞)
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have simp : ∃ m ≤ (weight w : (a : σ →₀ ℕ) → ℕ) d,
  ∃ (d : σ →₀ ℕ),
    ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧ (weight w : (a : σ →₀ ℕ) → ℕ) d = m
Tactic: simp only [ne_eq, Nat.cast_le, Nat.find_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have contrapose! : ∀ (h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
  weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ (↑n : ℕ∞) ≤ weightedOrder w f
have by_contra! : ∀ (H : weightedOrder w f < (↑n : ℕ∞)), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
H : weightedOrder w f < (↑n : ℕ∞)
⊢ (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
have rw : weightedOrder w f ≠ ⊤
Tactic: rw [coe_toNat_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
H : weightedOrder w f < (↑n : ℕ∞)
⊢ False
have this : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
Tactic: have : (f.weightedOrder w).toNat = f.weightedOrder w := by
    rw [coe_toNat_eq_self]; exact ne_top_of_lt H
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
H : weightedOrder w f < (↑n : ℕ∞)
this : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
⊢ False
have obtain : ∀ (d : σ →₀ ℕ) (hfd : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R))
  (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f), False
Tactic: obtain ⟨d, hfd, hd⟩ := exists_coeff_ne_zero_and_weightedOrder w this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
H : weightedOrder w f < (↑n : ℕ∞)
this : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hfd : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
⊢ False
have H₁ : (weight w : (a : σ →₀ ℕ) → ℕ) d < n
Tactic: rw [← hd, Nat.cast_lt] at H
Cleared hypotheses: H, hfd, hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ∞
h :
  ∀ (d : σ →₀ ℕ),
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < n →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ n ≤ weightedOrder w f
have top : ∀
  (h :
    ∀ (d : σ →₀ ℕ),
      LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) ⊤ →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
  ⊤ ≤ weightedOrder w f
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ∞
h :
  ∀ (d : σ →₀ ℕ),
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < n →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
top :
  ∀
    (h :
      ∀ (d : σ →₀ ℕ),
        LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) ⊤ →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
    ⊤ ≤ weightedOrder w f
⊢ n ≤ weightedOrder w f
have coe : ∀ (a : ℕ)
  (h :
    ∀ (d : σ →₀ ℕ),
      LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) (↑a : ℕ∞) →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
  (↑a : ℕ∞) ≤ weightedOrder w f
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h :
  ∀ (d : σ →₀ ℕ),
    LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) ⊤ →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ ⊤ ≤ weightedOrder w f
have top : f = 0
Tactic: rw [top_le_iff, weightedOrder_eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h :
  ∀ (d : σ →₀ ℕ),
    LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) ⊤ →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ f = 0
have top : ∀ (d : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: ext d
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) (↑a : ℕ∞) →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ (↑a : ℕ∞) ≤ weightedOrder w f
have coe : ∀ (d : σ →₀ ℕ),
  (weight w : (a : σ →₀ ℕ) → ℕ) d < a → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: apply nat_le_weightedOrder
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ weightedOrder w f = (↑n : ℕ∞) ↔
    (∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
      ∀ (d : σ →₀ ℕ),
        (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have mp : weightedOrder w f = (↑n : ℕ∞) →
  (∃ (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
    ∀ (d : σ →₀ ℕ),
      (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
mp :
  weightedOrder w f = (↑n : ℕ∞) →
    (∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
      ∀ (d : σ →₀ ℕ),
        (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ weightedOrder w f = (↑n : ℕ∞) ↔
    (∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
      ∀ (d : σ →₀ ℕ),
        (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have mpr : ((∃ (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
    ∀ (d : σ →₀ ℕ),
      (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)) →
  weightedOrder w f = (↑n : ℕ∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : weightedOrder w f = (↑n : ℕ∞)
⊢ (∃ (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
    ∀ (d : σ →₀ ℕ),
      (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have mp : ∀ (d : σ →₀ ℕ)
  (hd :
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f),
  (∃ (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
    ∀ (d : σ →₀ ℕ),
      (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: obtain ⟨d, hd⟩ := f.exists_coeff_ne_zero_and_weightedOrder w (by simp only [h, toNat_coe])
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    if a = 0 then ⊤ else (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have pos : ∀ (h : a = 0), weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) = ⊤
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
pos : ∀ (h : a = 0), weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) = ⊤
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    if a = 0 then ⊤ else (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have neg : ∀ (h : ¬a = 0),
  weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
h : a = 0
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) = ⊤
have pos : weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) 0) = ⊤
Tactic: rw [h, weightedOrder_eq_top_iff, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
h : a = 0
pos : weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) 0) = ⊤
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) = ⊤
have pos₁ : Eq (α := MvPowerSeries σ R) ((monomial d : (a : R) → MvPowerSeries σ R) 0) 0
Tactic: rw [h, weightedOrder_eq_top_iff, map_zero]