awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
⊢ LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) f : ℕ)
have simp : LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
Tactic: simp only [weight_apply, Finsupp.sum]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
⊢ LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
have pos : ∀ (h : s ∈ f.support),
  LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
Tactic: by_cases h : s ∈ f.support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
pos :
  ∀ (h : s ∈ f.support),
    LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
⊢ LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
have neg : ∀ (h : s ∉ f.support),
  LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
Tactic: by_cases h : s ∈ f.support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
have pos : (f : (a : σ) → ℕ) s ≤
  HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) +
    ∑ x ∈ f.support \ {s}, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
Tactic: rw [Finset.sum_eq_add_sum_diff_singleton_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ (f : (a : σ) → ℕ) s ≤
    HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) +
      ∑ x ∈ f.support \ {s}, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
have pos : (f : (a : σ) → ℕ) s ≤ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s)
Tactic: refine le_trans ?_ (Nat.le_add_right _ _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ (f : (a : σ) → ℕ) s ≤ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s)
have pos : 0 < w s
Tactic: apply Nat.le_mul_of_pos_right
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (hypothesis)
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∉ f.support
⊢ LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
have h₁ : Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
Tactic: simp only [notMem_support_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
have neg : LE.le (α := ℕ) 0 (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
⊢ LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) f : ℕ)
have simp : LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
Tactic: classical
  simp only [weight_apply, Finsupp.sum]
  by_cases h : s ∈ f.support
  · rw [Finset.sum_eq_add_sum_diff_singleton_of_mem h]
    refine le_trans ?_ (Nat.le_add_right _ _)
    apply Nat.le_mul_of_pos_right
    exact Nat.zero_lt_of_ne_zero hs
  · simp only [notMem_support_iff] at h
    rw [h]
    apply zero_le
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
simp :
  LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
⊢ LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) f : ℕ)
have pos : ∀ (h : s ∈ f.support),
  LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
Tactic: classical
  simp only [weight_apply, Finsupp.sum]
  by_cases h : s ∈ f.support
  · rw [Finset.sum_eq_add_sum_diff_singleton_of_mem h]
    refine le_trans ?_ (Nat.le_add_right _ _)
    apply Nat.le_mul_of_pos_right
    exact Nat.zero_lt_of_ne_zero hs
  · simp only [notMem_support_iff] at h
    rw [h]
    apply zero_le
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
simp :
  LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
pos :
  ∀ (h : s ∈ f.support),
    LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
⊢ LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) f : ℕ)
have neg : ∀ (h : s ∉ f.support),
  LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)
Tactic: classical
  simp only [weight_apply, Finsupp.sum]
  by_cases h : s ∈ f.support
  · rw [Finset.sum_eq_add_sum_diff_singleton_of_mem h]
    refine le_trans ?_ (Nat.le_add_right _ _)
    apply Nat.le_mul_of_pos_right
    exact Nat.zero_lt_of_ne_zero hs
  · simp only [notMem_support_iff] at h
    rw [h]
    apply zero_le
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : Ne (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ w s ≤ (weight w : (a : σ →₀ ℕ) → M) f
have simp : w s ≤ ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
Tactic: simp only [weight_apply, Finsupp.sum]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : Ne (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ w s ≤ ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
have trans : w s ≤ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s)
Tactic: trans f s • w s
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : Ne (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
trans : w s ≤ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s)
⊢ w s ≤ ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
have trans₁ : HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) ≤
  ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
Tactic: trans f s • w s
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : Ne (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ w s ≤ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s)
have apply : LE.le (α := ℕ) (1 : ℕ) ((f : (a : σ) → ℕ) s : ℕ)
Tactic: apply le_smul_of_one_le_left (hw s)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (hypothesis)
Goal:
σ : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : Ne (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) ≤
    ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
have hs₁ : s ∈ f.support
Tactic: rw [← Finsupp.mem_support_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : s ∈ f.support
⊢ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) ≤
    ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
have rw : HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) ≤
  HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) +
    ∑ x ∈ f.support \ {s}, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
