cases' eq_or_ne i k with hi hi <;> cases' eq_or_ne j k with hj hj <;> simp [hi, hj]
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ (if i = k then 1 else min (w i) (E w)) ≤ if j = k then 1 else min (w j) (E w)
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
⊢ 1 ≤ w j ∧ 1 ≤ E w

case intro.intro.intro.intro.intro.inr.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j = k
⊢ w i ≤ 1 ∨ E w ≤ 1

case intro.intro.intro.intro.intro.inr.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
⊢ w i ≤ w j ∨ E w ≤ w j