awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Weight
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) ≤
    HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) +
      ∑ x ∈ f.support \ {s}, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)

Tactic:
le_add_of_nonneg_right <| Finset.sum_nonneg <|
      fun i _ ↦ nsmul_nonneg (hw i) (f i)

Premises used: Finset.sum_nonneg, nsmul_nonneg, le_add_of_nonneg_right, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Weight
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) ≤
    HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) +
      ∑ x ∈ f.support \ {s}, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)

Tactic:
exact le_add_of_nonneg_right <| Finset.sum_nonneg <|
      fun i _ ↦ nsmul_nonneg (hw i) (f i)

Premises used: Finset.sum_nonneg, nsmul_nonneg, le_add_of_nonneg_right, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Weight
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)
simp₂ simp₃ :
  HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) ≤
    ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
⊢ w s ≤ (weight w : (a : σ →₀ ℕ) → M) f

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)

Premises used: Iff.mpr, Finsupp.mem_support_iff, Finsupp.sum, Finset.sum_nonneg, nsmul_nonneg, le_smul_of_one_le_left, le_add_of_nonneg_right, Nat.one_le_iff_ne_zero, DFunLike.coe, Finsupp.weight_apply, Finset.sum_eq_add_sum_diff_singleton_of_mem
-- Module: Mathlib.Data.Finsupp.Weight
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
s : σ
f : σ →₀ ℕ
hs : Ne (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ w s ≤ (weight w : (a : σ →₀ ℕ) → M) f

Tactic:
le_weight_of_ne_zero (fun _ ↦ zero_le) hs

Premises used: zero_le, Finsupp.le_weight_of_ne_zero
-- Module: Mathlib.Data.Finsupp.Weight
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
mpr : f = 0 → Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M) ↔ f = 0

Tactic:
constructor
-- Module: Mathlib.Data.Finsupp.Weight
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)
mp : ∀ (s : σ), Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) ((0 : (a : σ) → ℕ) s : ℕ)
⊢ f = 0

Tactic:
ext s
-- Module: Mathlib.Data.Finsupp.Weight
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 : σ
mp : ∀ (hs : ¬Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)), False
⊢ Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)

Tactic:
by_contra hs
-- Module: Mathlib.Data.Finsupp.Weight
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 : ℕ)
mp : w s = 0
⊢ False

Tactic:
apply NonTorsionWeight.ne_zero ℕ w s

Premises used: Nat, Finsupp.NonTorsionWeight.ne_zero
-- Module: Mathlib.Data.Finsupp.Weight
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 : ℕ)
mp : w s ≤ (weight w : (a : σ →₀ ℕ) → M) f
⊢ w s = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← h]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.Data.Finsupp.Weight
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 ≤ (weight w : (a : σ →₀ ℕ) → M) f

Tactic:
le_weight_of_ne_zero' w hs

Premises used: Finsupp.le_weight_of_ne_zero'
-- Module: Mathlib.Data.Finsupp.Weight
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 ≤ (weight w : (a : σ →₀ ℕ) → M) f

Tactic:
exact le_weight_of_ne_zero' w hs

Premises used: Finsupp.le_weight_of_ne_zero'
-- Module: Mathlib.Data.Finsupp.Weight
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)
mpr₁ mpr₂ : Eq.{u_4 + 1} (α := M) 0 0
⊢ Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M)

Tactic:
rw [h, map_zero]

Premises used: map_zero
-- Module: Mathlib.Data.Finsupp.Weight
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
mpr mpr₁ : f = 0 → Eq.{u_4 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) f : M) (0 : M)
⊢ 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]

Premises used: Pi.zero_apply, map_zero, Finsupp.coe_zero, nonpos_iff_eq_zero
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
inst : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
⊢ 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

Premises used: Finsupp.equivFunOnFinite, Function.const, Equiv.symm, DFunLike.coe, Finset.HasAntidiagonal.antidiagonal
-- Module: Mathlib.Data.Finsupp.Weight
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))
this :
  {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n} ⊆
    (↑(Finset.image (fun (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ uv.1) fg) : Set (σ →₀ ℕ))
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}

