Theorem: Weight.f_le_mul (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ f w ≤ f (Nat.succ k • w)
Tactic:
simp only [E, f_le_iff, f_apply, sum_smul, pair_smul_left, SetCoe.forall, Subtype.coe_mk]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ ∀ x ∈ testvecs n d,
    Weight.sum w * d / (n + 1) + 1 - pair w x ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w x

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ ∀ x ∈ testvecs n d,
    Weight.sum w * d / (n + 1) + 1 - pair w x ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w x
Tactic:
intro a _
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w a

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w a
Tactic:
have H : w.sum * d / (n + 1) + 1 - w.pair a
           ≤ k.succ * (w.sum * d / (n + 1)) + 1 - k.succ * w.pair a
State after:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a

n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w a

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w a
Tactic:
refine H.trans <| Nat.sub_le_sub_right (add_le_add_right ?_ _) _
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Nat.succ k * (Weight.sum w * d / (n + 1)) ≤ Nat.succ k * Weight.sum w * d / (n + 1)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Nat.succ k * (Weight.sum w * d / (n + 1)) ≤ Nat.succ k * Weight.sum w * d / (n + 1)
Tactic:
rw [mul_assoc]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Nat.succ k * (Weight.sum w * d / (n + 1)) ≤ Nat.succ k * (Weight.sum w * d) / (n + 1)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Nat.succ k * (Weight.sum w * d / (n + 1)) ≤ Nat.succ k * (Weight.sum w * d) / (n + 1)
Tactic:
exact Nat.mul_div_le_mul_div_assoc ..
State after:
no goals

State before:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
Tactic:
set m := w.sum * d / (n + 1)
State after:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
⊢ m + 1 - pair w a ≤ Nat.succ k * m + 1 - Nat.succ k * pair w a

State before:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
⊢ m + 1 - pair w a ≤ Nat.succ k * m + 1 - Nat.succ k * pair w a
Tactic:
set l := w.pair a
State after:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l

State before:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l
Tactic:
cases' lt_or_le m l with hlt hle
State after:
case H.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hlt : m < l
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l

case H.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hle : l ≤ m
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l

State before:
case H.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hlt : m < l
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l
Tactic:
rw [Nat.sub_eq_zero_of_le hlt]
State after:
case H.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hlt : m < l
⊢ 0 ≤ Nat.succ k * m + 1 - Nat.succ k * l

State before:
case H.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hlt : m < l
⊢ 0 ≤ Nat.succ k * m + 1 - Nat.succ k * l
Tactic:
exact Nat.zero_le _
State after:
no goals

State before:
case H.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hle : l ≤ m
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l
Tactic:
rw [← tsub_add_eq_add_tsub hle, ← tsub_add_eq_add_tsub (mul_le_mul' le_rfl hle),
    ← Nat.mul_sub_left_distrib]
State after:
case H.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hle : l ≤ m
⊢ m - l + 1 ≤ Nat.succ k * (m - l) + 1

State before:
case H.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hle : l ≤ m
⊢ m - l + 1 ≤ Nat.succ k * (m - l) + 1
Tactic:
exact add_le_add_right (Nat.le_mul_of_pos_left _ (Nat.succ_pos k)) 1
State after:
no goals