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

State before:
n✝ n : ℕ
inst✝ : NeZero n
⊢ balanced (w1 n)
Tactic:
simp only [balanced]
State after:
n✝ n : ℕ
inst✝ : NeZero n
⊢ ∀ (j : Fin (Nat.succ n)), w1 n j ≤ E (w1 n)

State before:
n✝ n : ℕ
inst✝ : NeZero n
⊢ ∀ (j : Fin (Nat.succ n)), w1 n j ≤ E (w1 n)
Tactic:
intro j
State after:
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
⊢ w1 n j ≤ E (w1 n)

State before:
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
⊢ w1 n j ≤ E (w1 n)
Tactic:
rw [E_w1, w1]
State after:
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
⊢ (if j = 0 then 0 else 1) ≤ 1

State before:
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
⊢ (if j = 0 then 0 else 1) ≤ 1
Tactic:
split_ifs with h
State after:
case pos
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
h : j = 0
⊢ 0 ≤ 1

case neg
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
h : ¬j = 0
⊢ 1 ≤ 1

State before:
case pos
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
h : j = 0
⊢ 0 ≤ 1
Tactic:
exact Nat.zero_le _
State after:
no goals

State before:
case neg
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
h : ¬j = 0
⊢ 1 ≤ 1
Tactic:
exact le_rfl
State after:
no goals