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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ w ≤ w + k • 1 ∧ w + k • 1 ≤ w
Tactic:
simp only [dom_iff, f_eq_on_shift, le_rfl, and_self]
State after:
no goals