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

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

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

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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
a : ↑(testvecs n d)
⊢ E (trunc w) - pair w ↑a ≤ E (trunc w) - pair (trunc w) ↑a
Tactic:
exact Nat.sub_le_sub_left (trunc_pair_le_pair w a) _
State after:
no goals