Tactic:
Set.Finite.subset (Finset.finite_toSet _) this

Premises used: Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Data.Finsupp.Weight
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))
this :
  {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n} ⊆
    (↑(Finset.image (fun (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ uv.1) fg) : Set (σ →₀ ℕ))
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}

Tactic:
exact Set.Finite.subset (Finset.finite_toSet _) this

Premises used: Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Data.Finsupp.Weight
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))
suffices :
  {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n} ⊆
    (↑(Finset.image (fun (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ uv.1) fg) : Set (σ →₀ ℕ))
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d ≤ n}

Tactic:
suffices {d : σ →₀ ℕ | weight w d ≤ n} ⊆ ↑(fg.image fun uv => uv.fst) by
    exact Set.Finite.subset (Finset.finite_toSet _) this
-- Module: Mathlib.Data.Finsupp.Weight
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
rw :
  d ∈
    (↑(Finset.image (α := (σ →₀ ℕ) × (σ →₀ ℕ)) (fun (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ uv.1)
          (@Finset.antidiagonal _ instAddMonoid _
              ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)) :
            Finset ((σ →₀ ℕ) × (σ →₀ ℕ)))) :
      Set (σ →₀ ℕ))
⊢ d ∈ (↑(Finset.image (fun (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ uv.1) fg) : Set (σ →₀ ℕ))

Tactic:
rw [hfg]
-- Module: Mathlib.Data.Finsupp.Weight
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
simp : ∃ (x : σ →₀ ℕ), d + x = (Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)
⊢ d ∈
    (↑(Finset.image (α := (σ →₀ ℕ) × (σ →₀ ℕ)) (fun (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ uv.1)
          (@Finset.antidiagonal _ instAddMonoid _
              ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)) :
            Finset ((σ →₀ ℕ) × (σ →₀ ℕ)))) :
      Set (σ →₀ ℕ))

Tactic:
simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe,
    Finset.mem_antidiagonal, Prod.exists, exists_and_right, exists_eq_right]

Premises used: Set.mem_image, Finset.coe_image, exists_eq_right, exists_and_right, Finset.HasAntidiagonal.mem_antidiagonal, Prod.exists, Finset.mem_coe
-- Module: Mathlib.Data.Finsupp.Weight
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
h :
  d + HSub.hSub (α := σ →₀ ℕ) ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) d =
    (Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)
⊢ ∃ (x : σ →₀ ℕ), d + x = (Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)

Tactic:
use Finsupp.equivFunOnFinite.symm (Function.const σ n) - d

Premises used: Finsupp.equivFunOnFinite, Function.const, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Weight
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
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 : ℕ)
⊢ d + HSub.hSub (α := σ →₀ ℕ) ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) d =
    (Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n)

Tactic:
ext x
-- Module: Mathlib.Data.Finsupp.Weight
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 : σ
⊢ (d : (a : σ) → ℕ) x ≤ n

Tactic:
grw [← le_weight _ (hw x)] at hd

