Theorem: Weight.tw'_sum (Weights/Weights.lean)

State before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
k : Fin (Nat.succ n)
⊢ Weight.sum (tw' n d k) = d
Tactic:
simp only [Weight.sum, tw', ge_iff_le, nsmul_eq_mul, Pi.coe_nat, Nat.cast_tsub, Nat.cast_id,
  Nat.cast_one, Pi.add_apply, Pi.mul_apply, ne_eq, Function.update_apply, zero_apply, mul_ite,
  mul_one, mul_zero, Finset.sum_add_distrib, Finset.sum_ite_eq', Finset.mem_univ, ite_true]
State after:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
k : Fin (Nat.succ n)
⊢ d - 1 + 1 = d

State before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
k : Fin (Nat.succ n)
⊢ d - 1 + 1 = d
Tactic:
exact Nat.sub_add_cancel (Nat.one_le_of_lt (NeZero.pos d))
State after:
no goals