awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
this :
  Eq.{u_5 + 1} (α := N)
    ((single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n : (a : (i : ι) × η i) → N)
        (Sigma.mk (β := fun (i : ι) ↦ η i) j b) :
      N)
    (0 : N)
⊢ Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)

Tactic:
simp [split_apply, dif_neg h, this]

Premises used: dif_neg, Finsupp.split_apply
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
neg :
  Eq.{u_5 + 1} (α := N)
    ((single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n : (a : (i : ι) × η i) → N)
        (Sigma.mk (β := fun (i : ι) ↦ η i) j b) :
      N)
    (0 : N)
⊢ Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)

Tactic:
suffices Finsupp.single (⟨i, a⟩ : Σ i, η i) n ⟨j, b⟩ = 0 by simp [split_apply, dif_neg h, this]
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ Sigma.mk (β := fun (i : ι) ↦ η i) i a ≠ Sigma.mk (β := fun (i : ι) ↦ η i) j b

Tactic:
simp [h]
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ Sigma.mk (β := fun (i : ι) ↦ η i) i a ≠ Sigma.mk (β := fun (i : ι) ↦ η i) j b

Tactic:
have H : (⟨i, a⟩ : Σ i, η i) ≠ ⟨j, b⟩ := by simp [h]
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : Sigma.mk (β := fun (i : ι) ↦ η i) i a ≠ Sigma.mk (β := fun (i : ι) ↦ η i) j b
neg : (if Sigma.mk (β := fun (i : ι) ↦ η i) i a = Sigma.mk (β := fun (i : ι) ↦ η i) j b then n else 0) = 0
neg₁ neg₂ : Eq.{u_5 + 1} (α := N) 0 0
⊢ Eq.{u_5 + 1} (α := N)
    ((single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n : (a : (i : ι) × η i) → N)
        (Sigma.mk (β := fun (i : ι) ↦ η i) j b) :
      N)
    (0 : N)

Tactic:
rw [Finsupp.single_apply, if_neg H]

Premises used: Finsupp.single_apply, if_neg
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : Sigma.mk (β := fun (i : ι) ↦ η i) i a ≠ Sigma.mk (β := fun (i : ι) ↦ η i) j b
neg : (if Sigma.mk (β := fun (i : ι) ↦ η i) i a = Sigma.mk (β := fun (i : ι) ↦ η i) j b then n else 0) = 0
neg₁ neg₂ : Eq.{u_5 + 1} (α := N) 0 0
⊢ Eq.{u_5 + 1} (α := N)
    ((single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n : (a : (i : ι) × η i) → N)
        (Sigma.mk (β := fun (i : ι) ↦ η i) j b) :
      N)
    (0 : N)

Tactic:
classical rw [Finsupp.single_apply, if_neg H]

Premises used: Finsupp.single_apply, if_neg
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : AddZeroClass N
f g : (i : ι) × η i →₀ N
h :
  ∀ (i : ι) (a : η i),
    Eq.{u_5 + 1} (α := N)
      (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) (f + g) :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
                (a : ι) → η a →₀ N)
              i :
            (a : η i) → N)
          a :
        N)
      (((HAdd.hAdd (α := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) (β := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
                  ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
                    Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
                  ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) g :
                    Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
                (a : ι) → η a →₀ N)
              i :
            (a : η i) → N)
          a :
        N)
⊢ (sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) (f + g) =
    HAdd.hAdd (α := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) (β := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
      ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
        Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
      ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) g :
        Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : AddZeroClass N
f g : (i : ι) × η i →₀ N
i : ι
a : η i
⊢ Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) (f + g) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        a :
      N)
    (((HAdd.hAdd (α := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) (β := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
                ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
                ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) g :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        a :
      N)

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
R : Type u_6
inst : Monoid R
inst_1 : AddMonoid N
inst_2 : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
h :
  ∀ (i : ι) (a : η i),
    Eq.{u_5 + 1} (α := N)
      (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) (r • f) :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
                (a : ι) → η a →₀ N)
              i :
            (a : η i) → N)
          a :
        N)
      (((HSMul.hSMul (β := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) r
                  ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
                    Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
                (a : ι) → η a →₀ N)
              i :
            (a : η i) → N)
          a :
        N)
