Theorem: Weight.f_apply_eq_zero_of_neg_pair'_v (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : pair' w (v a) < 0
⊢ f w a = 0
Tactic:
simp only [pair'_v, sub_neg] at h
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ f w a = 0

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ f w a = 0
Tactic:
simp only [f_apply, E, tsub_eq_zero_iff_le]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ Weight.sum w * d / (n + 1) + 1 ≤ pair w ↑a

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ Weight.sum w * d / (n + 1) + 1 ≤ pair w ↑a
Tactic:
zify
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1 ≤ ↑(pair w ↑a)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1 ≤ ↑(pair w ↑a)
Tactic:
change ((Weight.sum w) * ↑d / (↑n + 1) : ℤ) < ↑(pair w ↑a)
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) < ↑(pair w ↑a)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) < ↑(pair w ↑a)
Tactic:
apply Int.ediv_lt_of_lt_mul (by linarith)
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ ↑(Weight.sum w) * ↑d < ↑(pair w ↑a) * (↑n + 1)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ ↑(Weight.sum w) * ↑d < ↑(pair w ↑a) * (↑n + 1)
Tactic:
simp only [mul_comm, h]
State after:
no goals

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ 0 < ↑n + 1
Tactic:
linarith
State after:
no goals