Premises used: Finsupp.le_weight
-- Module: Mathlib.Data.Finsupp.Weight
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 : σ →₀ ℕ
x : σ
hd : (d : (a : σ) → ℕ) x ≤ n
⊢ Eq (α := ℕ)
    ((d +
            HSub.hSub (α := σ →₀ ℕ) ((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ)
              d :
          (a : σ) → ℕ)
        x :
      ℕ)
    ((((Equiv.symm equivFunOnFinite : (a : σ → ℕ) → σ →₀ ℕ) (Function.const σ n) : σ →₀ ℕ) : (a : σ) → ℕ) x : ℕ)

Tactic:
simp [*]
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
R_1 : Type u_3
inst : Semiring R_1
w : σ → M
R : Type u_4
inst_1 : AddCommMonoid R
⊢ Eq.{u_4 + 1} (α := R) (∑ i ∈ support.{u_1, u_4} (M := R) 0, (0 : (a : σ) → R) i) 0

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_4
inst : AddCommMonoid R
d : σ →₀ R
⊢ Eq.{u_4 + 1} (α := R) ((degree : (a : σ →₀ R) → R) d : R) (∑ i ∈ d.support, (d : (a : σ) → R) i : R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.sum, rfl
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_4
inst : AddCommMonoid R
inst_1 : Fintype σ
f : σ →₀ R
h : f.support ⊆ Finset.univ
hf :
  ∀ (x : σ),
    Membership.mem (γ := Finset σ) Finset.univ x →
      x ∉ f.support → Eq.{u_4 + 1} (α := R) ((f : (a : σ) → R) x : R) (0 : R)
⊢ Eq.{u_4 + 1} (α := R) ((degree : (a : σ →₀ R) → R) f : R) (∑ i : σ, (f : (a : σ) → R) i : R)

Tactic:
rw [degree_apply, Finset.sum_subset]

Premises used: Finsupp.degree_apply, Finset.sum_subset
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_4
inst : AddCommMonoid R
inst_1 : Fintype σ
f : σ →₀ R
⊢ f.support ⊆ Finset.univ

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_4
inst : AddCommMonoid R
inst_1 : Fintype σ
f : σ →₀ R
⊢ ∀ (x : σ),
    Membership.mem (γ := Finset σ) Finset.univ x →
      x ∉ f.support → Eq.{u_4 + 1} (α := R) ((f : (a : σ) → R) x : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_4
inst : AddCommMonoid R
a : σ
r : R
⊢ (degree : (a : σ →₀ R) → R) (single a r) = r

Tactic:
Finsupp.sum_single_index (h := fun _ => id) rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum_single_index, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_5
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
d : σ →₀ R
⊢ Eq.{u_5 + 1} (α := R) ((degree : (a : σ →₀ R) → R) d : R) (0 : R) ↔ d = 0

Tactic:
simp only [degree_apply, Finset.sum_eq_zero_iff, mem_support_iff, ne_eq, _root_.not_imp_self,
    DFunLike.ext_iff, coe_zero, Pi.zero_apply]

Premises used: Finsupp.mem_support_iff, Finsupp.degree_apply, Pi.zero_apply, DFunLike.ext_iff, ne_eq, not_imp_self, Finset.sum_eq_zero_iff, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_5
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
pos : ∀ (h : s ∈ f.support), LE.le.{u_5} (α := R) ((f : (a : σ) → R) s : R) ((degree : (a : σ →₀ R) → R) f : R)
neg : ∀ (h : s ∉ f.support), LE.le.{u_5} (α := R) ((f : (a : σ) → R) s : R) ((degree : (a : σ →₀ R) → R) f : R)
⊢ LE.le.{u_5} (α := R) ((f : (a : σ) → R) s : R) ((degree : (a : σ →₀ R) → R) f : R)

Tactic:
by_cases h : s ∈ f.support

Premises used: Finsupp.support
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_5
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∈ f.support
⊢ LE.le.{u_5} (α := R) ((f : (a : σ) → R) s : R) ((degree : (a : σ →₀ R) → R) f : R)

Tactic:
Finset.single_le_sum_of_canonicallyOrdered h

Premises used: Multiset.sum, Multiset.foldr, Finset.single_le_sum_of_canonicallyOrdered, Finset.sum
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_5
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∈ f.support
⊢ LE.le.{u_5} (α := R) ((f : (a : σ) → R) s : R) ((degree : (a : σ →₀ R) → R) f : R)

Tactic:
exact Finset.single_le_sum_of_canonicallyOrdered h

Premises used: Finset.single_le_sum_of_canonicallyOrdered
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_5
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∉ f.support
⊢ Eq.{u_5 + 1} (α := R) ((f : (a : σ) → R) s : R) (0 : R)

Tactic:
simp only [notMem_support_iff] at h

Premises used: Finsupp.notMem_support_iff
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_5
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : Eq.{u_5 + 1} (α := R) ((f : (a : σ) → R) s : R) (0 : R)
⊢ LE.le.{u_5} (α := R) ((f : (a : σ) → R) s : R) ((degree : (a : σ →₀ R) → R) f : R)

Tactic:
simp only [h, zero_le]

Premises used: zero_le
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_5
inst : Semiring R
H :
  ∀ (d : σ) (x : R),
    Eq (α := R) ((AddMonoidHom.comp degree (singleAddHom d) : (a : R) → R) x : R)
      ((AddMonoidHom.comp (N := σ →₀ R) (weight fun (x : σ) ↦ 1) (singleAddHom d) : (a : R) → R) x : R)
⊢ Eq (α := (σ →₀ R) →+ R) degree (weight fun (x : σ) ↦ 1)

Tactic:
ext d
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_5
inst : Semiring R
d : σ
x : R
⊢ Eq (α := R) ((AddMonoidHom.comp degree (singleAddHom d) : (a : R) → R) x : R)
    ((AddMonoidHom.comp (N := σ →₀ R) (weight fun (x : σ) ↦ 1) (singleAddHom d) : (a : R) → R) x : R)

Tactic:
simp [weight_apply, smul_eq_mul, mul_one]

Premises used: smul_eq_mul, mul_one, Finsupp.weight_apply
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
inst : Finite σ
n : ℕ
simp_rw : Set.Finite.{u_1} (α := σ →₀ ℕ) {f : σ →₀ ℕ | (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) f ≤ n}
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f ≤ n}

Tactic:
simp_rw [degree_eq_weight_one]

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
inst : Finite σ
n : ℕ
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {f : σ →₀ ℕ | (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) f ≤ n}

Tactic:
finite_of_nat_weight_le (Function.const σ 1) ?_ n

Premises used: setOf, Finsupp.finite_of_nat_weight_le, Function.const, OfNat.ofNat
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
inst : Finite σ
n : ℕ
refine : ∀ (x : σ), Ne (α := ℕ) (Function.const σ 1 x) 0
⊢ Set.Finite.{u_1} (α := σ →₀ ℕ) {f : σ →₀ ℕ | (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) f ≤ n}

Tactic:
refine finite_of_nat_weight_le (Function.const σ 1) ?_ n

Premises used: Finsupp.finite_of_nat_weight_le, Function.const, OfNat.ofNat
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
inst : Finite σ
n : ℕ
x : σ
⊢ Ne (α := ℕ) (Function.const σ 1 x) 0

Tactic:
simp only [Function.const_apply, ne_eq, one_ne_zero, not_false_eq_true]

Premises used: Function.const_apply, ne_eq, one_ne_zero, not_false_eq_true
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
inst : Finite σ
n : ℕ
⊢ Subset.{u_1} (α := Set (σ →₀ ℕ)) {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}
    {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f ≤ n}

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
⊢ Eq.{max (u_1 + 1) 1} (α := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1)
    {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}

Tactic:
subset_antisymm ?_ ?_

Premises used: subset_antisymm
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
refine_1 :
  Subset.{u_1} (α := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1)
    {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}
refine_2 :
  Subset.{u_1} (α := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}
    (Set.range fun (a : σ) ↦ single a 1)
⊢ Eq.{max (u_1 + 1) 1} (α := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1)
    {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}

Tactic:
refine subset_antisymm ?_ ?_

Premises used: subset_antisymm
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
⊢ Subset.{u_1} (α := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1)
    {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}

Tactic:
simp [Set.range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
p : σ →₀ ℕ
refine_2 :
  ∀ (hp : Eq (α := ℕ) (p.sum fun (a : σ) (k : ℕ) ↦ k) 1),
    Membership.mem (γ := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1) p
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)} p →
    Membership.mem (γ := Set (σ →₀ ℕ)) (Set.range fun (a : σ) ↦ single a 1) p

Tactic:
(hp : p.sum (fun a k ↦ k) = 1)