Theorem: Weight.f_apply_eq_pair'_v_of_nonneg (Weights/Weights.lean)

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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(f w a) = pair' w (v a) / (↑n + 1) + 1
Tactic:
have H : pair w a ≤ w.sum * d / (n + 1) + 1
State after:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1

n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(f w a) = pair' w (v a) / (↑n + 1) + 1

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

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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1 - ↑(pair w ↑a) = (↑d * ↑(Weight.sum w) - (↑n + 1) * ↑(pair w ↑a)) / (↑n + 1) + 1
Tactic:
rw [sub_eq_add_neg (_ * _), neg_mul_eq_mul_neg, Int.add_mul_ediv_left _ _ (by linarith)]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1 - ↑(pair w ↑a) = ↑d * ↑(Weight.sum w) / (↑n + 1) + -↑(pair w ↑a) + 1

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1 - ↑(pair w ↑a) = ↑d * ↑(Weight.sum w) / (↑n + 1) + -↑(pair w ↑a) + 1
Tactic:
ring_nf
State after:
no goals

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

State before:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(pair w ↑a) ≤ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1
Tactic:
refine Int.le_add_one (Int.le_ediv_of_mul_le (by linarith) ?_)
State after:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(pair w ↑a) * (↑n + 1) ≤ ↑(Weight.sum w) * ↑d

State before:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(pair w ↑a) * (↑n + 1) ≤ ↑(Weight.sum w) * ↑d
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 : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ 0 < ↑n + 1
Tactic:
linarith
State after:
no goals

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