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

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hE : E w = E w'
h : w' ≤ w
⊢ w ≤ w'
Tactic:
simp only [dom_iff, f_le_iff, f_apply, SetCoe.forall, Subtype.coe_mk, hE]
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hE : E w = E w'
h : w' ≤ w
⊢ ∀ x ∈ testvecs n d, E w' - pair w x ≤ E w' - pair w' x

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hE : E w = E w'
h : w' ≤ w
⊢ ∀ x ∈ testvecs n d, E w' - pair w x ≤ E w' - pair w' x
Tactic:
exact fun a _ ↦ Nat.sub_le_sub_left (pair_le_pair_of_lec _ _ _ h) _
State after:
no goals