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

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w ≤ w'
⊢ E w ≤ E w'
Tactic:
simp only [dom_iff, f_le_iff] at h
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : ∀ (a : ↑(testvecs n d)), f w a ≤ f w' a
⊢ E w ≤ E w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : ∀ (a : ↑(testvecs n d)), f w a ≤ f w' a
⊢ E w ≤ E w'
Tactic:
specialize h (tw n d 0)
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : f w (tw n d 0) ≤ f w' (tw n d 0)
⊢ E w ≤ E w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : f w (tw n d 0) ≤ f w' (tw n d 0)
⊢ E w ≤ E w'
Tactic:
simp_rw [eval_f_tw, hw, hw'] at h
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : E w - (d - 1) * 0 - 0 ≤ E w' - (d - 1) * 0 - 0
⊢ E w ≤ E w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : E w - (d - 1) * 0 - 0 ≤ E w' - (d - 1) * 0 - 0
⊢ E w ≤ E w'
Tactic:
simpa only [ge_iff_le, mul_zero, nonpos_iff_eq_zero, tsub_zero] using h
State after:
no goals