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

State before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∃ j, E w < w j ∧ 0 < a j
⊢ E w ≤ pair (trunc w) a
Tactic:
obtain ⟨j, hj, ha⟩ := h
State after:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
⊢ E w ≤ pair (trunc w) a

State before:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
⊢ E w ≤ pair (trunc w) a
Tactic:
have hm := mul_le_pair w.trunc a j
State after:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
hm : a j * trunc w j ≤ pair (trunc w) a
⊢ E w ≤ pair (trunc w) a

State before:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
hm : a j * trunc w j ≤ pair (trunc w) a
⊢ E w ≤ pair (trunc w) a
Tactic:
rw [trunc_apply, min_eq_right_of_lt hj] at hm
State after:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
hm : a j * E w ≤ pair (trunc w) a
⊢ E w ≤ pair (trunc w) a

State before:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
hm : a j * E w ≤ pair (trunc w) a
⊢ E w ≤ pair (trunc w) a
Tactic:
exact (Nat.le_mul_of_pos_left _ ha).trans hm
State after:
no goals