Theorem: Weight.mul_le_pair (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ pair w a
Tactic:
simp [pair]
State after:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ ∑ j : Fin (Nat.succ n), a j * w j

State before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ ∑ j : Fin (Nat.succ n), a j * w j
Tactic:
rw [Finset.sum_eq_add_sum_diff_singleton (Finset.mem_univ k)]
State after:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ a k * w k + ∑ x in Finset.univ \ {k}, a x * w x

State before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ a k * w k + ∑ x in Finset.univ \ {k}, a x * w x
Tactic:
exact Nat.le_add_right _ _
State after:
no goals