w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
hpos : ∀ (x : ℕ), x ∈ w → 0 < x
⊢ True ∧ ∀ (n : ℕ), n < List.length w → ∃ h, 0 < List.get w { val := n, isLt := (_ : (n, 0).fst < List.length w) }
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
hpos : ∀ (x : ℕ), x ∈ w → 0 < x
⊢ List.length (rowLens (ofRowLens w hw)) = List.length w
simp only [length_rowLens, colLen, Nat.find_eq_iff, mem_cells, mem_ofRowLens,
  lt_self_iff_false, IsEmpty.exists_iff, Classical.not_not]
no goals
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
hpos : ∀ (x : ℕ), x ∈ w → 0 < x
⊢ True ∧ ∀ (n : ℕ), n < List.length w → ∃ h, 0 < List.get w { val := n, isLt := (_ : (n, 0).fst < List.length w) }
refine' ⟨True.intro, fun n hn => ⟨hn, hpos _ (List.get_mem _ _ hn)⟩⟩