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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ trunc w ≤ w
Tactic:
simp_rw [lec_iff, trunc_apply]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ ∀ (j : Fin (Nat.succ n)), min (w j) (E w) ≤ w j

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ ∀ (j : Fin (Nat.succ n)), min (w j) (E w) ≤ w j
Tactic:
exact (fun j ↦ min_le_left _ _)
State after:
no goals