Theorem: Weight.trunc_zero (Weights/Uniqueness.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : w 0 = 0
⊢ trunc w 0 = 0
Tactic:
simp only [trunc_apply, Nat.min_eq_zero_iff] at h ⊢
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : w 0 = 0
⊢ w 0 = 0 ∨ E w = 0

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : w 0 = 0
⊢ w 0 = 0 ∨ E w = 0
Tactic:
exact Or.inl h
State after:
no goals