⊢ (sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) (r • f) =
    HSMul.hSMul (β := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) r
      ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
        Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.ToDFinsupp
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
R : Type u_6
inst : Monoid R
inst_1 : AddMonoid N
inst_2 : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
i : ι
a : η i
⊢ Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) (r • f) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        a :
      N)
    (((HSMul.hSMul (β := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) r
                ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        a :
      N)

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : σ →₀ R
⊢ Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ R) → M) f : M) (f.sum fun (i : σ) (c : R) ↦ c • w i : M)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq σ
s : σ
c : M
f : σ →₀ R
⊢ (weight (Pi.single (M := fun (a : σ) ↦ M) s c) : (a : σ →₀ R) → M) f =
    HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((f : (a : σ) → R) s : R) c

Tactic:
linearCombination_single_index σ M R c s f

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finsupp.linearCombination_single_index, Finset.sum
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
R : Type u_3
inst : Semiring R
inst_1 : DecidableEq σ
s : σ
f : σ →₀ R
rw : HSMul.hSMul (α := R) (β := R) ((f : (a : σ) → R) s : R) 1 = (f : (a : σ) → R) s
rw₁ : HMul.hMul (α := R) (β := R) ((f : (a : σ) → R) s : R) (1 : R) = (f : (a : σ) → R) s
rw₂ rw₃ : Eq.{u_3 + 1} (α := R) ((f : (a : σ) → R) s : R) ((f : (a : σ) → R) s : R)
⊢ Eq.{u_3 + 1} (α := R) ((weight (Pi.single (M := fun (a : σ) ↦ R) s 1) : (a : σ →₀ R) → R) f : R)
    ((f : (a : σ) → R) s : R)

Tactic:
rw [weight_single_index, smul_eq_mul, mul_one]

Premises used: Finsupp.weight_single_index, smul_eq_mul, mul_one
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : σ
r : R
⊢ (weight w : (a : σ →₀ R) → M) (single s r) = r • w s

Tactic:
Finsupp.linearCombination_single _ _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finsupp.linearCombination_single, Finset.sum
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : n • w s = 0
⊢ ¬w s = 0 → n = 0

Tactic:
rw [smul_eq_zero, or_iff_not_imp_right] at h

Premises used: Classical.or_iff_not_imp_right, smul_eq_zero
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : ¬w s = 0 → n = 0
⊢ n = 0

Tactic:
h (hw s)
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : ¬w s = 0 → n = 0
⊢ n = 0

Tactic:
exact h (hw s)
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : NonTorsionWeight R w
s : σ
h : w s = 0
⊢ HSMul.hSMul.{u_3, u_2, u_2} (α := R) 1 (w s) = 0

Tactic:
rw [← one_smul R (w s)] at h

Premises used: one_smul
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : NonTorsionWeight R w
s : σ
h : HSMul.hSMul.{u_3, u_2, u_2} (α := R) 1 (w s) = 0
apply : Eq.{u_3 + 1} (α := R) 1 0
⊢ False

Tactic:
apply zero_ne_one.symm (α := R)

Premises used: zero_ne_one, Ne.symm
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : NonTorsionWeight R w
s : σ
h : HSMul.hSMul.{u_3, u_2, u_2} (α := R) 1 (w s) = 0
⊢ Eq.{u_3 + 1} (α := R) 1 0

Tactic:
NonTorsionWeight.eq_zero_of_smul_eq_zero h

Premises used: Finsupp.NonTorsionWeight.eq_zero_of_smul_eq_zero
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : NonTorsionWeight R w
s : σ
h : HSMul.hSMul.{u_3, u_2, u_2} (α := R) 1 (w s) = 0
⊢ Eq.{u_3 + 1} (α := R) 1 0

