Theorem: Weight.w1_minimal (Weights/Degree1.lean)

State before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
⊢ w1 n ≤ w
Tactic:
simp only [dom_iff, f_le_iff, f_apply, Subtype.coe_mk]
State after:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
⊢ ∀ (a : ↑(testvecs n 1)), E (w1 n) - pair (w1 n) ↑a ≤ E w - pair w ↑a

State before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
⊢ ∀ (a : ↑(testvecs n 1)), E (w1 n) - pair (w1 n) ↑a ≤ E w - pair w ↑a
Tactic:
intro a
State after:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
⊢ E (w1 n) - pair (w1 n) ↑a ≤ E w - pair w ↑a

State before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
⊢ E (w1 n) - pair (w1 n) ↑a ≤ E w - pair w ↑a
Tactic:
simp only [E_w1, ge_iff_le, tsub_le_iff_right, pair_w1]
State after:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
⊢ 1 ≤ E w - pair w ↑a + if a = tw n 1 0 then 0 else 1

State before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
⊢ 1 ≤ E w - pair w ↑a + if a = tw n 1 0 then 0 else 1
Tactic:
split_ifs with h
State after:
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w - pair w ↑a + 0

case neg
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : ¬a = tw n 1 0
⊢ 1 ≤ E w - pair w ↑a + 1

State before:
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w - pair w ↑a + 0
Tactic:
rw [← f, h, eval_f_tw, hw]
State after:
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w - (1 - 1) * 0 - 0 + 0

State before:
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w - (1 - 1) * 0 - 0 + 0
Tactic:
simp only [mul_zero, tsub_zero, add_zero]
State after:
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w

State before:
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w
Tactic:
exact one_le_E w
State after:
no goals

State before:
case neg
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : ¬a = tw n 1 0
⊢ 1 ≤ E w - pair w ↑a + 1
Tactic:
simp only [le_add_iff_nonneg_left, zero_le']
State after:
no goals