Tactic: rw [Finset.sum_eq_add_sum_diff_singleton_of_mem hs]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : Ne (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ w s ≤ (weight w : (a : σ →₀ ℕ) → M) f
have simp : w s ≤ ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
Tactic: classical
  simp only [weight_apply, Finsupp.sum]
  trans f s • w s
  · apply le_smul_of_one_le_left (hw s)
    exact Nat.one_le_iff_ne_zero.mpr hs
  · rw [← Finsupp.mem_support_iff] at hs
    rw [Finset.sum_eq_add_sum_diff_singleton_of_mem hs]
    exact le_add_of_nonneg_right <| Finset.sum_nonneg <|
      fun i _ ↦ nsmul_nonneg (hw i) (f i)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : Ne (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
simp : w s ≤ ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
⊢ w s ≤ (weight w : (a : σ →₀ ℕ) → M) f
have simp₁ : w s ≤ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s)
Tactic: classical
  simp only [weight_apply, Finsupp.sum]
  trans f s • w s
  · apply le_smul_of_one_le_left (hw s)
    exact Nat.one_le_iff_ne_zero.mpr hs
  · rw [← Finsupp.mem_support_iff] at hs
    rw [Finset.sum_eq_add_sum_diff_singleton_of_mem hs]
    exact le_add_of_nonneg_right <| Finset.sum_nonneg <|
      fun i _ ↦ nsmul_nonneg (hw i) (f i)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : Ne (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
simp : w s ≤ ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
simp₁ : w s ≤ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s)
⊢ w s ≤ (weight w : (a : σ →₀ ℕ) → M) f
have simp₂ : HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) ≤
  ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
Tactic: classical
  simp only [weight_apply, Finsupp.sum]
  trans f s • w s
  · apply le_smul_of_one_le_left (hw s)
    exact Nat.one_le_iff_ne_zero.mpr hs
  · rw [← Finsupp.mem_support_iff] at hs
    rw [Finset.sum_eq_add_sum_diff_singleton_of_mem hs]
    exact le_add_of_nonneg_right <| Finset.sum_nonneg <|
      fun i _ ↦ nsmul_nonneg (hw i) (f i)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : CanonicallyOrderedAdd M
w : σ → M
inst_4 : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M) ↔ f = 0
have mp : Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M) → f = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : CanonicallyOrderedAdd M
w : σ → M
inst_4 : NonTorsionWeight ℕ w
f : σ →₀ ℕ
mp : Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M) → f = 0
⊢ Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M) ↔ f = 0
have mpr : f = 0 → Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : CanonicallyOrderedAdd M
w : σ → M
inst_4 : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M)
⊢ f = 0
have mp : ∀ (s : σ), Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) ((0 : (a : σ) → ℕ) s : ℕ)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : CanonicallyOrderedAdd M
w : σ → M
inst_4 : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M)
s : σ
⊢ Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
have mp : ∀ (hs : ¬Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)), False
Tactic: by_contra hs
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : CanonicallyOrderedAdd M
w : σ → M
inst_4 : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M)
s : σ
hs : ¬Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ False
have mp : w s = 0
Tactic: apply NonTorsionWeight.ne_zero ℕ w s
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : CanonicallyOrderedAdd M
w : σ → M
inst_4 : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M)
s : σ
hs : ¬Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ w s = 0
have mp : w s ≤ (weight w : (a : σ →₀ ℕ) → M) f
Tactic: rw [← nonpos_iff_eq_zero, ← h]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : CanonicallyOrderedAdd M
w : σ → M
inst_4 : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : f = 0
⊢ Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M)
have mpr : Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) 0 : M) (0 : M)
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : CanonicallyOrderedAdd M
w : σ → M
inst_4 : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : f = 0
mpr : Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) 0 : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M)
have mpr₁ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : CanonicallyOrderedAdd M
w : σ → M
inst_4 : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M) ↔ f = 0
have mp : Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M) → f = 0
Tactic: classical
  constructor
  · intro h
    ext s
    simp only [Finsupp.coe_zero, Pi.zero_apply]
    by_contra hs
    apply NonTorsionWeight.ne_zero ℕ w s
    rw [← nonpos_iff_eq_zero, ← h]
    exact le_weight_of_ne_zero' w hs
  · intro h
    rw [h, map_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : CanonicallyOrderedAdd M
w : σ → M
inst_4 : NonTorsionWeight ℕ w
f : σ →₀ ℕ
mp : Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M) → f = 0
⊢ Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M) ↔ f = 0
have mpr : f = 0 → Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M)
Tactic: classical
  constructor
  · intro h
    ext s
    simp only [Finsupp.coe_zero, Pi.zero_apply]
    by_contra hs
    apply NonTorsionWeight.ne_zero ℕ w s
    rw [← nonpos_iff_eq_zero, ← h]
    exact le_weight_of_ne_zero' w hs
  · intro h
    rw [h, map_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (hypothesis)
Goal:
σ : Type u_1
inst : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}
have hfg : let fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
  @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n));