Tactic:
exact NonTorsionWeight.eq_zero_of_smul_eq_zero h

Premises used: Finsupp.NonTorsionWeight.eq_zero_of_smul_eq_zero
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
w : σ → M
inst : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : Ne (α := ℕ) ((f : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
rw : (f - single i 1 + single i 1).sum fun (i : σ) (c : ℕ) ↦ c • w i
| ((weight w : (a : σ →₀ ℕ) → M) f : M)

Tactic:
rw [← sub_add_single_one_cancel hi, weight_apply]

Premises used: Finsupp.sub_add_single_one_cancel, Finsupp.weight_apply
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
w : σ → M
inst : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : Ne (α := ℕ) ((f : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
conv_rhs :
  HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (f - single i 1) : M) (w i) =
    (f - single i 1 + single i 1).sum fun (i : σ) (c : ℕ) ↦ c • w i
⊢ HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (f - single i 1) : M) (w i) = (weight w : (a : σ →₀ ℕ) → M) f

Tactic:
conv_rhs => rw [← sub_add_single_one_cancel hi, weight_apply]

Premises used: Finsupp.sub_add_single_one_cancel, Finsupp.weight_apply
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
w : σ → M
inst : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : Ne (α := ℕ) ((f : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
rw : HSMul.hSMul (α := ℕ) 0 (w i) = 0
h_zero : ∀ (a : σ), HSMul.hSMul (α := ℕ) 0 (w a) = 0
h_add : ∀ (a : σ) (b₁ b₂ : ℕ), (b₁ + b₂) • w a = b₁ • w a + b₂ • w a
⊢ HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (f - single i 1) : M) (w i) =
    (f - single i 1 + single i 1).sum fun (i : σ) (c : ℕ) ↦ c • w i

Tactic:
rw [sum_add_index', sum_single_index, one_smul, weight_apply]

Premises used: Finsupp.sum_single_index, Finsupp.sum_add_index', one_smul, Finsupp.weight_apply
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
w : σ → M
inst : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : Ne (α := ℕ) ((f : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ HSMul.hSMul (α := ℕ) 0 (w i) = 0

Tactic:
zero_smul ..

Premises used: zero_smul
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
w : σ → M
inst : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : Ne (α := ℕ) ((f : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ ∀ (a : σ), HSMul.hSMul (α := ℕ) 0 (w a) = 0

Tactic:
fun _ ↦ zero_smul ..

Premises used: zero_smul, Nat
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
w : σ → M
inst : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : Ne (α := ℕ) ((f : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ ∀ (a : σ) (b₁ b₂ : ℕ), (b₁ + b₂) • w a = b₁ • w a + b₂ • w a

Tactic:
fun _ _ _ ↦ add_smul ..

Premises used: add_smul
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
M : Type u_2
w : σ → M
inst : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : Ne (α := ℕ) ((f : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ HSMul.hSMul (α := ℕ) 0 (w i) = 0

Tactic:
exacts [zero_smul .., fun _ ↦ zero_smul .., fun _ _ _ ↦ add_smul ..]

Premises used: zero_smul, add_smul
-- Module: Mathlib.Data.Finsupp.Weight
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 : ℕ)

Tactic:
simp only [weight_apply, Finsupp.sum]

Premises used: Finsupp.sum, Finsupp.weight_apply
-- Module: Mathlib.Data.Finsupp.Weight
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) : ℕ)
neg :
  ∀ (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) : ℕ)

Tactic:
by_cases h : s ∈ f.support

Premises used: Finsupp.support
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
pos :
  (f : (a : σ) → ℕ) s ≤
    HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) +
      ∑ x ∈ f.support \ {s}, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
⊢ LE.le (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x) : ℕ)

Tactic:
rw [Finset.sum_eq_add_sum_diff_singleton_of_mem h]

Premises used: Finset.sum_eq_add_sum_diff_singleton_of_mem
-- Module: Mathlib.Data.Finsupp.Weight
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)

Tactic:
le_trans ?_ (Nat.le_add_right _ _)

Premises used: Nat.le_add_right, le_trans
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
pos : (f : (a : σ) → ℕ) s ≤ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s)
⊢ (f : (a : σ) → ℕ) s ≤
    HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) +
      ∑ x ∈ f.support \ {s}, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)

Tactic:
refine le_trans ?_ (Nat.le_add_right _ _)

Premises used: Nat.le_add_right, le_trans
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
pos : 0 < w s
⊢ (f : (a : σ) → ℕ) s ≤ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s)

Tactic:
apply Nat.le_mul_of_pos_right

Premises used: Nat.le_mul_of_pos_right
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ 0 < w s

Tactic:
Nat.zero_lt_of_ne_zero hs

Premises used: Nat.zero_lt_of_ne_zero
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ 0 < w s

Tactic:
exact Nat.zero_lt_of_ne_zero hs

Premises used: Nat.zero_lt_of_ne_zero
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∉ f.support
⊢ Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)

