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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : Monotone w
⊢ Monotone (trunc w)
Tactic:
intro i j hij
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : Monotone w
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ trunc w i ≤ trunc w j

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : Monotone w
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ trunc w i ≤ trunc w j
Tactic:
simp only [trunc_apply, min_le_iff, le_min_iff, le_refl, and_true, or_true]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : Monotone w
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ w i ≤ w j ∨ E w ≤ w j

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : Monotone w
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ w i ≤ w j ∨ E w ≤ w j
Tactic:
exact Or.inl (h hij)
State after:
no goals