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

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

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