Tactic:
simp only [notMem_support_iff] at h

Premises used: Finsupp.notMem_support_iff
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
neg : LE.le (α := ℕ) 0 (∑ 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) : ℕ)

Tactic:
rw [h]
-- Module: Mathlib.Data.Finsupp.Weight
Goal:
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : Eq (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ LE.le (α := ℕ) 0 (∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x))

Tactic:
apply zero_le

Premises used: zero_le
-- Module: Mathlib.Data.Finsupp.Weight
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) : ℕ)
neg neg₁ :
  ∀ (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 : ℕ)

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

Premises used: zero_le, Finsupp.notMem_support_iff, Nat.le_mul_of_pos_right, Nat.le_add_right, Finsupp.sum, Finsupp.support, Nat.zero_lt_of_ne_zero, Finsupp.weight_apply, le_trans
-- 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)
⊢ w s ≤ (weight w : (a : σ →₀ ℕ) → M) f

Tactic:
simp only [weight_apply, Finsupp.sum]

Premises used: Finsupp.sum, Finsupp.weight_apply
-- 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 : ℕ)
trans : w s ≤ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s)
trans₁ :
  HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) ≤
    ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)
⊢ w s ≤ ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)

Tactic:
trans f s • w s

Premises used: 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 : ℕ)
apply : LE.le (α := ℕ) (1 : ℕ) ((f : (a : σ) → ℕ) s : ℕ)
⊢ w s ≤ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s)

Tactic:
apply le_smul_of_one_le_left (hw s)

Premises used: le_smul_of_one_le_left
-- 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 : ℕ)
⊢ LE.le (α := ℕ) (1 : ℕ) ((f : (a : σ) → ℕ) s : ℕ)

Tactic:
Nat.one_le_iff_ne_zero.mpr hs

Premises used: Iff.mpr, Nat.one_le_iff_ne_zero
-- 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 : ℕ)
⊢ LE.le (α := ℕ) (1 : ℕ) ((f : (a : σ) → ℕ) s : ℕ)

Tactic:
exact Nat.one_le_iff_ne_zero.mpr hs

Premises used: Iff.mpr, Nat.one_le_iff_ne_zero
-- 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 : ℕ)
⊢ s ∈ f.support

Tactic:
rw [← Finsupp.mem_support_iff] at hs

Premises used: Finsupp.mem_support_iff
-- 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
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)
⊢ HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) s : ℕ) (w s) ≤
    ∑ x ∈ f.support, HSMul.hSMul (α := ℕ) ((f : (a : σ) → ℕ) x : ℕ) (w x)

Tactic:
rw [Finset.sum_eq_add_sum_diff_singleton_of_mem hs]

Premises used: Finset.sum_eq_add_sum_diff_singleton_of_mem