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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ trunc w ≤ w
Tactic:
rw [dom_iff, f_le_iff]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ ∀ (a : ↑(testvecs n d)), f (trunc w) a ≤ f w a

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ ∀ (a : ↑(testvecs n d)), f (trunc w) a ≤ f w a
Tactic:
intro a
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ f (trunc w) a ≤ f w a

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ f (trunc w) a ≤ f w a
Tactic:
simp_rw [f]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ E (trunc w) - pair (trunc w) ↑a ≤ E w - pair w ↑a

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ E (trunc w) - pair (trunc w) ↑a ≤ E w - pair w ↑a
Tactic:
refine (Nat.sub_le_sub_right (E_trunc_le_E w) _).trans ?_
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
Tactic:
by_cases h : ∃ j, w.E < w j ∧ 0 < a.1 j
State after:
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∃ j, E w < w j ∧ 0 < ↑a j
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a

case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ¬∃ j, E w < w j ∧ 0 < ↑a j
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a

State before:
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∃ j, E w < w j ∧ 0 < ↑a j
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
Tactic:
rw [Nat.sub_eq_zero_of_le (trunc_pair_lb w a h)]
State after:
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∃ j, E w < w j ∧ 0 < ↑a j
⊢ 0 ≤ E w - pair w ↑a

State before:
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∃ j, E w < w j ∧ 0 < ↑a j
⊢ 0 ≤ E w - pair w ↑a
Tactic:
exact Nat.zero_le _
State after:
no goals

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ¬∃ j, E w < w j ∧ 0 < ↑a j
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
Tactic:
push_neg at h
State after:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∀ (j : Fin (Nat.succ n)), E w < w j → ↑a j ≤ 0
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a

State before:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∀ (j : Fin (Nat.succ n)), E w < w j → ↑a j ≤ 0
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
Tactic:
rw [trunc_pair_eq_pair w a h]
State after:
no goals