fg = @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))
Tactic: set fg := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n)) with hfg
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
inst : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
  @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))
hfg :
  fg =
    @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}
have suffices : {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n} ⊆
  (↑(Finset.image (fun (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ uv.1) fg) : Set (σ →₀ ℕ))
Tactic: suffices {d : σ →₀ ℕ | weight w d ≤ n} ⊆ ↑(fg.image fun uv => uv.fst) by
    exact Set.Finite.subset (Finset.finite_toSet _) this
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
inst : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
  @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))
hfg :
  fg =
    @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))
d : σ →₀ ℕ
hd : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n} d
⊢ d ∈
    (↑(Finset.image (α := (σ →₀ ℕ) × (σ →₀ ℕ)) (fun (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ uv.1)
          (@Finset.antidiagonal _ instAddMonoid _
              ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)) :
            Finset ((σ →₀ ℕ) × (σ →₀ ℕ)))) :
      Set (σ →₀ ℕ))
have simp : ∃ (x : σ →₀ ℕ), d + x = (Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)
Tactic: simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe,
    Finset.mem_antidiagonal, Prod.exists, exists_and_right, exists_eq_right]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
inst : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
  @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))
hfg :
  fg =
    @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))
d : σ →₀ ℕ
hd : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n} d
⊢ ∃ (x : σ →₀ ℕ), d + x = (Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)
have h : d + HSub.hSub (α := σ →₀ ℕ) ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) d =
  (Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)
Tactic: use Finsupp.equivFunOnFinite.symm (Function.const σ n) - d
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
inst : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
  @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))
hfg :
  fg =
    @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))
d : σ →₀ ℕ
hd : Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n} d
⊢ d + HSub.hSub (α := σ →₀ ℕ) ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) d =
    (Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)
have h : ∀ (x : σ),
  Eq (α := ℕ)
    ((d +
            HSub.hSub (α := σ →₀ ℕ) ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ)
              d :
          (a : σ) → ℕ)
        x :
      ℕ)
    ((((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) : (a : σ) → ℕ) x : ℕ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (hypothesis)
Goal:
σ : Type u_1
inst : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
  @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))
hfg :
  fg =
    @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n
x : σ
⊢ Eq (α := ℕ)
    ((d +
            HSub.hSub (α := σ →₀ ℕ) ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ)
              d :
          (a : σ) → ℕ)
        x :
      ℕ)
    ((((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) : (a : σ) → ℕ) x : ℕ)
have hd₁ : (d : (a : σ) → ℕ) x ≤ n
Tactic: grw [← le_weight _ (hw x)] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
inst : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
set set₁ : Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}
have set₂ : let fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
  @Finset.antidiagonal _ instAddMonoid _ ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n));
∀
  (hfg :
    fg =
      @Finset.antidiagonal _ instAddMonoid _
        ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n))),
  Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}
Tactic: classical
  set fg := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n)) with hfg
  suffices {d : σ →₀ ℕ | weight w d ≤ n} ⊆ ↑(fg.image fun uv => uv.fst) by
    exact Set.Finite.subset (Finset.finite_toSet _) this
  intro d hd
  rw [hfg]
  simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe,
    Finset.mem_antidiagonal, Prod.exists, exists_and_right, exists_eq_right]
  use Finsupp.equivFunOnFinite.symm (Function.const σ n) - d
  ext x
  dsimp at hd
  grw [← le_weight _ (hw x)] at hd
  simp [*]